Line Jakubiec-Jamet
email: line.jakubiec@lif.univ-mrs.fr

A Case-study for the Semantic Analysis of Sentences in Coq

Keywords: natural language processing, Coq system, semantics, conceptual analysis

This paper presents a case-study devoted to the formalization of sentence frames in the Coq system. Therefore, we instanciate these frames for performing a semantic analysis of simple sentences. In particular, we rely on a hierarchy of types for type-checking the conceptual well-formedness of sentences. To do so, we investigate how to exploit the particular features of the Coq type system in order to take advantage of this elegant unifying framework for encoding the syntax-semantics interface and then we show how to improve our approach for combining it with linguistic resources distributed.

Introduction

During the last fifteen years, the use of type theoretic methods for describing natural langage syntax and semantics has gained more and more popularity, resulting in the development of software relying on these methods. On the one hand, these type theoretic methods can be constantly improved with advances in the field of logic. On the other hand, they depend on the developement of linguistic resources such as lexicons or dictionaries. In this context and from our point of view, the challenge for natural langage processing is twofold : first, the frameworks dedicated to linguistic analysis have to focus on the syntax-semantics interface ; secondly, they have to combine linguistic resources and natural language processing programs. Among the most significant achievements, let us mentionned the works on categorial grammars which provide the integration of syntax and semantics in the same framework as it is described in [START_REF] Moortgat | Categorial Type Logics[END_REF] and in [START_REF] Retoré | Systèmes déductifs et traitement des langues, un panorama des grammaires catégorielles[END_REF]. Moreover, categorial grammars are lexicalized that means that all items in the lexicon are typed. Thereby, although they describe syntactical rules, they also preserve the compositional aspect of Montague semantics [START_REF] Montague | The Collected Papers of Richard Montague[END_REF]. The most wellknown categorial grammars are those based on Lambek-Calculus [START_REF] Lambek | The Mathematics of Sentence Structure[END_REF]. Due to the Curry-Howard isomorphism, typed terms are proofs in logic which includes Lambek-Calculus1 . Although many studies have already showed that it is natural to associate a syntactic term to a semantic type and reciprocally [START_REF] Ranta | GF: a Multilingual Grammar Formalism[END_REF] [START_REF] Moot | The Logic of Categorial Grammars[END_REF] [23], our approach implemented in Coq, the Calculus of Inductive Constructions, aims to focus on the generality of definitions leading to reusable methodologies dedicated to pragmatic2 semantic analysis. In Coq, few investigations have been performed for natural language processing. [START_REF] Coscoy | Explication textuelles de preuves pour le calcul des constructions inductives[END_REF] developed an algorithm that produces natural language sentences from proofs described in a mathematical language. Later, for the case of categorial grammars, [START_REF] Anoun | Reasoning on Multimodal Logic with the Calculus of Inductive Constructions[END_REF] gave a Coq formalization of the Lambek-Calculus and of an extension as multimodal grammars, and proved in particular several theorems as completeness and consistency of multimodal logic. However, we are not aware of any work that straightforwardly used specific features of Coq language, for linguistic analysis. This paper presents on a casestudy, the capabilities of Coq for the determination of a sentence's conceptual well-formedness from general representations of sentences. Let us remark that the conceptual analysis is part of the traditionnal semantic analysis which takes into account the contextual analysis as well. Actually, the former determines the compatibility of the elements from which the sentence is composed (compositionality of words), while the latter studies the combination of sentences with each others (texts). The study is inspired by concepts developped in a prototype, Illico [START_REF] Pasero | [END_REF], realized in the research team TALEP (LIF) 3 . In Illico, the conceptual analysis is based on a first-order typed λ-calculus which is implemented in Prolog. Then, these Prolog rules are used to define relations that represent sentences. Moreover, the conceptual analysis is encoded according to conceptual types that are used to determine the compatibility of the words in a sentence. Types are hierarchically organized and they describe an ontology4 itself implemented as Prolog rules. This paper proposes a more straightforward approach and the relevance of our encoding in Coq can be summarized as follows :

1. define formal models for representing sentences by taking advantage of the Coq type system and its particularly rich language (polymorphism, higherorder logic, coercion mechanism, module system),

2. propose natural and general specifications of sentences that can be checked for a conceptual analysis based on types, 3. directly encode typed λ-terms without first specifying λ-calculus in a language and then, implement representations of sentences in the specified λcalculus, 4. take advantage of type-checking algorithms involved into the Coq system.

The paper is organized as follows. Section 2 briefly introduces Coq by focusing on used aspects. Section 3 deals with a formalization of the underlying ontology and with a semantic representation of simple sentences. In Section 4, we generalize our approach by specifying generic models for other sentences and we show how to use them. We mention in section 5 some tools and resources for improving our work. Then, on the conclusion, we further discuss the case-study and we highlight our perspectives.

An Overview of Coq

The Coq system [START_REF]INRIA: The Coq Proof Assistant[END_REF] is a specification and proof system developed in the LogiCal project at Laboratoire de Recherche en Informatique (CNRS and University of Paris-Sud) and LIX (INRIA-Futurs and Ecole Polytechnique). Coq's language relies on a higher-order typed λ-calculus, the Calculus of Constructions [START_REF] Coquand | Une Théorie des Constructions[END_REF] [START_REF] Coquand | Constructions : A Higher Order Proof System for Mechanizing Mathematics[END_REF] enriched with inductive and co-inductive definitions [START_REF] Paulin-Mohring | Inductive Definitions in the System Coq -Rules and Properties[END_REF] [START_REF] Giménez | Un calcul de constructions infinies et son application à la vérification de systèmes communicants[END_REF]. Coq's logic is a constructive logic and it is based on the propositions-as-types correspondence, the Curry-Howard isomorphism, that states a proposition is a type and a proof is a term inhabiting this type. This correspondence provides an elegant unifying framework where type-checking is proof-checking. The Coq system is tactic oriented and it allows to interactively develop proofs. The system is organized around a small kernel (the theory) extended by libraries. Moreover, it includes many user contributions. Coq developments can be splitted into various parameterized modules. Thus, several developments can share modules that, being compiled once and for all, are loaded fast. Moreover, sections allow to organise modules in a structured way. In Coq, any user's term must be classified according to a type. There are two sorts of types : logical propositions are of sort P rop and mathematical collections are of sort Set 5 . Polymorphic terms are parameterized with respect to terms of sort P rop or Set. By defining them into a section, one can obtain reusable developments in which generic specifications has been already typedchecked. However, when instanciating these abstract specifications, types can be cumbersome. The implicit parameter mechanism allows to automatically infer arguments from the definition's context. Moreover, Coq terms are organised according to a type hierarchy and they can be typed using the coercion subtyping system. This latter corresponds to an inheritance graph mechanism that allows to inject Coq hierarchy typed terms into another hierarchy's type. Technically, a term of type t is also of type t 1 (where t and t 1 are of types P rop or Set for example) if there exists a coercion between t 1 and t, defined in Coq as :

Coercion c : t1 >-> t.
The above declaration expresses the construction denoted by c as a coercion between t1 and t. Roughly speaking and for the need of the study, the coercion c indicates that t 1 is a subtype of t.

Sentence's Conceptual Analysis

The Starting Point : Illico's Conceptual Analysis

Illico is a generic software tool designed for analysis and synthesis of natural language [START_REF] Pasero | [END_REF]. It provides tools and formalisms to encode and to analyse lexical, syntactic and semantic knowledge. This latter allows the determination of a sentence's conceptual and contextual well-formedness. To sum up, Illico is able to perform any of the following tasks :

1. analyze sentences and display the representations associated with each one of them at the syntactic and semantic levels ; 2. detect during analysis, lexically, syntactically or semantically unexpected words ; 3. guide the composition of sentences, by displaying possible continuations for the user's sentence.

From a computational point of view, the Illico semantic analysis includes the following aspects :

1. Formal semantic representation : once the lexical and syntactical levels of a natural language expression are completed, then Illico automatically generates a semantic representation of this expression. This latter is encoded from composition rules, using first-order typed λ-calculus. 2. Conceptual validation : then, the typed λ-expression must be conceptually verified. If it describes a compatible situation with the underlying ontology, the conceptual well-formedness is established.

