André Arnold

Igor Walukiewicz

Nondeterministic controllers of nondeterministic processes

published or not. The documents may come   L'archive ouverte pluridisciplinaire

Introduction

At the end of the eighties, Ramadge and Wonham introduced the theory of control of discrete event systems (see the survey [START_REF] Ramadge | The control of discrete event systems[END_REF] and the books [START_REF] Kumar | Modeling and control of logical discrete event systems[END_REF] and [START_REF] Cassandras | Introduction to discrete event systems[END_REF]). In this theory a process (also called a plant) is a deterministic non-complete finite state automaton over an alphabet A of events, which defines all possible sequential behaviours of the process. The goal is to find for a given plant another process, called controller, such that a synchronous product of the plant and the controller satisfies desired properties. The usual properties considered are for instance, that some dangerous states are never reachable, or that one can always go back to the initial state of the plant. In decentralized control one looks for a fixed number of controllers that control the plant simultaneously.

In the setting described above one assumes that both a plant and controllers are deterministic automata. This paper examines what changes when assumption on determinism is dropped. It is shown that nondeterminism in a plant can be handled at no cost, while nondeterminism in controllers may lead to undecidability in the case of decentralized control.

The synthesis problem would be interesting neither form theoretical nor from practical point of view if there were no additional restrictions on controllers. In the most standard form a restriction is determined by two subsets A unc and A uobs of the alphabet A with the associated requirement that:

(C) For any state q of the controller, and for any uncontrollable event a, there is a transition from q labelled by a.

(O) For any state q of the controller, and for any unobservable event a, if there is a transition from q labelled by a then this transition is a loop over q.

In other words, a controller must react to any uncontrollable event and cannot detect the occurrence of an unobservable event.

In [START_REF] Arnold | Games for synthesis of controllers with partial observation[END_REF] an extension of this setting was proposed that handles specifications expressed in the mu-calculus, or rather in its extension called modal loop mu-calculus. This allowed a more general formulation of the synthesis problem:

(CC) Given a plant P and two formulas α and β, does there exist a controller R satisfying β such that P × R satisfies α?

With formulas α and β one can express properties (C) and (O) but also much more, as for example that an action becomes unobservable after a failure has occurred, or that always one of two actions is controllable but never both at the same time.

The problem (CC) can be solved thanks to the division operation [START_REF] Arnold | Games for synthesis of controllers with partial observation[END_REF]. For a process P and a formula α there is a formula α/P such that: R α/P iff P × R α. This way a process R is a solution to (CC) if and only if R (α/P ) ∧ β. As (α/P ) ∧ β is a formula of the modal loop mu-calculus the synthesis problem reduces to the constructive satisfiability problem: construct a model for a formula whenever a model exists. The latter is decidable and a witnessing model, which is a controller, can be constructed.

Ramadge and Wonham have considered also the problem of synthesis of decentralized controllers: a plant can be supervised by several independent controllers (instead of only one). But each controller has its own set of controllable and observable events. Hence the decentralized control problem is to find R 1 , . . . , R n such that the supervised system P × R 1 × • • • × R n satisfies the specification S and for each i, R i satisfies (C i ) and (O i ). More generally, in our setting, a decentralized control problem is:

(DC) Given a plant P and modal-loop mu-calculus formulas α, β1, . . . ,βn, do there exist controllers Ri satisfying βi (for i = 1, . . . , n) such that P × R1 × • • • × Rn satisfies α?

In [START_REF] Arnold | Games for synthesis of controllers with partial observation[END_REF] it is shown how to solve a decentralized control problem when at most one of the formulas α i restrains visibility of a controller. If one allows to put visibility restrictions on at least two controllers then the existence of a solution to the problem is undecidable.

Till now, all the constructions assumed that processes are deterministic automata. This may be a limiting assumption if, for example, a plant is a model of a continuous system. In this case a continuous domain of values must be sampled to a discrete one. Hence, the same measurement can correspond to different values that may have different effect on the behaviour of the plant. For similar reasons, the result of actions of controllers may be also not completely determined.

In this paper, we show that in the case of centralized synthesis the approach via division operation still works. We do this by generalizing the division operation described above to a division by a nondeterministic process. This shows that nondeterminism in a plant can be handled at no cost. Next, we study decidability of (DC) problem. Thanks to the division, allowing nondeterministic plant does not make the problem more complex. By contrast, if we allow at least two controllers to be nondeterministic, then the problem becomes undecidable even for formulas in the standard mu-calculus. We study also the case when at most one of the controllers can be nondeterministic, obtaining a full characterisation of decidability of (DC) problem.

The paper is organized as follows. In the next section we introduce processes and automata on processes. This will be a rather rich version of alternating automata that has not only loop testing, a , but also indistinguishability testing ↓↓ a,b . Intuitively, the first constraint will be used to say that a controller cannot observe a, and the second that it cannot make a difference between a and b. These kinds of automata were introduced in [START_REF] Arnold | Games for synthesis of controllers with partial observation[END_REF], and ↓↓ a,b test was added in [START_REF] Briand | Contrôle avec événements indiscernables et inobservables[END_REF]. In Section 3 we give basic properties of these automata, like closure under boolean operations and decidability of emptiness. Section 4 presents an operation of division of an automaton by a process. This operation is used in the following section to solve centralized synthesis problem and to eliminate the plant from formalization of decentralized synthesis problem. Main results of the paper are given in this section. The proofs of decidability and undecidability results announced here are given in Sections 6 and 7 respectively.

Processes and automata

Processes

Let A be a finite alphabet of actions. A process is a finite graph with a distinguished node and with edges labelled by actions:

P = S, A, s 0 ∈ S, e ⊆ S × A × S
We will usually refer to nodes as states. We will write s a → s ′ instead of (s, a, s ′ ) ∈ e, and will say that there is a transition labelled a form a state s to a state s ′ . A process is deterministic if e is a partial function e : S × A → S. We will write out P (s, a) for the set of states reachable from s by a transition labelled a:

