PERMISSIVITE MAXIMALE DU CONTROLE DES SYSTEMES A EVENEMENTS DISCRETS

30/09/2017
Publication e-STA e-STA 2004-3
OAI : oai:www.see.asso.fr:545:2004-3:20051
DOI :

Résumé

PERMISSIVITE MAXIMALE DU CONTROLE  DES SYSTEMES A EVENEMENTS DISCRETS

Métriques

11
4
108.56 Ko
 application/pdf
bitcache://340792563bfd4c1a96094089217b7916b622b9e3

Licence

Creative Commons Aucune (Tous droits réservés)
<resource  xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
                xmlns="http://datacite.org/schema/kernel-4"
                xsi:schemaLocation="http://datacite.org/schema/kernel-4 http://schema.datacite.org/meta/kernel-4/metadata.xsd">
        <identifier identifierType="DOI">10.23723/545:2004-3/20051</identifier><creators><creator><creatorName>Stéphane Riedweg</creatorName></creator><creator><creatorName>Sophie Pinchinat</creatorName></creator></creators><titles>
            <title>PERMISSIVITE MAXIMALE DU CONTROLE  DES SYSTEMES A EVENEMENTS DISCRETS</title></titles>
        <publisher>SEE</publisher>
        <publicationYear>2017</publicationYear>
        <resourceType resourceTypeGeneral="Text">Text</resourceType><dates>
	    <date dateType="Created">Sat 30 Sep 2017</date>
	    <date dateType="Updated">Sat 30 Sep 2017</date>
            <date dateType="Submitted">Tue 13 Nov 2018</date>
	</dates>
        <alternateIdentifiers>
	    <alternateIdentifier alternateIdentifierType="bitstream">340792563bfd4c1a96094089217b7916b622b9e3</alternateIdentifier>
	</alternateIdentifiers>
        <formats>
	    <format>application/pdf</format>
	</formats>
	<version>34068</version>
        <descriptions>
            <description descriptionType="Abstract"></description>
        </descriptions>
    </resource>
.