Technically, as it has been mentionned in Section 1, these two considerations are managed with Prolog rules. Semantic representations are λ-expressions encoded in Prolog and they are defined from a set of semantic labels. These latter corresponds to two basic types : i (that stands for agent) and o (that stands for boolean expressions or relations). For example, a verbal group is labelled < i, o > because it needs an agent (the subject) and an evaluation (the application of the subject to the verb). The expression verbal group = λx (name group (verb x)) where name group and verb are respectively labelled << i, o >, o > and < i, < i, o >>, represents the semantic rule to be conceptually verified 6 . Then, the conceptual validation is based on a conceptual tree as it is described hereunder.

Ontology as Concept Hierarchy

This section is devoted to the presentation of the ontology used to determine the well-formedness of sentences. Let us note that the "concepts as types" representation is largely used in the knowledge representation since it provides an appropriate interface for semantic processing. Figure 1 presents a conceptual hierarchy which organises concepts according a world we want to refer for our study. The verification of the sentence's conceptual well-formedness will be based on this hierarchy. It describes a simple world from which it is possible to analyse the meaning of sentences. This world is organized from animate and inanimate notions. For example, an animal is classified into the animate concept while a car is inanimate and can be considered as concrete as well. In this tree, each node is labelled by a conceptual information that can be specified as a type. Thus, for organizing this information, it is natural to consider the subtyping principle. In typed definitions, a subtype may appear wherever an element of the super type is expected. For example, in our verb's semantic representation (Section 3.3), a type t 1 is compatible with a type t, if t 1 is a subtype of t. Consequently, a semantic representation parameterized with t will be valid for parameters of type t 1 and for all those of the lower part. In Coq, we declare the conceptual types (all, animate...) as logical propositions. Then, we use the coercion mechanism for describing the relations between types, as follows :

Coercion animate_is_all : animate >-> all. Coercion animal_is_animate : animal >-> animate. Coercion dog_is_animal : dog >-> animal) Coercion cat_is_animal : cat >-> animal) ...... Each coercion creates a path between two nodes of the tree. The whole list of coercions is ordered and it defines the conceptual tree depicted in Figure 1. Coq detects ambiguous paths during the creation of the tree and, it verifies the uniform inheritance condition because at most one path must be declared between two nodes. Let us remark that, in Coq, the conceptual tree is straightforwardly implemented, in a natural way. Therefore, Coq automatically verifies that the hierarchy of types is well-formed. Moreover, the conceptual analysis will be parametrizable by this kind of hierarchy : in general, the ontology depends on the field under consideration and it is interesting to be able to change the ontology according the needs. Just for comparaison, the corresponding specification in Prolog is given hereunder : domain:all(all.v24457) -> ; domain:animate(all.animate.v24459) -> ; domain:animal(all.animate.animal.v24460) -> ; domain:dog(all.animate.animal.dog.v24461) -> ; domain:cat(all.animate.animal.cat.v24461) -> ;

It shows all the necessary paths from the root all. This Prolog specification is generated from the Illico interface : a parser analyses rules given by the users (as for example all = {animate, inanimate}) and constraints are introduced (into the parser) for avoiding incompatibilities in the tree ; in Coq, this processing can be directly used by means of the coercion mechanism. Later, in Section 5, we propose a tool that generates the hierarchy from a graphical interface for alleviating the creation of ontologies in Coq.

Coq Semantic Representation of Sentences

This section proposes a semantic formalization of simple sentences. Since a sentence is composed of elements that must be compatible with each other, we first deal with their representation and their types. In particular, we focus on the verb's description because the sentence's representation is specified according to the verb's domain of use. Then we describe a generic model for sentences which involve a verb and its subject. Finally, we show, by instanciation of the model, how sentences are semantically represented. Therefore, the verb has a central role in the sentence, as it has been developed in the Tesnière's linguistic theory [START_REF] Tesnière | Eléments de syntaxe structurale[END_REF] which defines the valence of verbs. Let us mention that, this characterisation of sentences have been widely used in the dependency grammars as it is described in [START_REF] Kahane | Grammaires de dépendance formelles et théorie sens-texte[END_REF].

Lexicon of Verbs For typing the verb's representation, we use the conceptual types described in Figure 1. For each verb, we have to choose the best label (best for the user who build the lexicon that is to say the most likely concept for the domain under consideration) which, in general, corresponds to the lower type in the hierarchy. For example, the verb to bark can reasonably be used for all the dogs. So, it is declared in the lexicon as a logical proposition by the unary predicate bark as follows :

Parameter bark : dog -> Prop.

Let us note that verbs can have different meanings and so, different lexical entries have to be considered. In [START_REF] Moot | A Discursive Analysis of Itineraries in an Historical and Regional Corpus of Travels[END_REF], the authors deal with this aspect on a study formalized in categorial grammars. They introduce constraints which change the interpretation of verbs by means of specific functions that change the type of terms. Our approach is different because once the hierarchy of types is defined, the verbs have to be described on these types. So, we can need to consider several declarations in Coq for the same verb. For example in french, the verb bark can be used for humans : Paul barks. (in the sense that Paul inveighs against someone or something) is an acceptable sentence. Here, we introduce a new input in our lexicon as :

Parameter bark2 : human -> Prop.
This is not really cumbersome because dictionnaries of verbs are built from all the possible situations (as it is described in the Section 5) and then, the Coq representation is very concise.

In Illico, the lexicon entry has to be duplicated as well (if needed). Let us remark that each input of the lexicon is specified by two following rules as, for example : lexicon(verb0,<to_bark>,<is_barking>,...) -> ; semantic.txt:verb_0 = <i,o> ;

where informations as lexical category (verb0), lemmatized form (< to bark >), used form (< is barking >) and other features appear. These characteristics are used for syntactic verification as well, but it is not the focus here.

Sentences as logical expressions

Let us now consider the sentence : A dog is barking. It can be represented by the logical expression : ∃x, bark(x) ∧ is dog(x) where the unary predicate is dog characterizes the semantics of the subject dog. The following predicates introduce in Coq semantic representation for some agents used later in the paper : The domain of definition is more general than the agent itself for avoiding dead end situation. It is a choice made in the Illico conception. For example, suppose the negative question : Who is not an animal? If is animal is defined on animal, we can write the expression ∃x, ¬is animal(x) (where x implicitly is of type animal and x must be instanciated to obtain a final well-typed representation). But any x will exist because no conceptual verification will allow the final representation (x must be of type animal or one of the subtypes of animal). If is animal is defined on animate, x will exist and can be, for example, a parameter h of type human, because the expression ¬is animal(h) is valid. Finally, for a first approach, the sentence : A dog is barking merely can be represented in Coq as follows :

Definition a_dog_is_barking := exists x, bark(x) /\ is_dog(x).

where the implicit argument mechanism automatically synthesizes the type of x as dog (from the first predicate of the definition).

Towards Generic Models Up to now, the kind of sentences we study is composed of a verb and a subject. In this part, we show how to generalize this kind of sentences by specifying a general frame in Coq that states : ∃x, verb0(x) ∧ is something(x), where verb0 (that stands for the verb) and is something (that stands for the subject) are polymorphic predicates respectively parameterized on A1 and A of sort P rop, with A1 subtype of A (to ensure the compatibility between words). The complete specification in Coq is given below, inside a section : In the definition f rame verb0, c is implicitly of type A1 and the coercion A1A which converts the type A1 to A is implicitly applied on c into is something(c).

Outside the section, the local context of the definition is discharged. This means that A, A1, A1A, verb0 and is something appear as parameters of the definition f rame verb0. So, f rame verb0 depends on two types, on a coercion which states a subtyping relation and on two predicates which respectively stand for a verb and a subject. It is a generic representation for this kind of simple sentences due to polymorphism (from the parameters A and A1) and higher-order (from the verb0 and is something predicates).

Type-checking is Well-formedness Checking By instanciation of the generic model f rame verb0, we can define the semantic representation of the sentence A dog is barking as :

Definition a_dog_is_barking := (frame_verb0 dog_is_animal bark is_dog).

