This paper addresses the problem of checking if an updated system is in compliance with the current regulations which apply on the domain. We first present the applicative context in which this problem has been met. We sketch a formalisation of the problem of compliance and we show that is can be split in several sub-problems of different types, the solutions of which are discussed.
This study is part of the ONERA program named IESTA 1 , which aims at developping models, methods and a platform of simulation for analysing innovative concepts of Air Transportation Systems (ATS). This platform will allow its customers (air companies, aircraft manufacturers, official regulation providers, research laboratories and relevant ATS stakeholders) to virtually modify some parameters of the ATS (for instance modify landing procedure, modify types of airplanes, equipe aircrafts with new kinds of fuel...) and analyse the impacts of these scenarii on some environmental metrics.
In particular, this platform will allow its users to study the impacts of expected ATS modifications, on the noise level and chimical emission in the vicinity of a given airport. Modifications of interest will thus be the ones which, according to the simulation, lead to a reduction of noise or/and pollution levels.
In this context, we focus on the particular problem of the compliance of these modifications with the current regulations.
For instance, assume that the simulation shows that, for such a given aiport, modifying the landing procedure in such a given way leads to noise reduction. Before discussing the adoption of this interesting modification, it would be helpful to help users to check if it complies with the current regulations, or if it is incompatible with them or if it is not even ruled.
This is the problem we address. More generally, the problem we are interested in can be described as follows:
given a system composed of several components, given the set of regulations which rule this system, given a modification which is proposed for the system (modification concerning its structure or the way of performing its function), we first want to be able to check if the modified system is in compliance with regulations. If it is not, we want to help users to understand where are the causes of non compliance. Users will then have to revise the given regulations or to revise the proposed modification.
This paper is organized as follows. Section 2 tends to formalise the problem of checking compliance of a system with regulations. Section 3 analyses more deeply this problem and shows that it can be split in several sub-problems of different types. Section 4 focuses on the problem of providing the users an assistance to revise violated regulations. Section 5 mentions some relevant works, the scientific domains they belong to (Information Retrieval and Normative Reasoning) being candidate to provide us with solutions. Section 6 concludes this paper.
The variables of the problem we address are the following.
Definition 1. new denotes the updated system the compliance of which has to be checked.
Definition 2. KB denotes the background knowledge, i.e the knowledge about the considered environment.
Example 1. In the ATS case, if the problem is to check the compliance of the ATS when aircrafts are given a new fuel, then KB may include characteristics and properties of this new fuel (density, volumic mass, inflammation temperature...), but also characteristics of airport environment (atmospheric pressure, physical models...). Any information describing the modified ATS when aircrafts are given a new fuel is in new.
¿From a more formal point of view, new and KB should be modelled in a common model. For instance, KB could be modelled by ontologies, hierarchy of concepts, dependance graphs between concepts, or more generally, and this will be supposed in the rest of the paper, by logical formulas. In the same way, new could be modelled by sets of nodes in the ontologies, sets of concepts, or more generally, and this will be supposed in the rest of the paper, by logical formulas. Assumption In the following, we will suppose that new is compatible with KB i.e, KB ∪ new will be supposed to be a consistent set of formulas.
Consistency is a prerequisite to the problem of compliance since, if KB ∪ new is inconsistant, this means that new contradicts the domain knowldege, thus, building new is impossible. Consequently, the question of checking his compliance is not posed. Definition 3. A regulation r is a triplet: r = < st r , ref r , norms r , def r >, where st r is an ordonned list of the levels which structure the text of r in an arborescent way. ref r denotes the set of other regulations r refers to.
norms r denotes the normative contents of r. If n is in norms r , n is assigned a position label related to st r which denotes its position in the arborescent structure of r. def r is a set of the definitions of the concepts which are used in the regulation text.
Note that several members of norms r may have the same position label. It means that they are in the same text unit in r.
What we want here to capture is that a regulation contains information of very different natures :
conceptual definition information (def r ) : that is an optional part of the regulation. Concepts which are ruled by r are defined in def r . rules (norms r ) : that is the core of the regulation. The rules apply on the real world by stating what is obligatory, permitted or forbidden under which conditions. Formal modelling rules requires the use of a logical formalism dedicated with normative reasoning i.e a deontic logic (see section 5). In the following, we will thus suppose that these rules are modelled by formulas of such a logic. -In a regulation r, conceptual definition and rules are expressed according a given structure (st r ). information about other regulations ref r : regulations which inspire the regulation, regulations which are abrogated by the regulation...One generally mainly find it in the head of the text of r. Example 4. Finally, for r being [2], ref r includes regulations [16] and [3].
Definition 4. R = {r 1 , ...r n } denotes the set of all the regulations which apply on the domain.
Example 5. In the ATS case, the set R of regulations which rule the aeronautic domain is composed of CEE regulations, national regulations such as environment code, civil aviation code, and lots of orders and procedures.
Several relations exist in R such as:
r 2 ≥ S r 1 is true if regulation r 1 is a specialization of regulation r 2 . ≥ S is a partial pre-order defined upon R. r 2 ≥ A r 1 is true if regulation r 2 abrogates regulation r 1 : it means that r 1 doesn't apply anymore since r 2 applies. ≥ A is a partial pre-order defined upon R. a binary relation replace so that replace(a ij , a k l ) is true if the i th article of regulation r j replaces the k th article of regulation r l .
Some of relations of this type has been presented in [4]. Our model represents a slightly simplified form of real regulations, since as for instance, ≥ A could be defined between text units of regulations, and not only between regulations (as for the relation replace) . We here suppose that instances of such relations concerning a regulation r are explicited in ref r . Example 6. Let r 1 and r 2 respectively being regulations [2] and [16]. r 2 ≥ S r 1 , because the regulation dealing with rules concerning the Blagnac airport specializes the regulation about french public air transport. Definition 5. If R = {r 1 , ..., r n } is the set of regulations which apply on the domain, we define norms R , as the set of all the rules of all the regulations of R, i.e, norms R = ∪ n i=1 norms ri norms R is thus a set of formulas of a particular deontic logic.
More formally, we assume that a formal model (formal language and formal inference denoted |= in the following) has been chosen for modelling and reason with rules of norm R , background knowledge KB and modification new2 .
In the rest of the paper, we will suppose that norm R is consistent i.e is a consistent set of rules. 3Checking compliance is then defined by checking one of the following assertions:
1. "case of permitted modification"
This expresses that all the consequences the system modification new (under context KB) are explicitely permitted by the rules in the regulations. In the first case, new could be accepted without any other modification since it is compliant with the regulations.
This expresses that the system modification, new, has some consequences (under context KB) which are explicitely forbidden by one regulation In this case, new cannot be taken into account since it explicitely leads to violate regulations, unless modifying regulations themselves. Localizing the very rules which are violated by new is addressed in section 4.
Notice that in the general case, the prohibition is not caused by only one regulation. So the case of forbidden modification should be described by:
However, in this paper, we assume that the prohibition is caused by a single regulation because it simplifies the presentation of localizing violated rules (see section 4).
∃φ KB ∪ new |= φ and
This expresses that the system modification, new, has some consequences (under context KB) which are neither explicitely permitted nor explicitely forbidden by the regulations. In this case, it will be possible to accept new only after an analyse and modifications of regulations so that consequences of new are permitted.
By definition, these three assertions are exhaustive. Furthermore, they are exclusive only if norm R is consistent. This is the reason why assuming consistency of rules is a prerequisite to the definition of compliance.
Checking compliance can be decomposed into several sub-problems. The idea is to check compliance only on a subset of R, made of regulations which "apply at present" and "concerned by new". At this step, the property "being a regulation concerned by new" remains to be formally defined. This property could be defined so that the test of checking compliance is more efficient in time. It could also be defined so that we can help the user (in the second case) to find the precise articles of the regulations that are violated.
-Problem pb 1 : find the "regulations which could be violated"
This problem can be divised into two sub-problems as follows:
• Problem pb 1.1 : find the "regulations which apply at present" This problem consists in selecting the regulations which are not abrogated nor replaced by other regulations. In other words, the problem is to focus only on the regulations that apply at the moment. This problem may be defined by : find max ≥ A (R) 4Information in ∪ n i=1 ref ri will be hepful to solve this sub-problem .
• Problem pb 1.2 : find the "regulations concerned by new" This problem is a problem of Information Retrieval, the information to be retrieved being regulations.
In order to solve it, considering information in ∪ n i=1 def ri (i.e definitions of the concepts used in the regulation text) will be necessary.
The two above sub-problems may be solved in any sequence order : each of them contributes towards reducing the set of regulations to be considered in checking compliance.
Let us denote R new the set of the regulations of R which apply at present and which are concerned by new.
-Problem pb 2 : checking compliance of new with R new This comes to check the three assertions:
In this section, we suppose the case when new doesn't comply with R new . I.e, we assume that the second assertion of problem pb 2 is true. In order to assist users in revising such regulations, several kinds of aids may be proposed to him. Below we sketch some induced problems.
Let r ∈ R F orbidden . This problem consists in:
1. exhibiting the elements in norms r which are involved in a demonstration of "forbidden modification". 2. finding their position label in r (according to st r , as defined in definition 3).
The problem is to identify the uppest regulations involved in non compliance, towards the specialization relation defined on R : in other words, it is to identify sources (in the specialization or hierarchical sense) of non compliance.
Formally : find max ≥ S (R F orbidden )
-Problem pb 5 : propagate a cause of non compliance in a set of regulations The problem is, given a regulation involved in non compliance, to identify all the regulations which specialize it. These regulations, because they take their inspiration from the violated regulations, are are also involved as causes of non compliance.
Formally : let r ∈ R F orbidden , find {r ∈ R F orbidden , r ≥ S r }.
-Problem pb 6 : explanation for non compliance The problem is to give an informative explanation based upon non compliance demonstrations. This comes to a problem of Explanation Generation, which has been studied for many years [20], [1].
Among the different sub-problems we have raised in the previous sections, two of them are of particular interest. More specifically, these are: a problem of information retrieval, the information to be retrieved are regulations (cf problem 1.2) and a problem of normative reasoning (cf problem 2). These two very different questions have been addressed by many works we mention some of them below.
Information Retrieval is a vast domain of research whose works aim to define models and methods or algorithms, to retrieve information among a large set of information, like the web space. See [22] for an interesting overview. The user's demand is formalised by a query Q (of the form "retrieve documents which contains terms t 1 ...t n ").
The three most used models in Information Retrieval are the vector space model, the probabilistic model and the inference network model.
According to the vector space model, the user query as well as the documents the query is addressed to, are represented by vectors of terms (words of a given vocabulary for instance). The score of a document is defined as a similarity degree between its vector and the query vector. Several similarity degrees are usually used, among which the dot product defined by: if D denotes the document vector and Q denotes the query vector, then the score of D for Q is:
where d i is the value of the i th component of (D) and q i is the value of the i th component of (Q). The value d i (resp q i ) is called the weight of the di th term in the document (resp, query).
Various methods for weighting terms have been defined. All of them are based on different parameters which are : term frequency (words that repeat several times in a text are considered salient), document frequency (words that appear in many documents are considered common and are not very indicative of document content), the number of documents that contain a given term, the document lenght (in bytes), the average document length (in bytes)... As for Probabilistic models, they assume that documents in a collection should be ranked by decreasing probability of their relevance to a query (probabilistic ranking principle). Since knowing its true value is impossible, the probability of relevance of a document to a query has to be estimated. In this family, the models differ from the way they estimate that probability of relevance.
Last models are Inference network models. In these models, document retrieval is modeled as an inference process in an inference network.
Since we consider Regulation Retrieval as a particular case of Information Retrieval, solving pb 1.2 could be done by adapting a model of Information Retrieval. For doing so, the definitions of concepts used in a regulation (i.e the def r part) has obviously an important role to play in the process. Furthermore, the very structure of regulations (i.e the st r part) is also something particular which must be taken into account by Regulation Retrieval models to be defined ( [4], [9]).
Let us also mention [10], in which the authors define a tool to analyse a regulation and extract rights and duties expressed in the regulation. Legal texts are annotated in order to identify the agents, their rights (actions that the agents have the permission to perform under come conditions) and duties (the actions they have to perform under some conditions)... A semantic model in then built from these annotations.
Let us finally cite [13], in which the author defines a legal ontology of the french Law. Such an ontology could be used as a common concept description language and links with the def r part of regulations should be establised.
Problem pb 2 raises the question of checking if a given formula, (here permitted(φ) or f orbidden(φ)), is implied by some rules (here norms Rnew ). This is a particular case of what is called "normative reasoning" i.e, reasoning with norms.
Reasoning with norms requires at least modelling deontic notions (permission, prohibition, obligation...). But it also requires modelling individuals (agents on which obligations, permission and prohibition apply) and properties on individuals. It sometimes also require modelling several dimensions of time (time of validity of norms, deadlines...) and different types of norms (defeasible norms, Contrary-to-duties...). To our knowledge, there is no general logical formalism which allow to reason with so many different notions. However, there are several kinds of formalisms which allow to model some aspects of the norms. These are deontic logics [8].
Most of deontic logics are modal ones, [5], since deontic operators are not very-functional operators (for instance, it may be the case that smoking is forbidden, even if somebody is smoking). Some of them are based on dynamic logics [15], or based on temporal logics, or both [7]. They also may be non monotonic [11], [23].
However, First Order Logic (FOL) can also been used to reason with deontic notions ( [21], [14], [17], [19], [12]...) and is a compromise between expressivity and simplicity. In this case, normative reasoning comes to a problem of theorem proving in FOL which is solved (at least from a theoretic pioint of view) by different means: provers based on Resolution Rule, tableaux methods, or any method defined for the SAT problem.
Let us finally mention a very theoretical but interesting work, [18], in which the authors define a dynamic deontic logic for reasoning with consequences on permissions and prohibitions, that the modification of a policy generates. This aims at helping the user who wants to modify a regulation, by allowing him/her to derive the permissions which were valid before the modification and which are no more valid after; or the permissions which become valid after the modification etc.
In this paper we have addressed the problem of checking compliance of an updated system with regulations. The main contributions are a formalisation of this problem and its decomposition in several sub-problems of different types. We also sketched some functionalities which could help a user to revise regulations in case of non compliance. We finally quickly presented relevant litterature, more precisely Information retrieval and Normative Reasoning, which could offer solutions.
Notice however that this work is very preliminary and thus raises many open questions, the most important one being the definitions of the solutions of the different sub-problems and their applicability as well. The case named "case of a non ruled modification" has also to be studied. And the model of regulations used in this work, has to be refined in order to take into account a finer granularity of representation. Indeed, for instance, this model does not allow to represent relations between text units .
However, even preliminary, this work enlights the complexity of the problem of checking compliance and the varieties of questions to be solved.
Acknowledgments. We would like to thank the anonymous reviewers for their comments which helped us to improve the paper.