out P (s, a) = {s ′ : s a → s ′ }.
A product of two processes over the same alphabet is standard P × R = S P × S R , A, (s 0 P , s 0 R ), e P ×R where ((s P , s R ), a, (s ′ P , s ′ R )) ∈ e P ×R if (s P , a, s ′ P ) ∈ e P and (s R , a, s ′ R ) ∈ e R .

Games

As our specification language we will use a rich variant of alternating automata that we will introduce in the next subsection. It will be very convenient to describe its semantics in terms of games, so we recall necessary definitions here.

A game G is a tuple

V E , V A , T ⊆ (V E ∪ V A ) 2 , Acc ⊆ V ω
where Acc is a set defining the winning condition, and V E ∪ V A , T is a graph with the vertices partitioned into those of Eve and those of Adam. We say that a

vertex v ′ is a successor of a vertex v if T (v, v ′ ) holds.
A play between Eve and Adam from some vertex v ∈ V = V E ∪ V A proceeds as follows: if v ∈ V E then Eve makes a choice of a successor, otherwise Adam chooses a successor; from this successor the same rule applies and the play goes on forever unless one of the parties cannot make a move. The player who cannot make a move looses. The result of an infinite play is an infinite path v 0 v 1 v 2 . . . This path is winning for Eve if it belongs to Acc. Otherwise Adam is the winner.

A strategy σ for Eve is a function assigning to every sequence of vertices v ending in a vertex v from V E a vertex σ( v) which is a successor of v.

A play respecting σ is a sequence v 0 v 1 . . . such that v i+1 = σ(v i ) for all i with v i ∈ V E . The strategy σ is winning for Eve from a vertex v iff all the plays starting in v and respecting σ are winning. A vertex is winning if there exists a strategy winning from it. The strategies for Adam are defined similarly. A strategy is positional if it does not depend on the sequence of vertices that were played till now, but only on the present vertex. So such a strategy can be represented as a function σ : V E → V and identified with a choice of edges in the graph of the game.

In this paper the winning conditions Acc ⊆ V ω will be regular conditions. That is conditions defined in monadic second-order logic on sequences. An important special case is a parity condition. It is a condition determined by a function Ω : V → {0, . . . , d} in the following way:

Acc = {v 0 v 1 . . . ∈ V ω : lim sup i→∞ Ω(v i ) is even}
Hence, in this case, each position is assigned a natural number and we require that the largest among those appearing infinitely often is even. This condition was discovered by Mostowski [START_REF] Mostowski | Regular expressions for infinite trees and a standard form of automata[END_REF] and is the most useful form of regular conditions. It guarantees existence of positional strategies [START_REF] Emerson | Tree automata, mu-calculus and determinacy[END_REF][START_REF] Mostowski | Games with forbidden positions[END_REF][START_REF] Mcnaughton | Infinite games played on finite graphs[END_REF]. It is closed by negation (the negation of a parity condition is a parity condition). It is universal in the sense that every game with a regular condition can be reduced to a game with a parity condition [START_REF] Mostowski | Regular expressions for infinite trees and a standard form of automata[END_REF].

The main results about games that we need are summarized in the following theorem.

Theorem 2.1 ( [START_REF] Martin | Borel determinacy[END_REF][START_REF] Emerson | Tree automata, mu-calculus and determinacy[END_REF][START_REF] Mostowski | Games with forbidden positions[END_REF]). Every game with regular winning conditions is determined, i.e., every vertex is winning for one of the players. It is algorithmically decidable who is a winner from a given vertex in a finite game. In a parity game a player has a positional strategy winning from each of his winning vertices.

Automata

We will need automata that work on graphs. These automata should cope with multiple outgoing edges with the same label. Moreover, we would like to equip them with tests of some simple structural graph properties. They will be able to check that an edge on a given letter is a self-loop or that the edges on two different letters lead to the same states. To incorporate all these tests it will be simpler to define automata which use a kind of modal formulas over the set of states in a process. Thus we start with defining these formulas.

Let A be an alphabet and let Q be a finite set. The set of modal formulas over A and Q, denoted F(A, Q), is the smallest set closed under the following rules:

• tt, ff , q, a , a , ↓↓ a.b ↓↓ a,b are formulas, for any q ∈ Q and a, b ∈ A.

• α ∨ β and α ∧ β are formulas for all α, β ∈ F(A, Q).

• a α and [a]α are formulas for all α ∈ F(A, Q) and a ∈ A.

An automaton over a set of actions A is a tuple:

A = Q, A, q 0 ∈ Q, δ : Q → F(A, Q), Acc ⊆ Q ω
where Q is a finite set of states, A is a finite alphabet, and Acc is an accepting condition that is a regular set of infinite sequences of states.

The acceptance of a process P by an automaton A is defined in terms of strategies in a game G(P, A) that we describe now. Let F A be the smallest set of formulas closed under taking subformulas, and containing all formulas in the range of δ together with tt and ff . We have

G(P, A) = V E , V A , T, Acc G where • V E = S × F A
E , and F A E is the set of formulas form F A of one of the forms: ff , a , ↓↓ a,b , q, a α, α ∨ β.

• V A = S × F A -V E .
• From (s, tt) and (s, ff ) no move is possible.

• From (s, a ) there is a move to (s, tt) if out P (s, a) = {s} and to (s, ff ) otherwise.

• From (s, ↓↓ a,b ) there is a move to (s, tt) if out P (s, a) = out P (s, b) and to (s, ff ) otherwise.

• Similarly for (s, a ) and (s, ↓↓ a,b ) but with roles of (s, tt) and (s, ff ) interchanged.

• From (s, α ∧ β) as well as from (s, α ∨ β) there are moves to (s, α) and to (s, β).

• From (s, a α) and from (s, [a]α) there are moves to (t, α) for every t ∈ out(s, a).

• Finally, from (s, q) there is a move to (s, δ(q)).