The instanciation of the parameters A and A1 can be omitted due to the implicit synthesis. The coercion dog is animal instanciates A1A in the generic model ; bark, which is defined on dog, instanciates verb0 and is dog, which is defined on animal, instanciates is something. So, the compatibility of words is ensured by the coercion that states dog is a subtype of animal.

In a similar way, the sentence A cocker is barking is formalized as :

Definition a_cocker_is_barking := (frame_verb0 cocker_is_dog bark is_cocker).

But the checking of A cat is barking :

Definition a_cat_is_barking := (frame_verb0 cat_is_animal bark is_cat).
is rejected by the system because the term bark has type dog → P rop, while it is expected from cat is animal (the coercion that states cat is a subtype of animal) to have type cat → P rop. This encoding leads to simple conceptual representation of sentences. Coq performs the type-checking of these instanciations and so, it establishes the sentence's well-formedness.

Generic Models Based on Verb's use

In this section, we propose two other generic frames for representing the sentences. The first one describes sentences which are composed of a verb, a subject and a complement. The second frame defines sentences where the parameters of the verb depends on each others. This latter is interesting is the case-study because it emphasizes the dependent aspect of typing for natural language processing.

Let us consider the sentence A woman likes cars. In this case, the verb to like may be of type animate → inanimate → P rop, where animate stands for the type of the subject and inanimate for the type of the complement 7 . Similarly to the representation given in Section 3.3, we can specify : where the model f rame verb1 is obtained from the generic definition depicted below : Definition frame_verb2 : Prop := exists h:human, exists a1:A1, exists a2 :A2, verb2 h a1 a2 /\ is_human h /\ is_something1 a1 /\ is_something2 a2.

End General_frame_v2.

The two types from A are A1 and A2 ; the variable verb2 sets that the first argument is a human while the following are from A.

As already described, due to implicit synthesis, the application (verb2 h a1 a2) is actually (verb2 h (A1A a1) (A2A a2)), for generating the type A from A1 and from A2. The instanciation of this frame is similar to the previous paragraphs and it is not given here.

Tools and resources

This section is devoted to the presentation of practical tools for faciliting the use of our work in Coq. Really, the interface presented to the user has to hide the logical aspects of the Coq specifications which can be cumbersome for a linguistic analysis. The Figure 2 gives an overview of the application based on the Coq type-checking presented in the paper. It is not yet fully implemented but it allows to explain the motivations of our work. The application takes as input a natural language sentence. A parser implemented in Java allows to interactively tag verbs the user wants to classify according an ontology (as for example, the Figure 1). This classification (program1 in the above figure) provides a lexicon of verbs in Coq (for instance, bark is tagged as dog → P rop depending on the choice of the user). The Coq description of the ontology can be automatically obtained by the program2 [START_REF] Azzabi | Description et analyse d'arbres à l'aide de Prefuse[END_REF] in the figure. This program uses the Prefuse toolkit [START_REF] Heer | Prefuse: a Toolkit for Interactive Information Visualization[END_REF]. Prefuse allows the user to graphically design its ontology without specifying Coq descriptions ; so program2 generates the Coq file that describes the coercion between types and also the semantic predicates corresponding to the ontology (is dog : animal → P rop for instance). Then the user chooses the Coq generic frame to be instanciated and the conceptual validation is performed as it has been depicted in this paper. If the representation of the sentence could be type-checked into Coq, the application outputs that the sentence is valid ; otherwise, it returns that the sentence is not valid. This application is motivated from the fact that there are few resources in french for having semantics on words. The classification mechanism seems to be interesting for our study because it allows to abstract properties for classes of verbs. Several linguistic resources rely on this aspect. On the one hand, there are dictionaries that provide a precise explanation of words : in [START_REF] Dubois | Les verbes français[END_REF], verbs are described as semantics classes whose scope is defined by syntax. These classes are generic and each of them gathers properties of verbs. For example, there is the class dedicated to the communication verbs. This latter is divided into 4 semantic categories (for french language) : 1. human, animal (to shout, to speak) 2. human (to say something) 3. human (to show) 4. figurative sense Then these categories are subdivided into syntactical sub-classes which describe the use cases of verbs (the verb can be used with a subject and a complement, it can be transitive or intransitive and so on).

On the other hand, lexicons have been developed from dictionaries and [START_REF] Dubois | Les verbes français[END_REF] have been used in several implementations as in [START_REF] Silberztein | La formalisation du dictionnaire LVF avec Nooj et ses applications pour l'analyse automatique de corpus[END_REF], [START_REF] Franc ¸ois | Classements syntactico-sémantiques des verbes français[END_REF] and [START_REF] Hadouche | Une version électronique du LVF comparée avec d'autres ressources lexicales[END_REF]. The study of these resources for the development of our application should be useful because they provide many linguistic descriptions not taken into account in our casestudy. So they may be reused and connected to our application.

Conclusion and Perspectives

The work presented in this paper aims at studying the capabilities of the Coq system, in the field of semantic representation and conceptual analysis for natural language processing. The relevance of our encoding has been motivated by the particular features of the Coq system. It provides an unifying framework with a rich type system that allows to straightforwardly specify the underlying conceptual tree as well as to analyse semantic representations. In this paper we have proposed :

1. a way for describing ontologies in Coq, 2. several reusable sentence's semantic representations, 3. a sentence's conceptual analysis by instanciation process.

In particular, for this analysis, we focused on several aspects of the Coq system :

1. polymorphism : the generic models of sentences are parametrized by types and they can be reused for specifying specific sentences. 2. higher-order : it allows to take as parameters relations and so it provides a good framework for developing general definitions. From these definitions, specific sentences are derived by instanciation. 3. modularity : the development is split into several sections. This contributes to lisibility and it allows an easy reuse of libraries. 4. coercion mechanism : the hierarchy of types is easily described in Coq and it is a good way for knowledge representation based on types. 5. implicit parameters : the implicit synthesis of some parameters greatly improves the readability of the definitions.

The case study proposed in this paper is being extended to several other modules.

In particular, it requires the addition of the following :

1. extension of the verb's lexicon : the lexicon takes into account around 50 verbs. We plan to use the developments of LVF mentionned in the Section 5 for improving the semantic analysis (by specifying classes of verbs and general models that characterize the uses of verbs). This study will allow to integrate syntactical rules for introducing more linguistic information in our representations. From this specification, formal properties about sentence's representations could be established in order to validate linguistic rules in Coq. 2. representation of other sentences : once the lexicon will be extended, it will be possible to describe other generic models of sentences. 3. contextual analysis : for completing the semantic analysis, contextual representation will be necessary. This will allow to analyse texts and not just sentences.

Finally, the application depicted in the Figure 2 should be completed by adding more automatic processing : firstly, in the parser, the tagging of verbs has to be improved. This can be done using an underlying lexicon which includes linguistic properties about verbs (conjugaison patterns, lemmatization for example). Secondly, the interface between the lexicon and the ontology has to be developped. This process involves the programming of an interface that allows to manipulate verbs and concepts according to the domain of the sentences to be analysed. Thirdly, it should be relevant to give more explanation about the output when an invalid sentence has been detected. This is possible by retrieving from the Coq system the information about typing, in order to propose for the user, some accepted constructions of sentences.

Fig. 1 .

 1 Fig. 1. A hierarchy of conceptual types

  Parameter is_animate : all -> Prop. Parameter is_animal : animate -> Prop. Parameter is_human : animate -> Prop. Parameter is_dog : animal -> Prop. Parameter is_cocker : dog -> Prop.

  Local parameters of the section **) (A1A : A1 -> A). Coercion A1A : A1 >-> A. (** Declaration of the subtype **) Variables (verb0 : A1 -> Prop) (** Declaration of the predicates **) (is_something : A -> Prop). (** Definition of the generic model **) Definition frame_verb0 := exists c, verb0 c /\ is_something c. End General_frame_v0.

  Choice of the frame to be instanciated

Fig. 2 .

 2 Fig. 2. Overview of the application based on a Coq analysis