PERMISSIVITÉ MAXIMALE DU CONTRÔLE DES SYSTÈMES À ÉVÉNEMENTS DISCRETS (MAXIMALLY PERMISSIVE CONTROLLERS IN ALL CONTEXTS) Stéphane Riedweg, Sophie Pinchinat IRISA-INRIA, F-35042, Rennes, France {sriedweg,pinchina}@irisa.fr} Abstract: Nous proposons un formalisme logique pour la spécification des problèmes de contrôle dans laquelle la requête de permissivité maximale des contrôleurs est rendue explicite. L’approche utilise une logique modale avec des quantifications aux propositions ; ce cadre logique offre de plus les algorithmes pour la décision des spécifications et, le cas échéant, pour la synthèse des contrôleurs solutions. We propose a logical formalism for the supervisory control specifications where the maximal permissiveness is explicitly handled, independently of the plant. The approach relies on a modal logic with quantified propositions and additionally provides a powerful machinery for decision and synthesis procedures. Keywords: Supervision, Discrete-event Systems, Permissiveness, Optimal Control, Temporal Logic 1. INTRODUCTION The control theory for discrete event systems was initiated by (Ramadge and Wonham, 1989), fol- lowed by (Thistle and Wonham, 1994) and many others. More recently, temporal logics specifica- tions were considered by (Kupferman et al., 2000) and (Arnold et al., 2003) in order to solve a larger class of problems. Typically, control problems require to find a su- pervision of the plant such that its (operational) behavior meets some desired properties, often called the control objectives. In regard to the ob- jectives, they most often concern standard proper- ties such as admissibility, non-blocking, safety etc. Among those, the fact that the controllers should allow any sound event, hence fulfilling the maxi- mal permissiveness property, is generally taken for granted. As studied in depth by (Ramadge and Wonham, 1989) and others, the theory of regular languages offers clear results on the subject: the existence of a controller implies the existence of a unique maximally permissive one. The proposed algorithms hence synthesize precisely this optimal solution. Unfortunately, this cozy situation does not extends to larger frameworks: for example, the ω-closure assumption is necessary for ω-regular definable objectives (as in (Thistle and Wonham, 1994)), the set of control patterns of (Golaszewski and Ramadge, 1987) must be union-closed, etc. Worse is the case of branching-time logic speci- fications as in (Kupferman et al., 2000; Arnold et al., 2003) where neither the unicity and nor the existence of a maximally permissive controller are guaranteed anymore. For instance, there is no optimal supervision of the plant (a + b)ω which eventually disables event b. Surprisingly, to our knowledge, the maximal permissiveness property has never been approached on its own, like a pos- sible parameter of the supervisory control prob- lems, likely because regular language semantics withstand this subject. In this paper, we propose a logical formalism which allows an explicit handling of maximally permissiveness, in addition to standard supervi- sory control specifications. The approach relies on a logical framework and provides a powerful machinery for decision procedures and effective synthesis. The logic is an extension of the propositional mu-calculus (Kozen, 1983; Arnold and Niwinski, 2001), called the Quantified mu-calculus (qLµ), as originally proposed by (Riedweg and Pinchi- nat, 2003b). The extension feature relies on the use of quantifications over (atomic) propositions. The resulting logic remains decidable as well as its model-checking thanks to its equivalence with infi- nite tree-automata, as already the case for the mu- calculus (see (Emerson and Lei, 1986)). For this reason, effective procedures to synthesis supervi- sory controllers are made possible by computing a finite model of a (infinite) tree-automaton (see also (Riedweg, 2003)). In this paper, we do not aim at explaining the synthesis procedure, but instead we shall take it for granted from (Riedweg and Pinchinat, 2003b). Rather, we demonstrate how the logical formalism elegantly specifies supervisory control problems with an explicit mention of the maximal per- missiveness property inside. Moreover, we make a proof that no other framework known in the literature can reach this expressive power. The paper is organized as follows : Section 2 introduces the logic qLµ. Section 3 explains how control objectives can be specified. Next, Section 4 dedicates to the maximal permissiveness specifi- cation with a proof of correctness. In Section 5, expressiveness issues are discussed, followed by a section of concluding remarks. 2. QUANTIFIED MU-CALCULUS Models are deterministic finite state machines with marked states, called processes in Defini- tion 2, as plants in supervisory control problems normally are. Since branching-time temporal sta- tements will be considered, the natural notion of behavior is the execution tree, namely the (possi- bly infinite) unfolding of the finite state machine. Given that controllers aim at pruning the execu- tion tree, the proposed logic can state in particular the existence of some pruning of the tree that sat- isfies a (mu-calculus definable) desired property. The prunings are simply represented by placing a fresh atomic proposition on the tree to delimit the remaining subtree after pruning: in this way, an edge of the tree where the source node is positively labeled by the proposition whereas the target node is not is meant to be pruned. Technically, an atomic proposition p is added to the unfolding of a process by composing the pro- cess with a particular one, namely a p-labeling process E as in Definition 3; controllers are ac- tually derived from those. To get the tree pruning induced from the proposition done, we prune the labeling process according to Definition 5 to get E(p), before we compose it with the system. So that, as stated by Proposition 7, wondering whether a given pruning/control S × E(p) of the system verifies some desired property α reduces to wonder whether the corresponding p-labeling by S × E is appropriated satisfies some adjustment α∗p of the original property. We assume given a finite set of events Σ = {a, b, . . .}, a set of atomic propositions AP = {p, p0 , c, c0 , . . . }, and a set of variables V ar = {X, Y, . . .}. Definition 1. (Syntax of qLµ) We first recall the syntax of the pure mu-calculus, written Lµ. The set of formulas of Lµ is defined by the following grammar: > | p | X | ¬β | β | β ∨ β0 | µX.β(X) where a ∈ Σ , p ∈ AP and X ∈ V ar. Fix-points formulas µX.β(X) can properly be in- terpreted (in Definition 4) whenever each occur- rence of X in β(X) is under an even number of negation symbols ¬. The quantified mu-calculus, written qLµ, extends Lµ as follows. The set of formulas of qLµ is defined by: ∃p.α | ¬α |α ∨ α0 | β where p ∈ AP and β ∈ Lµ. Freely extending the classical terminology of the mu-calculus to the quantified mu-calculus, we name sentences all the formulas where each oc- currence of a variable X is binded by a fix-point symbol µ. Also, we write ⊥, [a]α, α∧α0 , νX.α(X), and ∀p.α respectively for ¬>, ¬ ¬α, ¬(¬α ∨ ¬α0 ), ¬µX.¬α(¬X) and ¬∃p.¬α, as well as a →, [ ]α and α ⇒ α0 respectively for >, V a∈Σ[a]α and ¬α ∨ α0 . Lastly, for β ∈ Lµ, INV (β) is a notation for νX.[ ]X ∧ β: according to Definition 4 further, it states “from now on, the property β always holds”. Since in general, fixed-point operators and quanti- fiers do not commute, we forbid the use of quantifi- cations inside fixed-point terms, all the more since the formulas will have enough expressive power for control problems specifications, as shown in the next section. The semantics of the quantified mu-calculus (Def- inition 4) relies on models called processes: Definition 2. (Processes) Given a finite set Γ ⊆ AP, a process on Γ is a tuple S = hS, s0 , t, Li, where S is a set of states, s0 ∈ S is the initial state, t : S × Σ → S is a partial function called the transition function and L : S → 2Γ labels states by propositions. A process S is finite if S is finite and it is complete if t(s, a) is defined everywhere. Processes are normally subject to a natural abs- traction according to their execution tree isomor- phism class. Two processes with isomorphic exe- cution trees are called bisimilar. As announced, processes are composed in a syn- chronous manner, as to diminish their behavior: The (synchronous) product of S1 = hS1, s0 1, t1, L1i on Γ1 and S2 = hS2, s0 2, t2, L2i on Γ2 (with disjoint Γ1 and Γ2) is S1 × S2= hS1 × S2, (s0 1, s0 2), t, Li on Γ1 ∪ Γ2 where: (1) t((s1, s2), a) = (s0 1, s0 2) whenever s0 1 = t1(s1, a) and s0 2 = t2(s2, a)), and (2) L(s1, s2) = L1(s1) ∪ L2(s2). Definition 3. (Labeling Processes) Given p ∈ AP, a p-labeling process is a complete process on {p}. We let Labp be the set of p-labeling processes, and we use E, E0 for typical elements. A labeling of S by p, or a p-labeling of S, is a product S × E, where E ∈ Labp. The logic can now be interpreted. Given a process S, a formula α denotes a subset of the states, those which “satisfy” it. The semantics is given by induction over α, hence the need to interpret variable formulas: the standard manner consists in setting a valuation val : V ar → P(S) which defines the subset of states denoted by the for- mulas X ∈ V ar. The pure mu-calculus formulas semantics is standard. Definition 4. (Semantics of qLµ) Given a pro- cess S = hS, s0 , t, Li and val : V ar → P(S), the interpretation of a qLµ-formula α is J α K [val] S ⊆ S defined inductively by: J > K [val] S = S, J p K [val] S = {s ∈ S |p ∈ L(s)}, J X K [val] S = val(X), J ¬α K [val] S = S \ J α K [val] S , J α ∨ α0 K [val] S = J α K [val] S ∪ J α0 K [val] S , J α K [val] S = {s ∈ S |∃s0 , t(s, a) = s0 , s0 ∈ J α K [val] S }, J µX.α(X) K [val] S = \ {V ⊆ S |J α K [val(V/X)] S ⊆ V }, and J∃p.αK [val] S is the set of states s ∈ S, for which there exists E = hE, ε0 , t0 , L0 i ∈ Labp, such that (s, ε0 ) ∈ J α K [val0 ] S×E where val0 (X) ⊆ S × E is val(X) × E, in order to be sound. Since the interpretation of a sentence α is indepen- dent of the valuation val, we simply write J α KS , and we use S |= α whenever the initial state of S belongs to J α KS . To sum up, the assertions “S |= α ∧ α0 ”, “S |= ¬α”, ... respectively mean “S |= α and S |= α0 ”, “not S |= α” (also written “S 6|= α”),... Finally, “S |= ∃p.α” expresses that “there exists a p-labeling process E such that S × E |= α”. Apart from formulas of the form ∃p.α, the seman- tics is the classical mu-calculus definition. Because the mu-calculus is bisimulation invari- ant (formulas have the same truth value when interpreted over bisimilar processes), so is the logic qLµ since the synchronous product which the interpretation of ∃p.α relies on preserves the execution tree isomorphisms. In the rest of this section we establish how to ad- just qLµ formulas according to a fixed proposition when the latter is used to prune the model. We first formalize what the pruning is. Definition 5. (Pruning) Given any process S = hS, s0 , t, Li on Γ and p ∈ Γ, the p-pruning of S is S(p) = hS, s0 , t0 , L0 i on Γ \ {p}, where: (1) for all s ∈ S and a ∈ Σ, t0 (s, a) = t(s, a) if p ∈ L(t(s, a)), otherwise t0 (s, a) is undefined, and (2) L0 (s) = L(s) \ {p}. Definition 6. (Adjustment) For any sentence α ∈ qLµ and for any p ∈ AP, the p-adjustment of α is α∗p ∈ qLµ, inductively defined by (by convention, ∗ has highest priority) : >∗p = >, p0 ∗p = p0 , X∗p = X, (α)∗p =(p ∧ α∗p), (¬α)∗p = ¬α∗p, (α ∨ α0 )∗p = α∗p ∨ α0 ∗p, (µX.α)∗p = µX.α∗p, (∃p.α)∗p = ∃p.α∗p. Definition 5 and 6 together lead to the following fundamental result: Proposition 7. Given a sentence α ∈ qLµ, Γ ⊆ AP, p 6∈ Γ, a process S on Γ and E ∈ Labp, we have: S × (E(p)) |= α if and only if S × E |= α∗p. PROOF. Since, the processes S × (E(p)) and (S × E)(p) are isomorphic, they must satisfy the same formulas in each isomorphic states: J α KS×(E(p)) = J α K(S×E)(p) . An easy proof by induction on α gives the following more general result to conclude: J α K(S×E)(p) = J α∗p KS×E . As shown by Proposition 7, objects of type E(p) indicate what controllers should be like. The soundness of the coming logical specifications can be argued by using two kinds of binary relations between processes. The first kinds are equivalence relations: given a process S, two p-labeling pro- cesses E1 and E2 will be equivalent if they cause the same p-labeling on S. They will be used in the next section. Definition 8. (The ≡S-equivalences) Given a process S and two c-labeling processes E1 and E2, E1 and E2 induce the same c-labeling on S, written E1 ≡S E2, whenever S×E1 and S×E2 are bisimilar. The next binary relation between processes we consider here is the preorder of simulation; its main use further on is to compare more or less permissive behaviors. Definition 9. (Simulation) Given two processes S1 = hS1, s0 1, t1, L1i and S2 = hS2, s0 2, t2, L2i, a simulation of S1 by S2 is a binary relation R ⊆ S1 × S2 such that (s0 1, s0 2) ∈ R and, for any (s1, s2) ∈ R and for any a ∈ Σ, we have: if t1(s1, a) is defined, then t2(s2, a) is defined and (t(s1, a), t2(s2, a)) ∈ R. We write S1  S2 whenever there exists a simula- tion of S1 by S2. Basically, S1  S2 tells that S1 has less executions than S2. One easily checks that  is a preorder. Note that if two processes S1 and S2 are bisimilar, then S1  S2 and S2  S1; the relation  ignoring the atomic propositions, the reciprocal does not hold in general. We let S1 ≺ S2 mean S1  S2 and not S2  S1. We now establish two useful technical lemmas. Lemma 10. For any process S, we have: S  S(p) if and only if S |= [ ]INV (p). PROOF. Let S and S0 be respectively the set of states of S and S(p). Hence S0 ⊆ S. Actually one proves that S  S(p) by check the simulation {(s, s) ∈ S0 × S0 }. Lemma 11. For any p-labeling process E: S  S × E(p) if and only if S × E |= [ ]INV (p). PROOF. By Lemma 10 for S × E, S × E |= [ ]INV (p) if and only if S ×E  (S × E)(p). Since E is complete, S  S ×E and because (S × E)(p) is bisimilar to S × E(p), we obtain S  S × E  (S × E)(p)  S × E(p). By transitivity, S  S × E(p). The reciprocal is easy. 3. BASIC CONTROLLERS The current section shows how basic controllers can be specified in the logic qLµ. The correctness of the specifications is also given. ¿From now on, we assume given Γ ⊆ AP and a process P on Γ which represents a plant: usually, the set of events Σ divides between uncontrollable events Σuc ⊆ Σ on the one hand and controllable events, by complementary, on the other hand. We suppose that the reader is familiar with the no- tion of controller of P for some control objective, as proposed in the reference work of (Ramadge and Wonham, 1989). In our setting, since the control objectives are mu-calculus, and even quan- tified mu-calculus, definable properties, we agree that a controller of P for α ∈ qLµ is a process C with the following: (1) at any time, it allows all uncontrollable events: C |= Admi def = INV ( V u∈Σuc u →), and (2) it achieves the objectives inasmuch as: P × C |= α. In the following, we fix a fresh atomic proposition c and we let the following mu-calculus formula: Controller(c) def = c ∧ INV ((¬c) ⇒ INV(¬c)) ∧ INV(c ⇒ ^ u∈Σuc [u]c) Controller(c) is interpreted on a c-labeling of P, where c represents reachable states under control: a c-labeling of P satisfies Controller(c) when- ever, under control, (1) the initial state is reachable, since c-labeled, (2) successor states of unreachable states are neither reachable, and (3) the successors of reachable states via uncon- trollable events remain reachable. Proposition 12. For any E ∈ Labc s.t. P × E satisfies Controller(c), there exists E0 ∈ Labc which defines a control, in the sense that E0 (c) |= Admi, and s.t. E0 ≡P E. PROOF. Let E = hE, e0 , t, Li ∈ Labc and let us assume that P × E |= Controller(c). Define E0 ∈ Labc by E0 = hE, e0 , t0 , Li where t0 (e, a) =    e if (a ∈ Σuc) and (c ∈ L(e)) and (c / ∈ L(t(e, a))) t(e, a) otherwise By construction, E0 |= c ∧ INV(c ⇒ V u∈Σuc [u]c), hence E0 (c) |= INV ( V u∈Σuc u →). The fact that t0 (e, a) differs from t(e, a) only when a ∈ Σuc, c ∈ L(e) and c / ∈ L(t(e, a)), and since by assumption, P × E |= INV( V u∈Σuc c ⇒ [u]c), we conclude that E0 ≡P E. Propositions 7 and 12 together lead to Theorem 13 below, provided we agree upon the following: Solution(c, α) def = α∗c ∧ Controller(c) Theorem 13. For any α ∈ qLµ, there exists a controller of P for α if and only if P |= ∃c.Solution(c, α) (1) PROOF. The specification above is correct as we show now: assume there is an controller C for α. We will define E ∈ Labc such that E(c) and C are isomorphic: we assign c to each state of C and we complete the resulting process with a sink state. Then P × E satisfies c ∧ INV ((¬c) ⇒ INV (¬c)) and since C is a controller, P ×E satisfies INV (c ⇒ V u∈Σuc [u]c). Since C is a controller for α on P and since E(c) and C are isomorphic, by Proposition 7, P × E satisfies α∗c. Assume now that P satisfies the formula (1). Then there exists E ∈ Labc such that P × E satisfies (α ∗ c) and Controller(c). Since P × E |= Controller(c), there exists (Proposition 12) a labeling process E0 such that E0 ≡P E and E0 (c) is an controller. Moreover, E0 ≡P E and P × E |= α∗c imply P × E0 |= α∗c. Then, take E0 (c) to conclude (by Proposition 7). 4. MAXIMALLY PERMISSIVE CONTROLLERS We first give the definition for Maximal Permis- siveness in a fully natural way. Next we specify it in qLµ, with the arguments for its correctness. Definition 14. (Maximally Permissive Con- troller) Given a formula α ∈ qLµ, we say that the controller C of P for α is maximally permissive if for any other controller C0 of P for α, we do not have S × C ≺ S × C0 . Essentially, since the labelings of the plant can be compared regarding the size of the remaining subtree after pruning, so can the underlying con- trollers, hence our capability to express optimality in the logic: given any two fresh atomic proposi- tions c and c0 , we define the formulas c v c0 and c @ c0 by: c v c0 def = ([ ]INV (c0 ))∗c c @ c0 def = c v c0 ∧ ¬(c0 v c) Formula c v c0 contains a c-adjustment to express that c0 holds all along c-labeled executions. Proposition 15. For all E, E0 ∈ Labc, we have: P × E(c)  P × E0 (c0) iff P × E × E0 |= c v c0 PROOF. Assume that P ×E ×E0 satisfies c v c0 . By Proposition 7, this is equivalent to say that P × E0 × E(c) satisfies [ ]INV (c0 ). Applying now Lemma 11 for P × E(c) leads to P × E(c)  P × E(c) × E0 (c0). Because clearly P × E(c) × E0 (c0)  P × E0 (c0), we conclude by transitivity. Reciprocally, assume P × E(c)  P × E0 (c0) ; by composing both terms with E(c), we obtain P × E(c)  P × E0 (c0) × E(c). Now similar arguments to previous ones can be put forward to conclude. Theorem 16. For any α ∈ qLµ, there exists a maximally permissive controller of P for α if and only if P |= ∃c. Solution(c, α) ∧ ∀c0 .[ c @ c0 ⇒ ¬Solution(c0 , α) ] (2) PROOF. ⇐) By Theorem 13 and because P |= ∃c.Solution(c, α), there exists E ∈ Labc s.t. E(c) is a controller on P for α and P × E |= ∀c0 .c @ c0 ⇒ ¬Solution(c0 , α) (3) Equation 3 with Proposition 15 means for all process E0 ∈ Labc0 , if P × E(c) ≺ P × E0 (c0) then P × E × E0 6|= Solution(c0 , α). Now, be- cause E is complete and since c does not oc- cur in Solution(c0 , α), we can assert: P × E0 6|= Solution(c0 , α). By Theorem 13, E0 (c0) necessar- ily cannot be a controller of P for α. By Defini- tion 9, E(c) is a maximally permissive controller of P for α. ⇒) Assume a maximally permissive controller for α on P, say C. Let us label all states of C by c, and complete the result to get some E ∈ Labc s.t. E(c) equals C. By Theorem 13 (and actually its proof arguments), P × E |= Solution(c, α). Moreover, since C is maximally permissive, for all E0 ∈ Labc0 , we have P × E × E0 |= Solution(c0 , α) ⇒ ¬(c @ c0 ). This concludes. 5. EXPRESSIVENESS We focuse now on Formula (2), where α is a parameter, and we partially answer expresiveness. Recall that Formula (2) represents a new kind of specification which expresses the maximal permis- siveness requirement for controllers. Theorem 17. Let α be formula in Lµ. There cannot exist formulas β and γ in Lµ, or even in qLµ, such that for all plant P and process C: C is a maximally permissive controller of P for α if and only if C |= γ and P × C |= β PROOF. Take α = µX.[ ]X ∨ p, written AFp in the following, as in the classic logic CTL. AFp tells that along any execution, the proposition p will eventually hold. Assume some pair (β, γ) exists. Take P as in Fig.1, where the two events a and b of Σ are both controllable. Clearly, the single state process with an a-loop is a maximally permissive controller for AFp. By assumption, C |= γ and P × C |= β. s0 p a s1 ¬p b P a C s0 p a s1 ¬p b a P0 Fig. 1. P, the controller C and P0 Now define P0 as P plus an a-transition back to the initial state, as drawn in Figure 1. Because P × C and P0 × C are bisimilar, we also have P0 × C |= β. Since by assumption C |= γ, C is a solution of (β, γ) and yet C is not a maximally permissive controller of P0 for AFp: indeed, C cuts the transition from s0 to s1 of P0 , which should be kept. This leads to a contradiction. As a consequence of Theorem 17, while with the logic qLµ the maximal permissiveness is expressed in a uniform manner, its statement in the frame- work of (Arnold et al., 2003) must be designed according to the plant, hence an ad hoc solution. 6. CONCLUSION The presented work proposes a logical frame- work for the specification of control problems, which additionally allows to perform synthesis. The key ideas are built on an extension of the propositional mu-calculus using quantified atomic propositions. The resulting is expressive enough to specify maximally permissive controllers for any mu-calculus definable control objective, indepen- dently of the plant. Moreover, we showed that other existing logical frameworks, like (Arnold et al., 2003), cannot express maximal permissiveness on its own, but would rather need a system- dependent specification. For the sake of simplicity, we have only proposed here a fully observational setting, but the results still hold in the more general case of partial observation, as explained in (Riedweg and Pinchinat, 2003a), as well in a forthcoming paper. As explained in the paper, the maximal permis- siveness property is definitely a strong argument in favor of our approach and demonstrates a fun- damental feature of the quantified logic frame- work. Indeed, contrary to other approaches, it is possible to express properties outside the re- maining system after the synchronous product of the plant with the controller. As a consequence, many other kinds of optimality criteria can be considered, such as the unicity of a solution, but also, “contextual” properties: one can specify that deadlocks are forbidden unless they already exist in the plant, priority between events, fairness of the control, forcing events, etc. 7. ACKNOWLEDGMENTS A first version of this paper was published at IFAC Workshop on Discrete Event Systems, WODES’04, 22-24 September 2004. The authors would like to thank Peyman Gohari for helpful comments. REFERENCES Arnold, A., A. Vincent and I. Walukiewicz (2003). Games for synthesis of controllers with par- tial observation. Theoretical Computer Sci- ence 1(303), 7–34. Arnold, A. and D. Niwinski (2001). Rudiments of Mu-calculus. North-Holland. Emerson, E. A. and C. Lei (1986). Efficient mod- el checking in fragments of the proposition- al mu-calculus. In: Proc. 1st IEEE Symp. Logic in Computer Science, Cambridge, Mas- sachussets.. pp. 267–278. Golaszewski, C. H. and P. J. Ramadge (1987). Control of discrete event systems with forced events. In: Proc. of 26th Conf. Decision and Control. Los Angeles, CA, USA. pp. 247–251. Kozen, D. (1983). Results on the proposition- al µ-calculus. Theoretical Computer Science 27(3), 333–354. Kupferman, O., P. Madhusudan, P. S. Thiagara- jan and M. Y. Vardi (2000). Open systems in reactive environments: Control and synthe- sis. In: Proc. 11th Int. Conf. on Concurrency Theory. Vol. 1877 of LNCS. Springer-Verlag. pp. 92–107. Ramadge, P. J. and W. M. Wonham (1989). The control of discrete event systems. In: Proc. of the IEEE. Vol. 77(1). pp. 81–98. Riedweg, S. (2003). Logiques pour le Contrôle d’Automatismes Discrets. PhD thesis. Uni- versité de Rennes I. Riedweg, S. and S Pinchinat (2003a). Quantified loop mu-calculus for control synthesis under partial observation. Technical Report R4949. Irisa. Riedweg, S. and S. Pinchinat (2003b). Quantified mu-calculus for control synthesis. In: Math- ematical Foundations of Computer Science. Vol. 2747 of LNCS. pp. 642–651. Thistle, J.G. and W. M. Wonham (1994). Control of infinite behavior of finite automata. SIAM Control and Optimization 32(4), 1075–1097.