• The winning condition Acc G contains sequences such that when looking only at the elements of Q appearing in the sequence we obtain an element of Acc.

We say that P satisfies A, in symbols P A, if Eve has a winning strategy in G(P, A) from (s 0 , q 0 ), which is the pair consisting from the initial states of P and A, respectively. As our automata are very close to formulas we prefer to talk about satisfiability instead of acceptance. We will still use some automata terminology though. For example, the language recognized by an automaton A will be the class of processes that satisfy A.

Our automata are a variant of alternating automata. In particular the formulas used in the transition function are "closed" under disjunction and conjunction. Using standard constructions on alternating automata we get. A simple automaton is nothing else but a µ-calculus formula in a different presentation. Using the results on the µ-calculus we have.

Theorem 2.4 ([4, 14]). It is decidable if for a given simple automaton A

there is a process P such that P A. Similarly, if we require P to be deterministic. In both cases a process P can be constructed if the answer is positive.

Theorem 2.5 ( [START_REF] Niwiński | Fixed points vs. infinite generation[END_REF][START_REF] Janin | On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic[END_REF]). Over deterministic systems which are trees, the expressive power of simple automata is equivalent to that of monadic secondorder logic. Over all processes: a property is expressible by a simple automaton iff it is expressible in monadic second-order logic and bisimulation invariant.

Satisfiability

The basic question one can ask about our automata model is whether for a given automaton A there is a process that satisfies it. From the previous section we know that there is an algorithm answering this question in the case of simple automata. We will now reduce the general case to that of simple automata. For this, we will encode information about loops and parallel tests in additional transitions. This way for a process P we will define a process Code(P ). It will then turn out that behaviour of an automaton over P can be simulated by a behaviour of a simple automaton over Code(P ).

A type of a state s of a process P is:

type(s) = { a : out(s, a) = {s}} ∪ {↓↓ a,b : out(s, a) = out(s, b)}
Let Types(A) be the set of all possible types over an alphabet A.

Note that if τ ∈ Types(A) and ↓↓ a,b ∈ τ then a ∈ τ implies b ∈ τ , and also ↓↓ a,c ∈ τ implies ↓↓ b,c ∈ τ .

Fix an alphabet A and some arbitrary ordering < A on it. For a process P over an alphabet A we define its code Code(P ) over an alphabet A ∪ Types(A). For each state s of P we do the following:

• Add a transition on action τ = type(s), the target of this transition is some arbitrary fixed state (say, the initial state).

• Remove transitions on a if a ∈ type(s) or ↓↓ a,b ∈ type(s) for some b < A a.

Let C be a simple automaton expressing the conditions:

• For every state there is transition on exactly one letter from Types(A).

• For every a ∈ A, there is no transition on a if a ∈ τ or ↓↓ a,b ∈ τ for some b < A a.

Lemma 3.1. The process Code(P ) satisfies C and has no loops

s a → s Moreover, Code(P ) is deterministic if P is. If R is a process satisfying C without loops s a → s then there is a unique process P such that Code(P ) is isomorphic to R.

The next step is to transform an automaton over an alphabet A into an "equivalent" automaton over an alphabet A∪Types(A). Take an automaton

A = Q, A, q 0 , δ : Q → F(A, Q), Acc ⊆ Q ω
We first define transformation, Code(α), on formulas from F(A, Q):

• Code(q) = q. • Code( a ) = { τ tt : τ ∈ Types(A), a ∈ τ }. Similarly for ↓↓ a,b . • Code( a ) = { τ tt : τ ∈ Types(A), a ∈ τ }. Similarly for ↓↓ a,b . • Code(α ∨ β) = Code(α) ∨ Code(β)
, and similarly for the conjunction. Then automaton Code(A) is the same as A except for the transition function δ Code . We put δ Code (q) = Code(δ(q)). The following lemma follows directly from definitions.

• Code( a α) = { τ tt ∧ Code( a α, τ ) : τ ∈ Types(A)} where Code( a α, τ ) = Code(α) if a ∈ τ a Code(α) ∨ { b Code(α) :↓↓ a,b ∈ τ } otherwise • Code([a]α) = { τ tt ∧ Code([a]α, τ ) : τ ∈ Types(A)};
Lemma 3.2. For every process P and automaton A over an alphabet A:

P A iff Code(P ) Code(A)
Observe that Code(A) is simple, i.e., does not use neither nor ↓↓ constraints. Using Code(A) we can transfer results from simple automata to the general case.

Theorem 3.3. It is decidable if for a given automaton A there exist a process P such that P A. Similarly, if we ask for P being deterministic. In both cases, if the answer is positive then a process satisfying A can be constructed.

Proof. Consider Code(A).

As Code(A) ∧ C is a simple automaton, by Theorem 2.4 we can test if there exists a process R Code(A) ∧ C. Unfolding the loops of R we can construct a process R ′ without loops such that R ′ Code(A)∧C. Lemma 3.1 gives us a process P such that Code(P ) is isomorphic to R ′ , hence Code(P ) Code(A). By Lemma 3.2 we have P A. This construction works also when we require P to be deterministic.

Conversely, if P is a (deterministic) process that satisfies A then the (deterministic) process Code(P ) satisfies Code(A), by Lemma 3.2, and C, by Lemma 3.1.

q.e.d.

Quotient for extended automata

In this section we present an operation that will permit us to reduce synthesis problems to the satisfiability problems. Consider an extended automaton A = Q, A, q 0 , δ, Acc and a process P = S, A, s 0 , e over a common alphabet A. Our goal is to construct an automaton A/P such that for every process R: R A/P if and only if P × R A

We first define a division α/s for α a formula from F(A, Q), and s a state of P . The result is a formula from F(A, Q × S): q/s = (q, s)