Note that there are new approaches that extend Lambek-Calculus, in particular in linear logic because it provides an efficient representation of proofs[START_REF] De Groote | Semantic Readings of Proof Nets[END_REF] [27][START_REF] Lecomte | Grammaire et théorie de la preuve : une introduction[END_REF] and specific tools have been developed in this field as for example[START_REF] Moot | A short Introduction to Grail[END_REF].

The semantic analysis presented in this paper is pragmatic is the sense that, it plans to use linguistic resources mentionned in the section 5 in order to obtain a tool used by linguists.

Traitement Automatique du Langage Ecrit et Parlé (Laboratoire d'Informatique Fondamentale de Marseille)

Ontologies are widespread in the process of improving sentence's analysis. Many studies are based on the development of ontologies specially designed for managing the conceptual knowledge[START_REF] Asher | Lexical Meaning in Context. a Web of Words[END_REF] [4][START_REF] Oltramari | Restructuring Word-Net's Top-level: The OntoClean Approach[END_REF]. The advantages of using ontologies in natural language processing are : on the one hand, they provide a way to represent semantics of a given domain on which sentences have to be analysed ; on the other hand, it is possible to reuse or reorganize the knowledge depicted into the ontology.

Actually, this distinction is not necessary but it makes the system less confusing for the user. However, it is significant when extracting programs from proofs (a mechanism relying on the constructive aspect of Coq's logic). But this feature is not used here. For more details, one can refer to[START_REF]INRIA: The Coq Proof Assistant[END_REF].

Moreover, these semantic rules are associated to syntactic rules involved in the grammar of Illico named GNF (Grammaire Noyau du Français).

But, more generally, the type of the verb to like in the lexicon is animate → all → P rop because the type of the complement must be as general as possible.

Section General_frame_v1.

Variables (A A1 B B1:Prop) (A1A : A1 -> A) (B1B : B1 -> B).

Coercion A1A : A1 >-> A.

Coercion B1B : B1 >-> B.

Variables

Definition frame_verb1 := exists x, exists y, verb1 x y /\ is_something1 x /\ is_something2 y.

End General_frame_v1.

As in the previous frame, coercions has been defined between A1 and A and between B1 and B. The predicates is something1 and is something2 respectively stand for the subject and the complement. So the instanciation of f rame verb1 is realized using the two coercions woman is human and car is concrete, the verb like and the predicates is woman and is car.

The second model describes a particular case where sentences are composed of a verb, a subject and a complement as well, but the typing of the verb is more binding. For example, let us consider the verb conf use. Only a human can conf use two things that must represent the same concept in the hierarchy (for instance, a man confuse two dog breeds, two particular cars and so on ; but he cannot confuse a car and a dog). So, the type of the generic relation (verb2 in the hereunder definition) that stands for conf use is human → A → A → P rop where A gives the general concept to be used but the two subtypes of A can be different althought they are from the same concept. This is specified in the next Coq definition inside a section : Section General_frame_v2.

Variable A A1 A2 : Prop. Variable A1A : A1->A. Coercion A1A : A1>->A. Variable A2A : A2->A. Coercion A2A : A2>->A.

Variables (verb2 : human-> A -> A -> Prop) (is_something1 : A1 -> Prop) (is_something2 : A2 -> Prop).


Romain Jacob
email: romain.jacob@ens-cachan.fr

Jean-Jacques Lesage

Jean-Marc Faure

Opacity of Discrete Event Systems: models, validation and quantification

Keywords: Opacity, Discrete event systems, Validation, Verification, Enforcement Quantification, Secrecy, Privacy, Security

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

INTRODUCTION

Online services and network communications have become ubiquitous over the past 30 years. This evolution in our everyday life brought along new preoccupations regarding security and privacy. Despite continuously releasing tons of information about everything we do and think, we still want some information to remain secret. Thus, a new problem has arisen in computer science, called Information Flow. It characterizes the (possibly illegal and indirect) transmission of secret data from a high level user to a low level one. Various information flow properties have been defined in the literature: anonymity, non-interference, secrecy, privacy, security and opacity. In this paper, we focus on opacity, which characterizes whether a given "secret" about a system behavior is hidden or not from an external observer, further called the intruder. It is assumed the intruder has full knowledge of the system's structure but only partial observability. Based on its observations, the intruder constructs an estimate of the system's behavior. The secret is said to be opaque if the intruder's estimate never reveals the system's secret. Specifically, the system is opaque if for any secret behavior, there exists at least one other non-secret behavior that looks the same to the intruder. Opacity is a rather recent field of research. It was first introduced in 2004 in computer science to analyze cryptographic protocols [START_REF] Mazaré | Using unification for opacity properties[END_REF]). It reached the discrete event systems (DES) community with the work of [START_REF] Bryans | Modelling opacity using petri nets[END_REF] which investigated opacity in systems modeled as Petri nets. Secrets were set as predicates over Petri net markings (i.e., states). In [START_REF] Bryans | Opacity generalised to transition systems[END_REF], previous work was extended by investigating opacity in labeled transition systems (LTS), in which secrets were defined as predicates over runs. More recently, Saboori and Hadjicostis investigated state-based opacity properties using finite-state automata (FSA) models [START_REF] Saboori | Notions of security and opacity in discrete event systems[END_REF], [START_REF] Saboori | Verification and enforcement of statebased notions of opacity in discrete event systems[END_REF]). Many researchers have considered the validation of opacity properties which spans from system's opacity verification [START_REF] Hadjicostis | Opacity formulations and verification in discrete event systems[END_REF]) to the synthesis of a controller/scheduler which assures opacity, either through supervision [START_REF] Dubreil | Monitoring and Supervisory Control for Opacity Properties[END_REF]) or enforcement [START_REF] Falcone | Enforcement and validation (at runtime) of various notions of opacity[END_REF]). Recent work has been conducted on quantifying a system's opacity [START_REF] Bérard | Quantifying opacity[END_REF]). Indeed, opacity validation w.r.t. a given secret and intruder is a yes/no question for deterministic models. However, many systems are probabilistic.

In that case, one might be interested in quantifying the possible information leakage from the system. This paper aims to provide a comprehensive and general review of opacity related work considering DES models. After introducing relevant notations in Section 2, we synthesize different notions of opacity used in the literature in Section 3. Section 4 reviews validation methods of various opacity properties. Extensions to probabilistic models are presented in Section 5. Section 6 summarizes decidability and complexity of most approaches surveyed in this paper. Finally, applications of opacity in DES are presented in Section 7 and Section 8 concludes the paper.

PRELIMINARIES

Let E be an alphabet of labels. E * is the set of all finite strings composed of elements of E, including the empty string ε. A language L ⊆ E * is a set of finite-length strings of labels in E. For any string t, |t| denotes the length of t. For a string ω, ω denotes the prefix-closure of ω and is defined as ω = {t ∈ E * |∃s ∈ E * , ts = ω}. The post-string ω/s of ω after s is defined as ω/s = {t ∈ E * , st = ω}. A finite-state automaton G = (X, E, f, X 0 ) is a 4-tuple composed of a finite set of states X = {0, 1, ..., N -1}, a finite set of events E, a partial state transition function f : X × E → X and a set of initial states X 0 . The function f is extended to domain X × E * in the usual manner. The language generated by the system G describes the system's behavior and is defined by

L(G, X 0 ) := {s ∈ E * |∃i ∈ X 0 , f (i, s) is defined}; it is prefix-closed by definition.
Note that in opacity problems, the initial state need not to be known a priori, therefore the set of initial states instead of a single initial state. We also consider partially observable systems. The event set is partitioned into an observable set E o and an unobservable set E uo . Given a string t ∈ E * , its observation is the output of the natural projection function P : E * → E * o , which is recursively defined as P (te) = P (t)P (e) where t ∈ E * and e ∈ E. The projection of an event P (e) = e if e ∈ E o , while P (e) = ε if e ∈ E uo ∪ {ε}. Finally, for a language J ⊆ E * , the inverse projection is defined as P -1 (J) = {t ∈ E * : P (t) ∈ J}.

OPACITY OF DISCRETE-EVENT SYSTEMS

In this section, we formalize different opacity properties of DES. In the general case, the intruder is assumed to have full knowledge of the system structure (plus eventually the system's controller) but has only partial observability over it. Opacity is parameterized by a secret predicate S and by the intruder's observation mapping P over the system's executions. A system is opaque w.r.t. S and P if, for any secret run in S, there is another run not in S which is observably equivalent. In cases of DES models, the secret predicate S can be of two classes: a subset of executions (or parts of executions) or a subset of states. This classifies opacity properties into two families: language-based opacity and state-based opacity.

Language-based opacity -LBO

LBO has been formalized in different ways in the literature. It was first introduced in [START_REF] Badouel | Concurrent secrets[END_REF] and [START_REF] Dubreil | Opacity enforcing control synthesis[END_REF]. LBO (also referred to as trace-based opacity) is defined over a secret behavior described by a language L S ⊆ E * . The system is opaque w.r.t. L S and the projection map P if no execution leads to an estimate that is completely inside the secret behavior. Alternatively, in [START_REF] Lin | Opacity of discrete event systems and its applications[END_REF], LBO is defined over two sublanguages of the system, (L 1 , L 2 ) ⊆ (L(G, X 0 )) 2 . Sublanguage L 1 is opaque w.r.t. L 2 and any observation mapping θ if the intruder confuses every string in L 1 with some strings in L 2 under θ. In most recent papers considering LBO, the latter definition is used except for the observation mapping θ which is generally the natural projection mapping P . Definition 1 (LBO -Strong Opacity): Given a system G = (X, E, f, X 0 ), a projection P , a secret language L S ⊆ L(G, X 0 ), and a non-secret language L N S ⊆ L(G, X 0 ), G is language-based opaque if for every string t ∈ L S , there exists another string t ∈ L N S such that P (t) = P (t ). Equivalently, L S ∈ P -1 [P (L N S )].

The system is language-based opaque if for any string t in the secret language L S , there exists at least one other string t in the non-secret language L N S with the same projection. Therefore, given the observation s = P (t) = P (t ), intruders cannot conclude whether the secret string t or the non-secret string t has occurred. Note that L S and L N S do not need to be prefix-closed in general, nor even regular. Part of the literature refers to Definition 1 as strong opacity. In [START_REF] Lin | Opacity of discrete event systems and its applications[END_REF], a smoother opacity property is also defined.

Definition 2 (LBO -Weak Opacity): Given a system G = (X, E, f, X 0 ), a projection P , a secret language L S ⊆ L(G, X 0 ), and a non-secret language L N S ⊆ L(G, X 0 ), G is weakly opaque if for some string t ∈ L S , there exists another string t ∈ L N S such that P (t) = P (t ). Equivalently, L S ∩ P -1 [P (L N S )] = ∅.

The system is weakly opaque if some strings in L S are confused with some strings in L N S . As a consequence, the property of no opacity can be easily defined. Definition 3 (LBO -No opacity): L S is no opaque w.r.t. L N S and P if L S is not weakly opaque w.r.t. L N S and P . Equivalently, L S ∩ P -1 [P (L N S )] = ∅. Remark 1. It is shown in Ben-Kalefa and [START_REF] Ben-Kalefa | Opaque superlanguages and sublanguages in discrete event systems[END_REF] that LBO properties are closed under union, but may not be closed under intersection. They further discuss how to modify languages to satisfy the strong, weak, and no opacity by investigating sublanguages and superlanguages. Example 1. From Wu and Lafortune (2013) -Consider the system G in Fig. 1(a) with E o = {a, b, c}. It is languagebased opaque when L S = {abd} and L N S = {abc * d, adb} because whenever the intruder sees P (L S ) = {ab}, it is not sure whether string abd or string adb has occurred. However, this system is not language-based opaque if L S = {abcd} and L N S = {adb}; no string in L N S has the same projection as the secret string abcd.

State-based opacity -SBO

The state-based approach for opacity of DES was introduced in [START_REF] Bryans | Modelling opacity using petri nets[END_REF] (for Petri nets models) then extended to FSA in [START_REF] Saboori | Notions of security and opacity in discrete event systems[END_REF]. The state-based approach relates to the intruder ability to infer that the system is or has been in a given "secret" state or set of states. Depending on the nature of the secret set, different opacity properties have been defined.

Current-State Opacity -CSO

CSO was first introduced in [START_REF] Bryans | Modelling opacity using petri nets[END_REF] and called final opacity, in the context of Petri nets. The definition was then adapted to LTS in [START_REF] Bryans | Opacity generalised to transition systems[END_REF], and further developed in finite state automata models in [START_REF] Saboori | Notions of security and opacity in discrete event systems[END_REF]. A system is CSO if the observer can never infer, from its observations, whether the current state of the system is a secret state or not. Definition 4 (CSO): Given a system G = (X, E, f, X 0 ), a projection P , a set of secret states X S ⊆ X, and a set of non-secret states

X N S ⊆ X, G is current-state opaque if ∀i ∈ X 0 and ∀t ∈ L(G, i) such that f (i, t) ∈ X S , ∃j ∈ X 0 , ∃t ∈ L(G, j), such that f (j, t ) ∈ X N S and P (t) = P (t ).
The system is CSO if for every string t that leads to a secret state, there exists another string t leading to a nonsecret state whose projection is the same. As a result, the intruder can never assert with certainty that the system's current state is in X S .

Remark 2. In [START_REF] Bryans | Modelling opacity using petri nets[END_REF], the property of alwaysopacity is also introduced. A system is always-opaque (or total-opaque in [START_REF] Bryans | Opacity generalised to transition systems[END_REF]) over a set of runs if it is CSO for any state visited during these runs. This is equivalent to consider a set of secret states which lies on a prefix-closed language. is current-state opaque because the intruder is always confused between ab and cb when observing b; that is, the intruder cannot tell if the system is in state 3 or 4. However, if E o = {a, b}, CSO does not hold because the intruder is sure that the system is in state 3 when observing ab.

Initial-State Opacity -ISO

ISO property relates to the membership of the system's initial state within a set of secret states. The system is initial-state opaque if the observer is never sure whether the system's initial state was a secret state or not. Definition 5 (ISO): Given a system G = (X, E, f, X 0 ), a projection P , a set of secret initial states X S ⊆ X 0 , and a set of non-secret initial states

X N S ⊆ X 0 , G is initial- state opaque if ∀i ∈ X S and ∀t ∈ L(G, i), ∃j ∈ X N S , ∃t ∈ L(G, j), such that P (t) = P (t ).
The system is ISO if for every string t that originates from a secret state i, there exists another string t originating from a non-secret state j such that t and t are observationally equivalent. Therefore, the intruder can never determine whether the system started from a secret state i or from a non-secret state j.

Example 3. From Wu and Lafortune (2013) -Consider G in Fig. 1(c) with E o = {a, b}, X S = {2}, and X N S = X\X S . G is initial-state opaque because for every string t starting from state 2, there is another string (τ )t starting from state 0 that looks the same. However, ISO does not hold if X S = {0}. Whenever the intruder sees string aa, it is sure that the system originated from state 0; no other initial states can generate strings that look the same as aa.

Remark 3. [START_REF] Hadjicostis | Resolution of initial-state in security applications of des[END_REF] defines resolution of initial state w.r.t. a secret set of states S. It requires that when the system starts from a secret state, the observer will be able to eventually (i.e., after a finite sequence of events/observations) determine with certainty that the system's initial state lied within the set of secret states S. It is worth pointing out at this point that absence of resolution of initial state is necessary but not sufficient for ISO.

K-step opacity

Except for ISO, these opacity properties do not consider the system behavior once it has exited a secret state. A more general problem would be to keep secret the fact the system was in a secret state a few steps ago. This property is called K-step opacity and was first introduced in [START_REF] Saboori | Notions of security and opacity in discrete event systems[END_REF].

Definition 6 (K-step opacity): Given a system G = (X, E, f, X 0 ), a projection P , and a set of secret states X S ∈ X, G is K-step opaque w.r.t. X S and P , or (X S , P, K)-opaque (for

K ≥ 0), if: ∀i ∈ X 0 , ∀t ∈ L(G, i) and ∀t ∈ t such that f (i, t ) ∈ X S and |P (t)/P (t )| ≤ K, ∃j ∈ X 0 , ∃s ∈ L(G, j) and ∃s ∈ s, such that f (j, s ) ∈ X N S , P (s) = P (t) and P (s ) = P (t ).
This definition can be reformulate as in [START_REF] Falcone | Enforcement and validation (at runtime) of various notions of opacity[END_REF]. The system is (X S , P, K)-opaque if for every execution t of G and for every secret execution t prefix of t with an observable difference inferior to K, there exist two executions s and s observationally equivalent respectively to t and t such that s is not a secret execution (i.e., which does not bring the system in a secret state). Example 4. From Falcone and Marchand (2013) -Consider G in Fig. 1(d) with E o = {a, b}, X S = {2}, and X N S = X\X S . G is (X S , P, 1)-opaque. However, it is not (G, P, 2)-opaque as only (τ )aba is a compatible execution with the observation aba. After the last a has occurred, the intruder can deduce that the system was in state 2 two steps ago. Remark 4. K-step opacity is a direct extension of CSO. CSO is equivalent to 0-step opacity [START_REF] Saboori | Notions of security and opacity in discrete event systems[END_REF]). Remark 5. In [START_REF] Falcone | Enforcement and validation (at runtime) of various notions of opacity[END_REF], Definition 6 is referred to as K-step weak opacity. The property of K-step strong opacity holds if the system is K-step weakly opaque and there exists a trace of the system (observably equivalent to the actual execution) which does not cross any secret state over the last K steps.