(α ∨ β)/s = α/s ∨ β/s (α ∧ β)/s = α/s ∧ β/s ( a α)/s = a {α/s ′ : s a → s ′ } ([a]α)/s = [a] {α/s ′ : s a → s ′ } Now A/P = Q × S, A, (q 0 , s 0 ), δ / : Q × S → F(Q × S), Ω
where δ / (q, s) = δ(q)/s; recall that δ(q) ∈ F(Q), so δ(q)/s ∈ F (Q × S).

Theorem 4.1. Let A be an alphabet. For every extended automaton A and every process P , both over A, there is an automaton A/P such that for every process R over A: R A/P if and only if P × R A Proof. Fix a process R. We examine the games G × = G(P × R, A) and G / = G(R, A/P ). We want to show how a move of one of the players in G × from a position of the form ((s, r), α) can be mimicked by, possibly several, moves of the same player in G / from (r, α/s). For example, suppose that a position has the form ((s, r), α ∨ β) and that Eve chooses ((s, r), α). From a position (r, (α ∨ β)/s)) this move can be mimicked by going to (r, α/s). Slightly more complicated is the case of ((s, r), a α). In this case Eve can choose ((s ′ , r ′ ), α) for s a → s ′ and r a → r ′ . From (r, ( a α)/s) this move can be mimicked by first choosing (r ′ , {α/s ′′ : s a → s ′′ }) and then (r ′ , α/s ′ ); this is possible as ( a α)/s = a {α/s ′′ : s a → s ′′ }. The cases of α ∧ β and [a]α are dual.

These observations show that any play in G × can be mimicked in G / , so the same player has a winning strategy from ((s 0 , r 0 ), q 0 ) in G × and from (r 0 , (q 0 , s 0 )) in G / .

q.e.d.

Solving controller synthesis problems

Equipped with the operation of division we can reduce the control problem to the satisfiability problem.

Centralized control

As we have argued in the introduction, the centralized controller synthesis problem can be formulated as:

For a given process P and two automata A, B over an alphabet A, find R such that: This means that solving a synthesis problem amounts to checking emptiness of the automaton (A/P )∧B. Theorem 2.1 then states that this problem is decidable both for the general, nondeterministic, case as well as for the case of deterministic processes.

P × R A and

Decentralized control

The decentralized controller synthesis problem is:

For a given process P and automata A, B1, . . . , Bn over an alphabet A, find R1, . . . , Rn such that:

P × R1 × • • • × Rn A and Ri Bi for all i = 1, . . . , n
Thanks to Theorem 4.1 we can take A/P and remove P from the left hand side. This shows that we can as well consider the following simpler formulation of the problem where P is not mentioned.

For a given automata A, B1, . . . , Bn over an alphabet A, find R1, . . . , Rn such that:

R1 × • • • × Rn A and Ri Bi for all i = 1, . . . , n
This last problem was studied in [START_REF] Arnold | Games for synthesis of controllers with partial observation[END_REF][START_REF] Briand | Contrôle avec événements indiscernables et inobservables[END_REF] in the case when R 1 , . . . , R n are required to be deterministic. In particular the problem was shown decidable when all but one B i are simple. We will see later that the same problem is undecidable in the nondeterministic case. To better understand the decidable/undecidable borderline we propose a classification of decentralized synthesis problems with respect to restrictions on R 1 ,. . . , R n .

A pair (pt, st) ⊆ {det, nondet} × {simple, f ull} describes requirements on processes and specifications. A choice of a number of components and a type for each component determines a distributed control problem: DS(n, (pt1, st1), . . . , (ptn, stn)): Given automata A, B1,. . . ,Bn such that Bi is simple if sti = simple, find R1, . . . , Rn such that Ri is deterministic if pti = det, satisfying P × R1 × • • • × Rn A and Ri Bi for all i = 1, . . . , n.

The following theorem gives a complete classification of these problems with respect to decidability.

Theorem 5.2. The problem DS(A, (pt 1 , st 1 ), . . . , (pt n , st n )) is decidable iff

• There is at most one i such that st i = f ull.

• There is at most one j such that pt j = nondet and moreover j = i.

The proof of this theorem will be given in the two following sections. In terms of the decentralized control problem formulated at the beginning of the section, we get that the problem is decidable if at most one of B i is not simple and at most one R j is allowed to be nondeterministic (moreover j = i). Probably the most important difference with respect to the deterministic case considered in [START_REF] Arnold | Games for synthesis of controllers with partial observation[END_REF] is that now P can be nondeterministic.

The decidable sub-case of decentralized control

We would like to show the right to left implication of Theorem 5.2.

The solution in the case when all R 1 , . . . , R n are required to be deterministic uses the following extension of the quotient operation : Theorem 6.1 ( [START_REF] Arnold | Games for synthesis of controllers with partial observation[END_REF]). For every automaton A and every simple automaton B there is an automaton A/B such that for every deterministic process P :

P A/B iff ∃R. R deterministic, R B, and P × R A
Here we show existence of a variant of this division operation. The difference is that the existentially quantified process R need not be deterministic. Theorem 6.2. For every automaton A and every simple automaton B, there is an automaton A/ ndet B such that for every deterministic process P :

P A/ ndet B iff ∃R. R B and P × R A
Before giving the proof of this theorem let us show how it can be used to prove right to left direction of Theorem 5.2.

Let us assume that st n = f ull and pt 1 = nondet. First, we find a deterministic process R n (A/ ndet B 1 /B 2 . . . /B n-1 ) ∧ B n . If none exists then the problem has no solutions. Otherwise, by Theorem 3.3, we can construct required R n . Equipped with it we can find a deterministic process R n-1 (A/R n / ndet B 1 /B 2 . . . /B n-2 ) ∧ B n-1 . This construction can be repeated, giving R n-1 . . . , until we construct a deterministic R 2 (A/R n /R n-1 / . . . /R 3 / ndet B 1 ) ∧ B 2 . Once R 2 , . . . , R n are fixed, we can look for, this time nondeterministic, process R 1 (A/R n /R n-1 / . . . /R 2 ) ∧ B 1 . By the above two theorems on division operations, R 1 , . . . , R n is a solution to the problem. The theorems also guarantee that all solutions to the problem can be obtained this way.