Infinite-step opacity

In [START_REF] Saboori | Verification and enforcement of statebased notions of opacity in discrete event systems[END_REF], K-step opacity has been further extended to infinite-step opacity. Definition 7 (Infinite-step opacity): Given a system G = (X, E, f, X 0 ), a projection P , and a set of secret states X S ∈ X, G is infinite-step opaque w.r.t. X S and P , or

(X S , P, ∞)-opaque, if: ∀i ∈ X 0 , ∀t ∈ L(G, i) and ∀t ∈ t such that f (i, t ) ∈ X S , ∃j ∈ X 0 , ∃s ∈ L(G, j
) and ∃s ∈ s, such that f (j, s ) ∈ X N S , P (s) = P (t) and P (s ) = P (t ).

A system is infinite-step opaque if, for every execution of the system, after having observed an arbitrary long sequence of events, the intruder cannot infer the system was in a secret state at some point (at any step back in the execution).

Transformations between different opacity properties

The aforementioned opacity properties have strong connections between each another. Several works have addressed the translation between opacity properties. [START_REF] Saboori | Verification and enforcement of statebased notions of opacity in discrete event systems[END_REF] adapts the language-based definition to ISO in order to apply supervisory control (refer to Section 4.2). On the contrary, [START_REF] Cassez | Synthesis of opaque systems with static and dynamic masks[END_REF] describes transformations from LBO to CSO. In [START_REF] Wu | Comparative analysis of related notions of opacity in centralized and coordinated architectures[END_REF], the authors extend these works and provide a full transformation mapping between LBO, CSO, ISO and IFO (initial-and-final state opacity -defined therein). In addition, we already mentioned that K-step opacity is an extension of CSO. CSO is equivalent to 0-step opacity. Finally, in [START_REF] Saboori | Verification and enforcement of statebased notions of opacity in discrete event systems[END_REF], a language-based translation of K-step opacity is suggested: trace-based K-step opacity. It is a special case of K-step opacity which, to the best of our knowledge, has never been used or considered in any other work. It is mentioned here for the sake of completeness.

Distributed opacity

Most opacity-related studies account for a single intruder. However, a few of them consider distributed notions of opacity. Hence, [START_REF] Badouel | Concurrent secrets[END_REF] considers multiple intruders, each of them having its own observation mapping and secret of interest. The system is said to be concurrently opaque if all secrets are safe. A different notion, called joint opacity is presented in [START_REF] Wu | Comparative analysis of related notions of opacity in centralized and coordinated architectures[END_REF] and [START_REF] Wu | Verification and Enforcement of Opacity Security Properties in Discrete Event Systems[END_REF]. In this setting, several intruders collaborate through a coordinator in order to discover the same secret. Finally, Paoli and Lin (2012) considers decentralized framework with and without coordination among agents and formalizes definitions of decentralized opacity. It is shown to be an extension of co-observability, used in traditional supervisory control.

Infinite DES models

Up to a few years ago, opacity-related studies only considered finite-state DES models have been considered in . There are recent work addressing extensions to infinitestate DES. CSO and diagnosability verification are investigated for infinite-state DES modeled by pushdown automata in [START_REF] Kobayashi | Verification of opacity and diagnosability for pushdown systems[END_REF] (therein called pushdown systems), as well as in [START_REF] Chédor | Diagnosis and opacity problems for infinite state systems modeled by recursive tile systems[END_REF], in the more general setting of recursive tile systems.

Relation with other DES and information flow properties

We mentioned in Section 1 that opacity is an information flow property. Relations between several of these properties can be easily drawn. First of all, secrecy is a special case of opacity. A system predicate is secret if the predicate and its complement are simultaneously opaque [START_REF] Badouel | Concurrent secrets[END_REF]). It was shown in [START_REF] Bryans | Opacity generalised to transition systems[END_REF] that anonymity and non-interference problems may be reduced to opacity, using suitable observation functions. Lin (2011) also establishes links between opacity, anonymity and secrecy and shows that observability, diagnosability, and detectability, can be reformulated as opacity as well. The equivalence between opacity and intransitive non-interference is proven in [START_REF] Mullins | Opacity with orwellian observers and intransitive non-interference[END_REF]. Moreover, opacity can be considered in some sense as the dual of diagnosability [START_REF] Zaytoon | Overview of fault diagnosis methods for discrete event systems[END_REF]): for opacity to hold, the secret should not be diagnosable from the viewpoint of the intruder. As a result, several opacity related works use techniques from diagnosis of DES; e.g., [START_REF] Dubreil | Monitoring and Supervisory Control for Opacity Properties[END_REF], [START_REF] Kobayashi | Verification of opacity and diagnosability for pushdown systems[END_REF], [START_REF] Chédor | Diagnosis and opacity problems for infinite state systems modeled by recursive tile systems[END_REF].

ENSURING OPACITY

Traditional opacity formulations from the literature were presented in Section 3. The following question is how does one know that a given system G is opaque w.r.t. a secret and the information available to intruders? Furthermore, if it is not, what can be done to make it opaque? These questions have been continuously addressed and this section aims to synthesize the main approaches available in the literature. There are three main approaches to ensure opacity properties of DES:

• Verification, which roughly consists in model-checking opacity properties; • Supervisory control theory (SCT), which restricts the system's behavior in order to preserve the secret; • Enforcement, which inputs observable events of the systems and outputs (possibly) modified information to the observer, such that the secret is preserved. The main difference between SCT and enforcement is that SCT constrains the system behavior (by restraining its output) by means of a controller while enforcement allows the system free-behavior but post-processes all its output.

Verification of opacity properties

Diagnosis approaches

We mentioned in Section 3.6 that opacity can be considered as the dual property of diagnosability. [START_REF] Dubreil | Monitoring confidentiality by diagnosis techniques[END_REF] investigates the use of techniques from diagnosis of DES [START_REF] Zaytoon | Overview of fault diagnosis methods for discrete event systems[END_REF]) to detect and predict the flow of secret information and construct a monitor that allows an administrator to detect it. In the sequel of the paper, only control and enforcement approached will be further developed. For more details about verification of: (i) LBO, refers to Lin (2011); (ii) SBO, refers to [START_REF] Falcone | Enforcement and validation (at runtime) of various notions of opacity[END_REF] and [START_REF] Hadjicostis | Opacity formulations and verification in discrete event systems[END_REF].

Supervisory control theory -SCT

The potential use of SCT for opacity validation of DES is rather obvious. Several works present construction of minimally restrictive opacity-enforcing supervisory controllers; e.g., [START_REF] Takai | Verification and synthesis for secrecy in discrete-event systems[END_REF], [START_REF] Saboori | Verification and enforcement of statebased notions of opacity in discrete event systems[END_REF], Ben-Kalefa and [START_REF] Lin | Opacity of discrete event systems and its applications[END_REF]. It is shown that optimal control always exists for strong-opacity [START_REF] Dubreil | Monitoring and Supervisory Control for Opacity Properties[END_REF]). In these approaches, the intruder is generally assumed to have full knowledge of the controller's structure in addition to the system's. Moreover, the set of events the intruder can observe is fixed. The applicability of SCT depends on the hypothesis made on the system's model. Given E I , E O and E C being respectively the set of events observable by the intruder, of events observable by the controller and of controllable events respectively, SCT can be directly applied in the following cases [START_REF] Dubreil | Monitoring and Supervisory Control for Opacity Properties[END_REF]

): (1) E C ⊆ E O ⊆ E I ; (2) E I ⊆ E C ⊆ E O .
Furthermore, to deal with the following two cases, slight extensions of SCT have been suggested in Dubreil ( 2010):

(3) E C ⊆ E I ⊆ E O ; (4) E I ⊆ E O and E C ⊆ E O
but without E C and E I being comparable. In [START_REF] Badouel | Concurrent secrets[END_REF], the authors solved the problem of concurrent secrecy (Section 3.4) using SCT. Sufficient conditions to compute an optimal controller preserving all secrets are provided, assuming that the controller has complete knowledge of the system and full control over it. The work of Ben-Kalefa and Lin (2011) considers the verification of both strong and weak opacity. It shows that the solution to the Strong-Opacity Control Problem (SOCP) exists and is unique if all controllable events are observable. However solutions for the Weak-Opacity Control Problem (WOCP) does not exist. This means that if a system is not weakly opaque w.r.t. a given secret language, there exists no controllable and observable sublanguage which can assure weak opacity. In [START_REF] Darondeau | Enforcing opacity of regular predicates on modal transition systems[END_REF], the authors lift the opacity enforcing control problem using SCT from a single finite transition systems to families of finite transition systems specified by modal transition systems [START_REF] Larsen | Modal specifications[END_REF]). The objective is to ensure opacity of a secret predicate on all models of a LTS derived from a given modal transition system. Using SCT is naturally more suited to language-based notions of opacity. However, the verification of initial state opacity has been addressed in [START_REF] Saboori | Verification and enforcement of statebased notions of opacity in discrete event systems[END_REF] by means of reformulation of ISO to LBO, under regular SCT hypothesis (cases ( 1) and ( 2)). Similar work was performed for infinite-step opacity even though it cannot be so easily translated to LBO. It is shown that the approach for ISO can be extended by using a finite bank of supervisors and ensure infinite-step opacity in a minimally restrictive way.

Superlanguages and Sublanguages

In a nutshell, supervisory control resumes to find the supremal sublanguage that ensures opacity. In Ben-Kalefa and [START_REF] Ben-Kalefa | Opaque superlanguages and sublanguages in discrete event systems[END_REF], the authors further investigate language composition and show that opacity properties (with secrets being languages) are closed under union, but may not be closed under intersection. They also demonstrate the following results: (i) the supremal strongly opaque sublanguage exists and is unique; (ii) the minimal strongly opaque superlanguage exists but may not be unique; (iii) the minimal weakly opaque superlanguage exists but may not be unique; and (iv) the supremal not opaque sublanguage exists and is unique.

Enforcement of opacity properties

Opacity enforcement at run-time was recently surveyed in [START_REF] Falcone | Enforcement and validation (at runtime) of various notions of opacity[END_REF]. Enforcement does not restrict the system behavior anymore. Instead, it "hides" some of the system's output events whenever it is necessary. It is a non-intrusive approach, opposite to supervision. There are three main approaches used for opacity enforcement: 1) Deleting occurrences of events from the output; 2) Adding events to the output; 3) Delaying the output.

Deletion of events

Considering a trace observed by the intruder, it may happen that the observation of the next event discloses the secret. A simple idea is to hide the occurrence of this event from observation at run-time (and possibly only this single occurrence) to avoid information flow. Main work achieving this is synthesized in [START_REF] Cassez | Synthesis of opaque systems with static and dynamic masks[END_REF]. In this approach, the enforcer is a device called a mask. This mask restricts the observable outputs of the system either in a static or dynamic fashion. The latter case allows the mask to adapt to the intruder observation mapping (assumed to be dynamic) at each execution step.

Addition of events

Deleting events from the output was still considered as intrusive by some researchers. Even if the internal behavior of the system is no longer restricted (as it is with SCT), its actual output is. To cope with this problem, Wu and Lafortune derived a method which artificially adds output to the set of observable events. This approach is called insertion functions [START_REF] Wu | Verification and Enforcement of Opacity Security Properties in Discrete Event Systems[END_REF]). An insertion function is a monitoring interface at the system's output that changes it by inserting additional ("fake") observable events. Remark 6. Both these approaches were suggested in [START_REF] Ligatti | Edit automata: Enforcement mechanisms for run-time security policies[END_REF], which proposed an enforcement mechanism called edit-automata. This mechanism featured the idea of "suppressing" and "inserting" actions in the current execution of a system but without direct application to information flow and opacity.

Delay of events

The last approach to enforce of opacity properties is to delay emissions of one or several events which would have disclosed the secret, up to the point the disclosure is of no interest anymore, or the system reaches a state in which opacity holds again. This method allows the full system behavior as well, but can only apply to secrets for which time duration is of concern. This approach has been presented in [START_REF] Saboori | Notions of security and opacity in discrete event systems[END_REF] and applied to K-step (weak) opacity. It was later extended in [START_REF] Falcone | Enforcement and validation (at runtime) of various notions of opacity[END_REF] to K-step strong opacity.

QUANTIFYING OPACITY

We presented in Section 3 main formulations of opacity properties which have been considered in the literature. With these definitions, even decidable problems (refer to Section 6) only provide a yes/no answer to the system's opacity. Control (Section 4.2) and enforcement (Section 4.3) can manage to turn a non-opaque system into an opaque one. However, this only accounts for deterministic models, which is known to be a strong limitation in practice. Thus, researchers extended some notions of opacity and tried to quantify it in a probabilistic setting. That is, how can one evaluate the possible information leakage of a system w.r.t. a given secret? Hence, for a given system's execution, we do not ask if there exists an observably equivalent execution, but how many there are, with a probabilistic measure taking into account the likelihood of such executions.

Quantification of language-based opacity

Initial work on quantification of opacity properties was reviewed in [START_REF] Bryans | Towards quantitative analysis of opacity[END_REF]. It provides quantitative measures of LBO in a probalistic setting but it is limited to purely probalistic models, based on labeled Markov chains.

In [START_REF] Bérard | Quantifying opacity[END_REF] two dual notions of probabilistic opacity are introduced: (i) Liberal probabilistic opacity (LPO) measures the probability for an intruder observing a random execution of the system to be able to gain information he can be sure about. This definition provides a measure of how insecure the system is. LP O = 0 ⇔ LBO. (ii) Restrictive probabilistic opacity (RPO) measures the level of certitude in the information acquired by an intruder observing the system. RP O = 0 means the system is never opaque, whichever the running execution. This work was extended very recently in [START_REF] Bérard | Probabilistic opacity for markov decision processes[END_REF] to Markov decision processes with infinite executions. Quantification is performed through the computation of a probabilistic disclosure (PD). It is the probabilistic measure that a run disclosing the secret has been executed. Several problems are addressed, among which: (i) General disclosure: Is P D bigger than a threshold? (ii) Limit disclosure problem: Is P D = 1? (iii) Almost-sure disclosure: does there exists a scheduler such that P D = 1? (iv) Almost-sure opacity: Is P D = 0? Future extensions to this work would include the investigation of disclosure before some given delay, either as a number of steps in the spirit of [START_REF] Saboori | Verification and enforcement of statebased notions of opacity in discrete event systems[END_REF], or for probabilistic timed systems with an explicit time bound.

Quantification of state-based opacity