The rest of this section presents the proof of Theorem 6.2. We want to transform the property of a deterministic process P :

∃R. R B and P × R A (1.1)
to an equivalent formulation that is expressible by an automaton. This will be our automaton A/B. The first step is to introduce well-typed processes and restrict our problem only to this kind of processes. Given a process P over an alphabet A, a well-typed process, wt(P ), is a process over the alphabet A ∪ P(A) that is obtained form P by adding a new state ⊤, and precisely one action from each state as follows: to a state s of P we add a transition to ⊤ on out P (s) ∈ P(A), where out P (s) is the set of actions possible form s, out P (s) = {b : out P (s, b) = ∅}. It should be clear that there is an automaton checking if a processes is of the form wt(P ). It is also easy, given an automaton C, to construct an automaton C ′ such that for all processes P over an alphabet A wt(P ) C iff P C ′ This means that in the following we can consider only processes of the form wt(P ). We call these processes well-typed.

The restriction to well-typed processes is important for the first simplification step. We want to find an automaton D such that (1.1) is equivalent to

∃R. P × R D (1.2)
For this we construct an automaton B ′ and show that (1.1) is equivalent to

∃R ′ . P × R ′ B ′ ∧ P × R ′ A.
Having this, we can just take B ′ ∧ A for D. We call a process over A ∪ P(A) typed if every state has precisely one transition on a letter from P(A). Compared with well-typed processes, we do not put any restriction what a γ is. We also define a safe extension of a typed process R to be a process obtained form R by adding some states and transitions provided that if (s, b, t) is an added transition and s is a state from R then t must be an added state and b must not appear in the label of the unique action from P(A) possible from s. With these definitions we can say what the automation B ′ is. We want B ′ to accept a process if it is typed, and moreover it has a safe extension that is accepted by B. It remains to argue that B ′ has the desired property. For one direction suppose that we have R ′ with P × R ′ B ′ and P × R ′ A ′ . If P × R ′ B ′ then, by the definition of B ′ , there is a safe extension R of P × R ′ that satisfies B. By the definition of the safe extension, and the fact that P is well-typed we have that P × R ′ = P × R. So P × R A. Now consider the opposite direction. Take R which is assumed to exists and add to R a state ⊤ as well as transitions to ⊤ from each state of R on every letter from P(A). As B does not talk about the actions from P(A) then R ′ B. We have P × R ′ B ′ because P × R ′ is typed and R ′ is a safe extension of P × R ′ . We also have P × R ′ A as A does not talk about actions from P(A).

The above argument reduces our task to the problem of expressing by an automaton the property (1.2) of well-typed P . First, we will consider a simpler property where the branching of the process R we quantify over is bounded by k, i.e. for every s ∈ R and a, |out(s, a)| ≤ k.

∃R. branching(R) ≤ k and P

× R D (1.3)
This formulation will allow us to use the division operation for the deterministic case, i.e, Theorem 6.1. Consider processes over an alphabet /tt where tt is an automaton accepting all the processes over A [k] . By Theorem 6.1 we have