Saboori first investigated the extension of state-based opacity properties to probabilistic models. Three probabilistic properties are presented in Saboori and Hadjicostis (2014): (i) Step-based almost current-state opacity considers the a priori probability of violating current state opacity following any sequence of events of length K. It requires this probability to lie below a threshold for all possible lengths k = (0, 1, . . . K). It is the extension of K-step opacity. (ii) Almost current-state opacity is step-based almost current-state opacity when there is no consideration regarding the length of the sequence of events, i.e., it considers the a priori probability of violating CSO following any sequence of events. It requires this probability to lie below a threshold. It is the extension of infinite-step opacity. (iii) Probabilistic current-state opacity holds if the maximum increase in the conditional probability that the system's current state lies in the set of secret states (conditioned on a sequence of observations) compared to the case when no observation is available (prior probability) is bounded. These definitions were extended to ISO in [START_REF] Keroglou | Initial state opacity in stochastic des[END_REF] for systems modeled as probabilistic finite automata: (i) Step-based almost initial state opacity captures the a priori probability that the system will generate behavior that violates initial state opacity after a certain number of events. (ii) Almost initial-state opacity captures the a priori probability that the system will eventually generate behavior that violates initial state opacity. Finally, [START_REF] Ibrahim | Secrecy in stochastic discrete event systems[END_REF] extended step-based almost current-state opacity from [START_REF] Saboori | Opacity verification in stochastic discrete event systems[END_REF]. Instead of the disclosure probability being below a threshold at each time step, it considers the probability of reveal-ing the secret over the set of all behaviors. Two properties are introduced : (i) S τ -Secrecy (stochastic-secrecy) holds if the probability of secret disclosure is always below τ . Secrecy ⇔ S 0 -secrecy. (ii) I-S-Secrecy (increasing stochastic-secrecy) hold if, whatever the threshold, there exists a size n of execution length beyond which every trace has a disclosure probability below the threshold.

DECIDABILITY AND COMPLEXITY OF OPACITY PROPERTIES

Opacity is a very general property. As a result, many opacity problems are undecidable. This was demonstrated in [START_REF] Bryans | Opacity generalised to transition systems[END_REF] Much of the work in the DES community is essentially theoretical. This applies to opacity-related papers as well, therefore the shortness of this section. However, there have been a few implementations, which are presented in the following section.

Tools and implementation

Saboori used the Umdes Library to implement the verification method for infinite-step opacity, as described in [START_REF] Saboori | Verification and enforcement of statebased notions of opacity in discrete event systems[END_REF]. Umdes is a library of C routines developed at the University of Michigan (Umdes ( 2009)) for studying DES modeled by finite automata.

CONCLUSIONS AND OPEN PROBLEMS

Over the past ten years, opacity applied to DES has been broadly studied. Almost all opacity problems proven decidable have a known complexity. Future trends are oriented toward infinite-state discrete-event models, eventually coupled with probabilistic transition functions. Moreover, in order to broaden the fields of applications, one could consider opacity validation from another perspective. Starting from a fully observable system and a given secret, which events one should "hide" in order to assure opacity. This approach could provide a pragmatic methodology for people interested in designing opaque systems. To the best of our knowledge, this problem has never been addressed so far and is an interesting perspective.

Fig. 1 .

 1 Fig. 1. From Wu and Lafortune (2013) and Falcone and Marchand (2013) -Systems discussed in Examples 1 to 4.Example 2. From Wu and Lafortune (2013) -Consider G in Fig.1(b) and the sets of secret and non-secret states X S = {3} and X N S = X\X S . If E o = {b}, then G is current-state opaque because the intruder is always confused between ab and cb when observing b; that is, the intruder cannot tell if the system is in state 3 or 4. However, if E o = {a, b}, CSO does not hold because the intruder is sure that the system is in state 3 when observing ab.

  . It remains undecidable for general finite labeled transition systems if you do not restrict the class of observation function. Even for decidable opacity problems, they are computationally complex to solve in general. This sections synthesizes decidability and complexity results demonstrated in the literature. Note that LBO, ISO and CSO -referred to as general opacity problems -have been proven to be reducible into one another in polynomial time[START_REF] Wu | Comparative analysis of related notions of opacity in centralized and coordinated architectures[END_REF],[START_REF] Chédor | Diagnosis and opacity problems for infinite state systems modeled by recursive tile systems[END_REF]). Therefore, these problems have same decidability and complexity (since their own complexity is at least polynomial). Table1synthesizes decidability and complexity results of general opacity problems w.r.t the system's model and the observation mapping. Table2gathers results from opacity quantification approaches. Finally, more specific complexity results are presented in Table3.

	7. APPLICATIONS AND RELATED ISSUES
	Over the literature, some opacity properties and validation
	strategies have been applied and evaluated. The reference
	case of study is known as the Dinning cryptographers
	problem, introduced by Chaum (1988); see e.g., Bérard
	et al. (2010), Wu and Lafortune (2013). It illustrates
	properties of ISO and CSO. Another ISO application is
	presented in Saboori (2011), related to encryption using
	pseudo random generators. The same work also presents
	the problem of sensor network coverage for vehicle track-
	ing. Opacity Issues in Games with Imperfect Information is
	another application considered in Maubert et al. (2011).
	It exhibits relevant opacity verification problems, which
	noticeably generalizes approaches considered in the liter-
	ature for opacity analysis in DES. Finally, the problem of
	Ensuring Privacy in Location-Based Services was studied
	in Wu (2014), using opacity techniques.

Table 1 .

 1 Decidability and complexity results for general opacity problems X\X S is a visible PDA (if X S is a visible PDA)

	System model	Observation mapping	Decidability	Complexity	Reference
	Petri Nets	-	Undecidable	-	Bryans et al. (2008)
	Finite labeled	Static	Undecidable	-	Bryans et al. (2008)
	transition system	m-orwellian	Decidable	PSPACE-complete	Cassez et al. (2012)
	Pushdown automata (PDA) if Recursive tile systems (RTS) -Undecidable / Decidable -Undecidable	-/ 2(1)-EXPTIME -	Kobayashi and Hiraishi (2013) Chédor et al. (2014)
	Weighted RTS (CwRTS)	-	Decidable	2-EXPTIME	Chédor et al. (2014)

Table 2 .

 2 Decidability and complexity results for quantified opacity problems

	Problem	Decidability	Complexity	Reference
	General disclosure	Decidable /
	Limit disclosure opacity	Undecidable with partial	Polynomial / -
	Almost-sure disclosure	observation of the controller		Bérard et al. (2015)
	Almost-sure opacity (perfect observation)	Decidable	Polynomial
	Almost-sure opacity (partial observation)	Decidable for ω-regular secrets	EXPTIME
	Step-based / almost current-state opacity Probabilistic current-state opacity opacity	Decidable Undecidable	PSPACE-hard -	Saboori and Hadjicostis (2014)
	Step-based / almost initial-state opacity	Decidable	-	Keroglou and Hadjicostis (2013)
	Sτ -Secrecy/I-S-Secrecy	Decidable	-	Ibrahim et al. (2014)

Table 3 .

 3 Other complexity resultsFalcone developed a specific toolbox named Takos: a Java Toolbox for the Analysis of K-Opacity of Systems[START_REF] Takos | Takos: A java toolbox for analyzing the k-opacity of systems[END_REF]) to implement the K-step opacity enforcement method presented in Falcone et al. (2014) (using delays). Finally, in[START_REF] Klai | An on-the-fly approach for the verification of opacity in critical systems[END_REF], a symbolic observation graphbased opacity checker has been implemented in C++ using a binary decision diagram package called BuDDy (BuDDy (1998)). Results are compared with the Takos toolbox on the other well known Dinning philosophers problem.

	Problem	Complexity	Order	Reference
	Current-state opacity	PSPACE-complete	O(2 N )
	Initial-state opacity K-Step opacity	PSPACE-complete NP-hard	O(4 N ) O((|E obs | + 1) K × 2 N )	Saboori (2011)
	Infinite-Step opacity	PSPACE-hard	-
	Resolution of initial-state	Polynomial	-	Hadjicostis and Keroglou (2014)
	LBO Strong-opacity	PSPACE-complete	-	Lin (2011)
	LBO Weak-opacity	Polynomial	-	Zhang et al. (2012)
	Static mask synthesis Dynamic mask systhesis	PSPACE-complete EXPTIME lower bound	--	Cassez et al. (2012)