A [k] = A × {1, . . . ,
P ′ D [k] /tt iff ∃R ′ . P ′ × R ′ D [k] ;
Here, all the processes are over A [k] . For a deterministic process P over A we can define P [k] to be a deterministic process over A [k] where there is an edge (b, i), for i = 1, . . . , k, between two nodes iff in P there is an edge b between them. For an automaton D ′ over A [k] is easy to construct an automaton red (D ′ ) such that for all deterministic processes P over

A P red (D ′ ) iff P [k] D ′
With this we get

P red (D [k] /tt) iff P [k] D [k] /tt iff ∃R ′ . P [k] × R ′ D [k]
where R ′ and P [k] are over the alphabet A [k] . By definition, the last formula is equivalent to ∃R ′ .red We are left to show that we can bound the branching in our problem (1.2), so that we can fix k. The following proposition gives the desired bound. Lemma 6.3. Let P be a deterministic process and let A be an automaton with parity acceptance conditions. If there is (possibly nondeterministic) process R such that:

(P [k] × R ′ ) D. As P is deterministic red ( P [k] × R ′ ) = P × red (R ′ ).
P × R A
then there is R ′ with the same property which has the branching degree |A||A| Proof. Take R such that P × R A. Then Eve has a positional winning strategy (cf. Theorem 2.1) in the game G(P × R, A). This strategy is a function σ : (P ×R)×F A E → (P ×R)×F A which to pairs of the form (s, α∨β) assigns either (s, α) or (s, β); and to pairs of the form (s, b α) assigns a pair (s ′ , α) for some s ′ ∈ out P ×R (s, b). This function has the property that all the plays respecting suggestions of this function are winning for Eve. Take some state s of P × R. Let us(s, b), the set of useful successors, be the set of all successors t of s such that (t, α) = σ(s, b α) for some formula b α. Because the number of formulas of this kind is bounded by the size of A, so is the size of us(s, b).

The intention is that we would like to prune P × R so that on action b from s only edges to us(s, b) remain. This may not be correct as the following example shows. Suppose that us(s, b) = us(s, c), while out P ×R (s, b) = out P ×R (s, c). Now, the result of ↓↓ b,c test will be different in P × R and in the pruned structure. Hence, it may happen that A does not accept the pruned structure.

In order to avoid the problem mentioned in the above paragraph we extend us(s, b) to us ′ (s, b). For every state s and action b, let us ′ (s, b) be a set satisfying the following.

• us(s, b) ⊆ us ′ (s, b). • if s b then s ∈ us ′ (s, b). • if s b then either us ′ (s, b ′ ) = ∅, or s ′ ∈ us ′ (s, b ′ ) for some s ′ = s and s ′ ∈ out P ×R (s, b). • if s ↓↓ b,c then us ′ (s, b) = us ′ (s, c). • if s ↓↓ b,c and out P ×R (s, b) ⊆ out P ×R (s, c) then s ′ ∈ us ′ (s, b) for some arbitrary chosen s ′ ∈ out P ×R (s, b) -out P ×R (s, c).
It is easy to see that us ′ (s, b) can be chosen in such a way that it is at most |A|-times bigger than us(s, b). Now take P × R and delete all edges (s, b, t) such that t ∈ us ′ (s, b). Let us call the resulting process R ′ . In R ′ , strategy σ is still a winning strategy because we have only limited choices for Adam. Hence, Eve wins in G(R ′ , A), and in consequence R ′ A. We have that P × R ′ A, as P × R ′ = R ′ , since P is deterministic. By construction, the branching of R ′ is bounded by the maximal possible size of us ′ (s, b) which is |A||A|.

q.e.d. Remark 6.4. If the restriction of determinism of P is dropped than the division A/ ndet B does not exist even when A and B are simple. For example, take A which says that all maximal paths are of the form a * b, and if a state has an successor on action a then it does not have one on action b. Consider A/ ndet A. Condition P A/ ndet A means that there is R such that P × R A and R A. If P had two paths a i b and a j b of different length then in P × R we would have a path that does not finish with b. This implies that P A/ ndet A iff there is k such that all the paths in P have the form a k b. So the set of processes satisfying A/ ndet A is not regular. Observe that in this argument it did not matter whether we restrict to R being deterministic or not. Remark 6.5. Even when restricting to deterministic processes, automaton A/B may not exist if B is not simple. In [START_REF] Arnold | Games for synthesis of controllers with partial observation[END_REF] it is shown that decentralized control problem is undecidable for n = 2 if both B 1 and B 2 are automata with a constraints. In [START_REF] Briand | Contrôle avec événements indiscernables et inobservables[END_REF] undecidability is shown when both automata used ↓↓ a,b constraints, or when one uses a constrains and the other ↓↓ a,b constraints.

Undecidable cases of decentralized control

In this subsection we show left to right direction of Theorem 5.2. It will be enough to study the version of the control problem for two processes:

(ABC)Given automata A, B and C over the same action alphabet A, do there exist, possibly nondeterministic, processes P , R such that P A, R B and P × R C.

First, we will show that the problem is undecidable even when A, B and C are simple automata. This will give the proof of Theorem 5.2 for the case when there are at least two processes that can be nondeterministic. Next, we will consider the case when at most one of the processes can be nondeterministic. We will show that the above problem is undecidable when only R can be nondeterministic, and when B can use either constraints or ↓↓ constrains. This not only will imply the remaining part of Theorem 5.2, but will also show that restricting our automata uniquely to constraints or to ↓↓ constraints does not change the decidability classification.

Before showing these results we would like to introduce a syntactic extension of our setting which will make the presentation easier. We will suppose that we have propositional letters labelling states of processes. So each process comes not only with an alphabet of actions but also with an alphabet Λ of propositions:

P = A, Λ, S, s 0 , e ⊆ S × A × S, λ : S → Λ
Automata are also extended to reflect this, so the transition function can test what is a label of the current state:

A = Q, A, Λ, q 0 , δ : Q × Λ → F (A, Q), Acc ⊆ Q ω
There are many possible definitions of a product of two processes with state labels. Here we choose the one that will suit our needs. Given two processes over the same action alphabet, but possibly different proposition alphabets:

P = A, Λ P , S P , s 0 P , e p , λ P R = A, Λ R , S R , s 0 R , e R , λ R
we define their product as:

P ⊗ R = A, Λ P × Λ R , S P × S R , (s 0 P , s 0 R ), e ⊗ , λ ⊗
where λ ⊗ (s P , s R ) = (λ P (s P ), λ R (s R )) and, as before, ((s p , s R ), a, (s ′ P , s ′ R )) ∈ e ⊗ iff (s P , a, s ′ P ) ∈ e P and (s R , a, s ′ R ) ∈ e R . It is quite straightforward to see how to simulate propositional letters by actions. One can add propositional letters to the action alphabet and require that from each state there is a transition on exactly one propositional letter; the target of this transitions is of no importance.

The problem with this coding is that the standard product does not reflect our ⊗-product. In order to recover the ⊗-product, we first make the alphabets Λ P and Λ R disjoint. Let P , R denote respective plants with encoding of propositions as described above. We add to every state of P an action on every letter from Λ R and to every state of R an action on every letter of Λ P . This way we have that P × R is the encoding of P ⊗ R: from every state of P × R we have a successor on exactly one letter from Λ P and on one letter from Λ R .

After these remarks it should be clear that instead of the problem (ABC) we can consider the problem (ABC ⊗ ) where the processes are allowed to have propositions and ⊗ is used in place of ordinary product.

(ABC⊗)Given automata A, B and C over the same action alphabet A, and over proposition alphabets Λa, Λ b and Λa × Λ b respectively, do there exist processes P , R such that P A, R B and P ⊗ R C.

Thus, the following proposition implies undecidability of the problem (ABC).

Proposition 7.1. The problem (ABC ⊗ ) is undecidable.

Proof. We will present a reduction of the halting problem. Let us fix a deterministic Turing machine together with an alphabet Γ needed to encode its configurations. We write c ⊢ c ′ to say that a configuration c ′ is a successor of a configuration c. Without a loss of generality we assume that the machine loops from the accepting configuration. We will use just one action letter, so we will not mention it in the description below. The alphabet of propositions will contain Γ and special symbols: l and #. The nodes labelled by l will be called l-nodes; similarly for #-nodes, and γ-nodes for γ ∈ Γ. We will say that a node is a Γ-node, if it is a γ-node for some γ. We will also talk about an l-successor of a node, this a successor that is an l-node. Finally, when we will say that there is a path γ 1 . . . γ n in a process, this would mean that there is a sequence of nodes, that is a path, and such that the propositional letters associated to nodes form the sequence γ 1 . . . γ n .

l γ 1 1 γ 1 2 γ 1 n1 # ω l γ 2 1 γ 2 2 γ 2 n3 # ω l γ 3 1 γ 3 2 γ 3 n3 # ω Figure 1.
Intended shape of a process satisfying AB1, AB2, AB3.

We want to construct A, B and C so that the problem (ABC ⊗ ) has a solution iff the machine accepts when started from the empty tape. Consider the following three conditions that will be used for specifications A and B: AB1 Every l-node has an l-successor and a Γ-successor. Every Γ-node has either only Γ-nodes or only #-nodes as successors.

AB2 From every Γ-node, every path reaches a #-node.

AB3 Every #-node has only #-nodes as successors.

The intended shape of a process satisfying these conditions is presented in Figure 1. These conditions do not imply that the shape is exactly as presented in the figure. For example, they do not guarantee that there is only one infinite path labelled with l.

The constraints on the product of two processes are listed below. They are formulated in terms of the product alphabet.

C1 Every (l, l)-node has an (l, l)-successor and an (γ, γ)-successor for some γ ∈ Γ. Moreover all its successors are labelled either by (l, l), (l, γ), (γ, l) or (γ, γ).

C2 Every maximal path starting with (l, l) i (γ, γ) has a form (l, l) i ∆ + (#, #) ω where ∆ = {(γ, γ) : γ ∈ Γ}.

C3 Every maximal path that starts with (l, l) i (γ 1 , l)(γ 2 , γ ′ 1 ) for some

γ 1 , γ 2 , γ ′ 1 ∈ Γ has the form: (l, l) i (γ 1 , l)(γ 2 , γ ′ 1 ) . . . (γ k , γ ′ k-1 )(#, γ k )(#, #) ω . Moreover γ 1 . . . γ k ⊢ γ ′ 1 .
. . γ ′ k , or the two are identical if γ 1 . . . γ k is an accepting configuration.

C4 For every path labelled (l, l)(γ 1 , γ 2 ) . . . (γ k , γ k )(#, #) ω , the sequence γ 1 . . . γ k represents the initial configuration for the Turing machine. An accepting state of the machine appears in the tree.

Let C be the automaton expressing the conjunction of the conditions C1-C4. We claim that with this choice of automata the problem (ABC ⊗ ) has a solution iff the Turing machine halts on the initial configuration.

We first consider an easy direction. Suppose that the Turing machine halts on the initial configuration. Then we construct P and R as in the Figure 1, where for every i the sequence of Γ letters after l i is the i-th configuration of the machine (we assume that all configurations are represented by words of the same length). This way P and R satisfy conditions AB1-3. It is straightforward to verify that P ⊗ R satisfies the conditions C1-C4.

For the other direction, suppose that P and R are as required. We will show that the machine has an accepting computation from the initial configuration.

First, we show that the conditions we have imposed limit very much possible nondeterminism in P and R. Take any n and a path labelled l n γ 1 . . . γ kn # ω in P as well as a path labelled l n γ ′ 1 . . . γ ′ mn # ω in R. These paths exist by conditions AB1-AB3. In P × R these two paths give a path that starts with (l, l) n (γ 1 , γ ′ 1 ). The condition AB1 implies that γ 1 = γ ′ 1 . Consequently, the condition AB2 implies that k n = m n and γ i = γ ′ i for all i = 1, . . . , k n . This allows us to define u n = γ 1 . . . γ kn . To summarize, in P all paths of the form l n Γ + # ω have the same labels: l n u n # ω . Similarly for paths in R.

It remains to show that u n is the n-th configuration of the computation of the Turing machine. By condition A3, we know that u 1 is the initial configuration. Consider now a path in P ⊗ R labelled with

(l, l) n (γ 1 , l)(γ 2 , γ ′ 1 ) . . . (γ k , γ ′ k-1 )(#, γ ′ k )(#, #
) ω This path exists as it is a product of a path in P starting with l n γ 1 and a path in R starting with l n+1 γ ′ 1 . We have that

u n = γ 1 . . . γ k and u n+1 = γ ′ 1 . . . γ ′ k .
By the condition A2 we get u n ⊢ u n+1 .

q.e.d.

This finishes the case of Theorem 5.2 when at least two processes can be nondeterministic. It remains to consider the case when only one of the processes, say R can be nondeterministic, and when specification B of R is not simple. We will show that in this case the problem is undecidable even if B uses uniquely ↓↓ constraints, or uniquely constraints. Recall that the problem is decidable if B is simple, i.e. uses neither ↓↓ nor .

Proposition 7.2. The problem (ABC ⊗ ) is undecidable if P is required to be deterministic but R may be nondeterministic and moreover a specification for R may use constraints ↓↓. The reduction is very similar to the previous one. We just need to replace nondeterminism with appropriate use of ↓↓. This time our processes will be over the alphabet of two actions {a, b}. The intended shapes of processes P and R are shown in the Figure 2.

P : l γ 1 1 γ 1 2 γ 1 n1 # ω b l γ 2 1 γ 2 2 γ 2 n3 # ω b l γ 3 1 γ 3 2 γ 3 n3 # ω b a a R : l γ 1 1 γ 1 2 γ 1 n1 # ω b a l γ 2 1 γ 2 2 γ 2 n3 # ω b a l γ 3 1 γ 3 2 γ 3 n3 # ω
The shape of P is almost the same as in the previous construction, but as P needs to be deterministic, some a transitions have to be changed to b transitions. Process R has almost the same structure as P but it is nondeterministic, and each a transition has a b transition in parallel.

Looking at P ⊗ R we get almost exactly the same structure as in the case of nondeterministic processes. The fact that process P is deterministic and that the two transitions from an l-node of P have different actions is compensated by the fact that a and b transitions have the same targets in R.

The formalization of the constraints and the proof of the proposition is almost the same as in case of Proposition 7.1.

The following proposition treats the remaining case of constraints.

Proposition 7.3. The problem (ABC ⊗ ) is undecidable when P is required to be deterministic but R may be nondeterministic and moreover a specification for R may use looping constraints .

Proof. Consider an instance of the Post correspondence problem:

{(u 1 , v 1 ), . . . , (u k , v k )};
where all u i , v i are words over an alphabet Σ. Let D = {1, . . . , k} stand for the alphabet of indices. As an alphabet of actions we take A = Σ ∪ D ∪ {α 1 , α 2 , β, #}, with an assumption that the last four actions do not appear in Σ ∪ D.

The specification A for P will require that A1 Every state, except the root, has only one successor. The root has successors on α 1 and α 2 .

A2 There is a maximal path of the form α 1 βi 1 u i1 . . . i m u im # for some i 1 , . . . , i m ∈ D.

A3 There is a maximal path of the form α 2 βj 1 v j1 . . . j m v jm # for some j 1 , . . . , j m ∈ D.

Observe that together with requirement that P is deterministic, the first condition implies that P has exactly two maximal paths. The shape of P is presented in Figure 3.

The specification B for R will require that:

B1 The root has loops on actions α 1 and α 2 and some transitions on β.

B2 There is a path from the root of the form βΣ * #. Every node on this path except the root has loops on all actions from D and has a successor on at most one action from Σ ∪ {#}.

B3 There is a path from the root of the form βD * #. This time every node except the root has loops on actions from Σ and a successor on at most one action from D ∪ {#}.

The intended shape of a process satisfying B is presented in Figure 3. Observe that we cannot force this process to be deterministic. The specification C for P × R will require that all the paths are finite and that the last action on every path is #.

We claim that with this choice of A, B, and C, the problem (ABC) has a solution iff the instance of the Post correspondence problem has a solution.

For the right-to-left direction, take a solution i 1 , . . . , i m to the correspondence problem. We construct P that has two paths: α 1 βi 1 u i1 . . . i m u im # P: and α 2 βi 1 v i1 . . . i m v im #. As R we take a process as depicted in Figure 3 where the path satisfying condition B2 has the form βu i1 . . . u im #, and the path satisfying B3 is βi 1 . . . i m #. It is easy to see that P × R satisfies A.

For the direction from left to right suppose that P and R are a solution to the problem. Consider a path of R labelled βΣ * # satisfying B2 and the path α 1 βi 1 u i1 . . . i m u im # of P as required by the condition A2. Recall that there are loops on α 1 and α 2 in the root of R. This means that the two paths synchronize, at least at the beginning. The only way that the synchronization can continue until # is that u i1 . . . u im is exactly the labelling of the path in R. We can use the same argument for the path α 2 βj 1 v j1 . . . j m v jn # and in consequence we get u i1 . . . u im = v j1 . . . v jn . If we now repeat this argument once again but with a path of R labelled with βD * # as required by condition B3 then we will get that i 1 . . . i m = j 1 . . . j n . This finishes the proof.

q.e.d.

We can now summarize how the three propositions of this subsection can be used to show left to right implication of Theorem 5.2. If two of the processes R i are allowed to be nondeterministic then the undecidability follows from Proposition 7.1. The case when there are two automata that are not simple but all processes are deterministic was proven in [START_REF] Arnold | Games for synthesis of controllers with partial observation[END_REF] for constraints and in [START_REF] Briand | Contrôle avec événements indiscernables et inobservables[END_REF] for ↓↓ constraints, and a mix of and ↓↓ constraints. If a spec-ification can use either or ↓↓ constraints and the corresponding process can be nondeterministic then undecidability follows from Propositions 7.2 and 7.3, respectively.

Conclusions

In this paper we have studied the controller synthesis problem for nondeterministic plants and controllers. We have seen that going from deterministic to nondeterministic plants does not change the complexity of the problem. Allowing nondeterministic controllers is more delicate. It can be done in centralized case, but in the decentralized case at most one controller can be nondeterministic, moreover it should be able to observe all actions of the plant.

Let us briefly comment on the complexity of the constructions presented here. The operation of division by a process gives an exponential blow-up. It is unavoidable for the same reason as in a translation from alternating to nondeterministic automaton. The complexity of the construction for division by automaton is also exponential.

Given the results above one can ask whether they also apply to the setting of architectures of Pnueli and Rosner [START_REF] Pnueli | On the synthesis of a reactive module[END_REF]. It is quite simple to encode this latter setting into our setting using unobservable actions. Thus all decidability results in our setting transfer to architecture setting. As for undecidability results, one can show by methods very similar as those used in this paper that even two element pipeline becomes undecidable when specifications for controllers are allowed to be nondeterministic.

Proposition 2 . 2 .

 22 The class of languages recognized by automata is closed under sum, intersection and complement. This proposition allows to write A ∧ C to denote an automaton which recognizes L(A) ∩ L(C). Definition 2.3. An automaton is called simple if formulas in its transition function use none of a , a , ↓↓ a,b , ↓↓ a,b .

  where the definition of Code([a]α, τ ) is as above but replacing a by [a], b by [b], and disjunctions by conjunctions.

1 Corollary 5 . 1 .

 151 R BWe denote by Sol (P, A, B) the set of solutions to the problem. The following is a direct corollary of Theorem 4.For every process R: R ∈ Sol (P, A, B) if and only if R (A/P ) ∧ B.

Figure 2 .

 2 Figure 2. ↓↓ constraints. Intended shapes of P and R.

Figure 3 .

 3 Figure 3. -constraints. Intended shapes of P and R.

  Every nondeterministic process of branching bounded by k can be represented in such a way (in general not uniquely). From automaton D it is easy to construct an automaton D [k] which accepts a process P ′ over A [k] iff red (P ′ ) is accepted by D. Consider D[k]

k}. A deterministic process P ′ over an alphabet A [k] represents a nondeterministic process red (P ′ ) over an alphabet A where each action (a, i), for i = 1, . . . , k, is mapped to a.