Benjamin Aminof

Axel Legay

Aniello Murano

Olivier Serre

µ-calculus Pushdown Module Checking with Imperfect State Information

The model checking problem for open systems (module checking) has recently been the subject of extensive study. The problem was first studied by Kupferman, Vardi, and Wolper for finite-state systems and properties expressed in the branching time logics CTL and CTL * . Further study continued mainly in two directions: considering systems equipped with a pushdown store, and considering environments with imperfect information about the system. A recent paper combined the two directions and considered the CTL pushdown module checking problem in the imperfect information setting, i.e., in the case where the environment has only a partial view of the system control states and pushdown store content. It has been shown that this problem is undecidable when the environment has imperfect information about the pushdown store content, while it is decidable and 2Exptime-complete when the imperfect information only concerns control states. It was left open whether the latter remains decidable also for more expressive logics. In this paper, we answer this question in the affirmative, showing that the pushdown module checking problem with imperfect information about the control states is decidable and 2Exptime-complete for the propositional and the graded µ-calculus, and 3Exptime-complete for CTL * .

Introduction

A main distinction in system modeling is between closed systems, whose behavior is totally determined by the program, and open systems, which are systems where the program interacts with an external environment [START_REF] Harel | On the development of reactive systems[END_REF][START_REF] Hoare | Communicating Sequential Processes[END_REF]. In order to check whether a closed system satisfies a required property we translate the system into a formal model (such as a transition system), specify the property with a temporal-logic formula (such as CTL [START_REF] Clarke | Design and verification of synchronization skeletons using branching time temporal logic[END_REF], CTL * [EH86], and µ-calculus [START_REF] Kozen | Results on the propositional mu-calculus[END_REF]), and check formally that the model satisfies the formula. This process is called model checking ( [START_REF] Clarke | Design and verification of synchronization skeletons using branching time temporal logic[END_REF][START_REF] Queille | Specification and verification of concurrent programs in Cesar[END_REF]). Checking whether an open system satisfies a required temporal logic formula is much harder, as one has to consider the interaction of the system with all possible environments.

In this paper, we consider open systems which are modeled in the framework introduced by Kupferman, Vardi, and Wolper. Concretely, in [START_REF] Kupferman | Module checking[END_REF][START_REF] Kupferman | Module Checking[END_REF], an open finite-state system is described by an extended transition system called a module, whose set of states is partitioned into system states (where the system makes a transition) and environment states (where the environment makes a transition). Given a module M, describing the system to be verified, and a branching time temporal logic formula ϕ, specifying the desired behavior of the system, the problem of model checking a module, called module checking, asks whether for all possible environments, M satisfies ϕ. In particular, it might be that the environment does not enable all the external choices. Module checking thus involves not only checking that the full computation tree obtained by unwinding M (which corresponds to the interaction of M with a maximal environment) satisfies the specification ϕ, but also that every tree obtained from it by pruning children of environment nodes (this corresponds to the different choices of different environments) satisfies ϕ. For example, consider an ATM machine that allows customers to deposit money, withdraw money, check balance, etc. The machine is an open system, and an environment for it is a subset of the set of all possible infinite lines of customers, each with their own plans. Accordingly, there are many different possible environments to consider.

The finite-state system module checking problem, for CTL and CTL * formulas, has been investigated in [START_REF] Kupferman | Module checking[END_REF][START_REF] Kupferman | Module Checking[END_REF]; while for propositional µ-calculus formulas it has been investigated in [START_REF] Ferrante | Enriched µ-calculus module checking[END_REF]. In all these cases, it has been shown that module checking is exponentially harder than model checking. However, an interesting aspect of these results is that they bear on the corresponding automata-based results for closed systems [START_REF] Kupferman | An Automata-Theoretic Approach to Branching-Time Model Checking[END_REF], which gives the hope for practical implementations and applications.

Recently, the module checking idea has been extended to pushdown systems [START_REF] Bozzelli | Pushdown module checking[END_REF], and it has been shown that CTL and µ-calculus pushdown module checking is 2Exptime-complete, while CTL * pushdown module checking is 3Exptime-complete [START_REF] Bozzelli | Pushdown module checking[END_REF][START_REF] Ferrante | Enriched µ-calculus pushdown module checking[END_REF]. Another extension of the module checking idea has been the investigation of environments with imperfect information. The first results on the subject were dedicated to finite-state systems [START_REF] Kupferman | Module checking revisited[END_REF]. In this framework, every state of the module is a composition of visible and invisible variables, where the latter are hidden from the environment. While a composition of a module M with an environment with perfect information corresponds to arbitrary disabling of transitions in M, the composition of M with an environment with imperfect information is such that whenever two computations of the system differ only in the values of invisible variables along them, the disabling of transitions along them coincide. In [START_REF] Kupferman | Module checking revisited[END_REF] it has been shown that CTL and CTL * module checking with imperfect information is harder than module checking with perfect information. The results in [START_REF] Kupferman | Module checking revisited[END_REF] were recently extended in [START_REF] Aminof | Pushdown module checking with imperfect information[END_REF] to pushdown systems. In this framework, environments with imperfect information about the system's control state and pushdown store content are considered. Like in the finite-state case, the control states are assignments to Boolean control variables, some of which are visible and some of which are not. Similarly, symbols of the pushdown store are assignments to Boolean visible and invisible pushdown store variables. It has been shown in [START_REF] Aminof | Pushdown module checking with imperfect information[END_REF] that in the presence of imperfect information, CTL pushdown module-checking becomes undecidable, and that the undecidability relies upon hiding information about the pushdown store. Indeed, it was shown that CTL pushdown module checking with imperfect state information but visible pushdown store is decidable and 2Exptime-complete.

[AMV07] left open the question whether the pushdown module checking problem with imperfect state information, but visible pushdown store, is still decidable when more expressive logics are considered. In this paper we answer this question in the affirmative. Our main contribution is showing that this problem is decidable and 2Exptime-complete for the propositional µ-calculus and the graded µ-calculus [KSV02]1 , and 3Exptime-complete for CTL * . The lower bound follows from the known perfect information case. For the upper bound we use an automata theoretic approach, and reduce the problem to the emptiness problem of a semi-alternating pushdown parity tree automaton (PD-SPT). These are alternating pushdown parity tree automata that behave deterministically on the pushdown store content. That is, two copies of the automaton that read the same input, from two configurations that have the same top of pushdown store, must push the same value into the pushdown store. In this paper, we show that unlike alternating pushdown parity tree automata, for which the emptiness problem is undecidable2 , the emptiness problem for PD-SPT is solvable in 2Exptime, which allows us to get the required upper bound for our problem.

Preliminaries

In this section, we first recall the concept of open system. Then, we introduce the logics that will be model checked.

Open Systems.

Let Υ be a finite set. An Υ -tree is a prefix closed subset T ⊆ Υ * . The elements of T are called nodes and the empty word ε is the

root of T . For v ∈ T , the set of children of v (in T ) is child(T, v) = {v • x ∈ T | x ∈ Υ }. Given a node v = u • x,
with u ∈ Υ * and x ∈ Υ , we define last(v) to be x. The complete Υ -tree is the tree Υ * . For v ∈ T , a (full) path π of T from v is a minimal set π ⊆ T , such that v ∈ π and for each v ′ ∈ π, such that child(T, v ′ ) = ∅, there is exactly one node in child(T, v ′ ) belonging to π. Note that every w ∈ Υ ω can be thought of as an infinite path in the tree Υ * , namely the path containing all the finite prefixes of w. For an alphabet Σ, a Σ-labeled Υ -tree is a pair T, V where T is an Υ -tree and V : T → Σ maps each node of T to a symbol in Σ.

An open system is a system that interacts with its environment and whose behavior depends on this interaction. We consider the case where the environment has imperfect information about the system, i.e., when the system has internal variables that are not visible to its environment. We describe such a system by a module M = AP, W s , W e , w 0 , R, L, ∼ = , where AP is a finite set of atomic propositions, W s is a set of system states, and W e is a set of environment states. We assume that W s ∩ W e = ∅, and call W = W s ∪ W e the set of M's states. The state w 0 ∈ W is the initial state, R ⊆ W × W is a total transition relation, L : W → 2 AP is a labeling function that maps each state of M to the set of atomic propositions that hold in it, and ∼ = is an equivalence relation on

W . A module M is closed if W e = ∅.
States that are indistinguishable by the environment are equivalent according to ∼ =. We write [W ] for the set of equivalence classes of W under ∼ =. For the environment, the states of the system are actually the equivalence classes themselves. The equivalence class [w] of a state w ∈ W is called the visible part of w. We write vis(w), instead of [w], to emphasize this.

Given w, w ′ ∈ R, w ′ is a successor of w. For each state w ∈ W , we denote by succ(w) the set (possibly empty) of w's successors. A computation of M is a sequence w 0 • w 1 • • • of states, such that for all i ≥ 0 we have w i , w i+1 ∈ R. The set of all (maximal) computations of M starting from the initial state w 0 can be described by an AP -labeled W -tree T M , V M called a computation tree, which is obtained by unwinding M in the usual way.

Each node v = v 1 • • • v k of T M , V M describes the (partial) computation w 0 • v 1 • • • v k of M,
with the root ε corresponding to w 0 . The children of v are exactly all nodes of the form v 1 • • • v k • w, where w ranges over all the successors of v k in M. We extend the definition of vis to nodes in the natural way. Thus, the visible part of a node v is vis(v) = vis(v 1 ) • • • vis(v k ). The labeling V M of a node v depends on the state it corresponds to (its last state), i.e., V M (v) = L(last(v)). Also, if v corresponds to an environment state we say that v is an environment node.

Whenever M interacts with an environment ξ, its possible moves from environment states (i.e., states in W e ) depend on the behavior of ξ. We can think of an environment to M as a strategy ξ : [W ] * → {⊤, ⊥} that maps a finite history s of a computation, as seen by the environment, to either ⊤ or ⊥, meaning that the environment respectively allows or disallows M to trace s (obviously, if s is a successor of a system state, the decision whether to trace s or not is made by the system, and we ignore the environment's value of ξ(s)). Observe that if an environment disallows M to trace s, it effectively disallows M to trace any of the successors of s. Note that one can either require that for every y ∈ [W ] * , if ξ(x) = ⊥ then ξ(x • y) = ⊥, or simply ignore the value ξ(x • y). We chose the latter. We say that the tree [W ] * , ξ maintains the strategy applied by ξ, and we call it a strategy tree. We denote by M ✁ ξ the AP -labeled W -tree induced by the composition of T M , V M with ξ; that is, the AP -labeled W -tree obtained by pruning from T M , V M subtrees according to ξ. Note that by the definition above, ξ may disable all the children of a node v. Since we usually do not want the environment to completely block the system, we require that at least one child of each node is enabled. In this case, we say that the composition M ✁ ξ is deadlock-free. Given a module M, and a strategy tree [W ] * , ξ for an environment ξ, an AP -labeled W -tree T, V corresponds to M ✁ ξ iff:

-The root of T corresponds to w 0 . -For v ∈ T with last(v) ∈ W s , we have child(T, v) = {v • w 1 , . . . , v • w n }, where succ(last(v)) = {w 1 , . . . , w n }. -For v ∈ T with last(v) ∈ W e , there exists a nonempty subset {w 1 , . . . , w k } of succ(last(v)) such that child(T, v) = {v • w 1 , . . . , v • w k }. Furthermore, for all w in {w 1 , . . . , w k } we have that ξ(vis(v • w)) = ⊤, while for all w in succ(last(v)) \ {w 1 , . . . , w k } we have that ξ(vis(x • w)) = ⊥. -For every node v ∈ T , we have that V (v) = L(last(v)).
For a module M and a temporal logic formula ϕ defined over AP , we say that M reactively satisfies ϕ, denoted M |= r ϕ, if M✁ξ satisfies ϕ, for every environment ξ for which M ✁ ξ is deadlock-free. The problem of deciding whether M |= r ϕ is called the module checking problem with imperfect information.

Logics.

In this paper, we consider ϕ to be either a CTL * or a propositional/graded µ-calculus formula. The syntax and semantics of CTL * and µ-calculus are well known, and we assume that the reader is familiar with them (for references, see [START_REF] Kozen | Results on the propositional mu-calculus[END_REF] and [START_REF] Kupferman | An Automata-Theoretic Approach to Branching-Time Model Checking[END_REF]). In the rest of this section, we focus on graded µcalculus, which is an extension of the propositional µ-calculus that allows graded modalities. These modalities are denoted by n ("exist at least n-successors") and [n] ("all but at most n successors"), respectively.

Formally, we have the following. Let AP and Var be finite and pairwise disjoint sets of atomic propositions and propositional variables. The set of graded µ-calculus formulas is the smallest set such that (i ) true and false are formulas; (ii ) p and ¬p, for p ∈ AP , are formulas; (iii ) x ∈ Var is a formula; (iv ) if ϕ 1 and ϕ 2 are formulas, n is a non negative integer, and y ∈ V ar, then ϕ 1 ∨ ϕ 2 , ϕ 1 ∧ϕ 2 , n ϕ 1 , [n]ϕ 1 , µy.ϕ 1 (y), and νy.ϕ 1 (y) are also formulas. Observe that we use positive normal form, i.e., negation is applied only to atomic propositions. We often refer to the graded modalities n ϕ 1 and [n]ϕ 1 as, respectively, atleast formulas and allbut formulas, and assume that the integers in these operators are given in binary coding: the contribution of n to the length of each of the formulas n ϕ and [n]ϕ is ⌈log n⌉, rather than n.

The definition of the semantics of graded µ-calculus w.r.t an AP -labeled Wtree T, V is similar to that of the standard µ-calculus, except for the graded modalities. Informally, an atleast formula n ϕ holds at a node w of the tree if ϕ holds in at least n + 1 children of the node. Dually, the allbut formula [n]ϕ holds in a node of the tree K if ϕ holds in all but at most n of its successors.

Due to space limitation, we refer the reader to [START_REF] Kupferman | The complexity of the graded µ-calculus[END_REF] (also [START_REF] Bonatti | The complexity of enriched µ-calculi[END_REF]) for a formal description of the full semantics.

Imperfect Information Pushdown Module Checking

In this section, we consider infinite-state modules which are induced by Open Pushdown Systems (OPD) [START_REF] Aminof | Pushdown module checking with imperfect information[END_REF]. In our framework, the environment has imperfect information about the internal control states of the system, but the pushdown store is visible. Definition 1. An OPD is a tuple S = AP, Q, q 0 , Γ, ♭, δ, η, Env , where AP is a finite set of atomic propositions; Q is a finite set of ( control) states; and q 0 ∈ Q is an initial state. We assume that Q ⊆ 2 V ∪H , where V and H are disjoint finite sets of visible and invisible control variables, respectively. Γ is a finite pushdown store alphabet; ♭ ∈ Γ is the pushdown store bottom symbol, and we use

Γ ♭ to denote Γ ∪{♭}. The transition relation δ ⊆ (Q×Γ ♭ )×(Q×Γ * ♭ ) is finite; η : Q × Γ ♭ → 2 AP is a labeling function; and Env ⊆ Q × Γ ♭ is used to specify the set of environment configurations. The size |S| of S is |Q|+|Γ |+|δ|, with |δ| = ((p,γ),(q,β))∈δ |β|.
A configuration of S is a pair (q, α), where q is a control state and α ∈ Γ * • ♭ is a pushdown store content. We write top(α) for the leftmost symbol of α, and call it the top of the pushdown store α. The OPD moves according to the transition relation. Thus, ((p, γ), (q, β)) ∈ δ implies that if the OPD is in state p, and the top of the pushdown store is γ, then it can move to state q, pop γ and push β. We assume that ♭ is always present at the bottom of the pushdown store, and nowhere else. Note that we make this assumption also about the various pushdown automata we use later. For a control state q ∈ Q, the visible part of q is vis(q) = q ∩ V . The visible part of a configuration (q, α), is thus vis((q, α)) = (vis(q), α). As for modules, the designation of a configuration of an OPD as an environment configuration is known to the environment. Thus, we require that for every two configurations (q, α) and (q ′ , α ′ ), such that vis(q) = vis(q ′ ), it holds that (q, top(α)) ∈ Env iff (q ′ , top(α ′ )) ∈ Env. Definition 2. An OPD S = AP, Q, q 0 , Γ, ♭, δ, η, Env induces an infinite-state module M S = AP, W s , W e , w 0 , R, L, ∼ = , possibly with invisible information, where AP is a set of atomic propositions; W s ∪ W e = Q × Γ * • ♭ is the set of configurations; W e is the set of configurations (q, α) such that (q, top(α)) ∈ Env; w 0 = (q 0 , ♭) is the initial configuration; R is a transition relation, where

((q, γ • α), (q ′ , β)) ∈ R iff there exist ((q, γ), (q ′ , β ′ )) ∈ δ such that β = β ′ • α; L((q, α)) = η(q, top(α)
) for all (q, α) ∈ W ; and for every two configurations w, w ′ ∈ W , we have that w ∼ = w ′ iff vis(w) = vis(w ′ ).

To describe the interaction of an OPD S with its environment we consider the interaction of the environment with the induced module M S . Indeed, every environment ξ of S can be represented by a strategy tree [W ] * , ξ , and the composition M S ✁ ξ of [W ] * , ξ with T MS , V MS describes all the computations of S allowed by the environment ξ.

We consider the pushdown module checking problem with imperfect state information, i.e., given an OPD S and a formula ϕ, decide whether M S |= r ϕ.

The pushdown module checking problem with imperfect state information is known to be 2Exptime-complete when ϕ is a CTL formula [START_REF] Aminof | Pushdown module checking with imperfect information[END_REF]. In this paper, we answer an open question of [START_REF] Aminof | Pushdown module checking with imperfect information[END_REF] and show that the problem remains 2Exptime-complete when considering ϕ to be a propositional or a graded µ-calculus formula, and that it becomes 3Exptime-complete when ϕ is a CTL * formula. For the upper bound, we reduce our problem to the emptiness problem of a semi-alternating pushdown parity tree automata.

Semi-Alternating Pushdown Tree Automata.

We start with the definition of semi-alternating pushdown parity tree automata (PD-SPT ), first introduced in [AMV07] w.r.t. a Büchi acceptance condition. A PD-SPT is a tuple A = Σ, D, Γ, Q, q 0 , ♭, δ, F , where Σ is a finite input alphabet, D is a finite set of directions, Γ is a finite pushdown store alphabet, Q is a finite set of states, q 0 ∈ Q is the initial state, ♭ ∈ Γ is the pushdown store bottom symbol, and F is a parity acceptance condition (to be defined later). Moreover, δ is a finite transition relation defined as a function δ :

Q × Σ × Γ ♭ → B + (D × Q × Γ * ♭ )
, where, as usual, Γ ♭ = Γ ∪ {♭}, and

B + (D × Q × Γ * ♭ )
is the set of all finite positive Boolean combinations of triples (d, q, β), where d is a direction, q is a state, and β is a word made of pushdown store symbols. We also allow the formulas true and false. We write S ∈ δ(p, σ, γ) to denote that S is a set of tuples (d, q, β) that satisfy δ(p, σ, γ).

What makes the automaton semi-alternating is the requirement that for every d ∈ D, σ ∈ Σ, p, p ′ ∈ Q (possibly the same state), and γ ∈ Γ , if (d, q, β) appears in δ(p, σ, γ), and (d, q ′ , β ′ ) appears in δ(p ′ , σ, γ), then β = β ′ . That is, two copies of the automaton that read the same input, from two configurations that have the same top symbol of the pushdown store, and proceed in the same direction, must push the same value into the pushdown store. In particular, it follows that in every run, two copies of the automaton that are reading the same node of an input tree have the same pushdown store content. Note that if we remove the semi-alternation requirement the resulting automaton is called alternating pushdown parity tree automaton (PD-APT ).

As a special case of PD-APT, we consider nondeterministic pushdown parity tree automata (PD-NPT ), where the concurrency feature (i.e., the ∧ operator in δ) is not allowed. That is, whenever a PD-NPT visits a node x of the input tree, it sends to each successor (direction) of x at most one copy of itself. More formally, a PD-NPT is a PD-APT in which δ is in disjunctive normal form, and in each conjunct each direction appears at most once. Note that if A is a PD-APT with Γ = ∅, its pushdown store is neutralized, hence, A is simply called an alternating parity tree automaton (APT ), and we can abbreviate and write

A = Σ, D, Q, q 0 , δ, F , where δ : Q × Σ → B + (D × Q).
Similarly, a PD-NPT with an empty pushdown store alphabet is called a nondeterministic parity tree automaton (NPT ).

A run of a PD-SPT A, on a Σ-labeled tree T, V , with T = D * , is a (D * × Q × Γ * • ♭)-labeled N-tree T r , r , such that the root is labeled with (ε, q 0 , ♭) and the labels of each node and its successors satisfy the transition relation. Formally, a (D * × Q × Γ * • ♭)-labeled tree T r , r is a run of A on T, V iff -r(ε) = (ε, q 0 , ♭), and -for all x ∈ T r such that r(x) = (y, p, γ • α), there is an n ∈ N such that the successors of x are exactly x•1, . . . x•n, and for all 1 ≤ i ≤ n we have r(

x•i) = (y • d i , p i , β i • α) for some {(d 1 , p 1 , β 1 ), . . . , (d n , p n , β n )} ∈ δ(p, V (y), γ).
For a path π ⊆ T r , let inf r (π) ⊆ Q be the set of states that appear in the labels of infinitely many nodes in π. For a parity condition

F = {F 1 , F 2 , . . . , F k }, with F 1 ⊆ F 2 ⊆ • • • ⊆ F k = Q,
we have that π is accepting iff the minimal index i, for which inf r (π) ∩ F i = ∅, is even. The number k is called the index of the automaton. A run T r , r is accepting iff all its paths are accepting. The automaton A accepts an input tree T, V iff there is an accepting run of A on T, V . The language of A, denoted L(A), is the set of Σ-labeled trees with branching degree D accepted by A. We say that an automaton A is nonempty iff L(A) = ∅. Given a PD-SPT A = Σ, D, Γ, Q, q 0 , ♭, δ, F , we define the size of δ as the sum of the lengths of the satisfiable (i.e., not false) formulas that appear in δ(q, σ, γ), for some q, σ, and γ.

Simulating a PD-SPT by a PD-NPT.

As mentioned in [START_REF] Aminof | Pushdown module checking with imperfect information[END_REF], alternating pushdown automata are not equivalent to nondeterministic ones. However, as we show here, the limitations imposed on semi-alternating automata allow us to translate a PD-SPT to an equivalent PD-NPT3 . A key observation is that since a pushdown store operation performed by a semi-alternating automaton does not depend on the current (or next) control states, we can split the transition function of a PD-SPT into two functions: a state transition function δ Q , and a pushdown store update function δ Γ , as follows. Given a PD-SPT A = Σ, D, Γ, Q, q 0 , ♭, δ, F , let δ

Q : Q × Σ × Γ ♭ → B + (D × Q) be the projection of δ on B + (D × Q). That is, δ Q (q, σ
, γ) is obtained from δ(q, σ, γ) by replacing every element (d, q, β) that appears in δ(q, σ, γ) with (d, q). The pushdown store update function δ

Γ : Σ × Γ ♭ × D → Γ * ♭ , is a partial function; for every (p, σ, γ) ∈ Q × Σ × Γ ♭ and every (d, q, β) ∈ D × Q × Γ * ♭ , such that (d, q, β) appears in δ(p, σ, γ), we let δ Γ (σ, γ, d) = β. Since A is semi- alternating, δ Γ is well defined. Observe that for every (p, σ, γ) ∈ Q × Σ × Γ ♭ we
have that δ(p, σ, γ) can be obtained from δ Q (p, σ, γ) by replacing every (d, q) that appears in δ Q (p, σ, γ) with (d, q, δ Γ (σ, γ, d)).

Consider a Σ-labeled tree T, V , with T = D * . Note that for every node x ∈ T and every run of A on T, V , the pushdown store content of all the copies of A that visit x is the same, and only depends on x. We can thus define a function ∆ Γ : T → Γ * ♭ , giving for every node x its associated pushdown store content, as follows: (1) ∆ Γ (ε) = ♭, and (2) for all x • d ∈ T we have

∆ Γ (x • d) = δ Γ (V (x), γ, d) • β, where ∆ Γ (x) = γ • β, and γ ∈ Γ ♭ .
Annotating input trees with pushdown store symbols enables us to simulate a PD-SPT by an APT running on the annotated version of an input tree. Given a Σ-labeled tree T, V , we define its Γ A -annotation to be the (Σ × Γ ♭ )-labeled tree T, U , obtained by letting U (x) = (V (x), top(∆ Γ (x))), for every x ∈ T . Lemma 1. Let A = Σ, D, Γ, Q, q 0 , ♭, δ, F be a PD-SPT. There is an APT Ã, such that A accepts T, V iff à accepts the Γ A -annotation of T, V .

Proof. Consider the APT à = Σ × Γ ♭ , D, Q, q 0 , δ, F , where δ(q, (σ, γ)) = δ Q (q, σ, γ). It is not hard to see that every run r = T r , r of A on T, V induces a corresponding run r ′ = T r , r ′ of à on the Γ A -annotation of T, V , and vice versa. The connection between r and r ′ being that for every x ∈ T r , we have that r(x) = (y, p, α) iff r ′ (x) = (y, p) and ∆ Γ (x) = α. ⊓ ⊔ By [START_REF] Muller | Alternating automata on infinite trees[END_REF], every APT can be translated to an equivalent NPT. Hence, Lemma 1 implies that if A is a PD-SPT, then there is an NPT A ′ such that A accepts T, V iff A ′ accepts the Γ A -annotation of T, V . This allows us to translate A to an equivalent PD-NPT A ′′ (running on the same input trees as A). Given a Σ-labeled tree, A ′′ generates on the fly its Γ A -annotation and runs A ′ on the annotated tree. Formally, we have the following: Theorem 1. Every PD-SPT can be translated to an equivalent PD-NPT.

Proof. Let A = Σ, D, Γ, Q, q 0 , ♭, δ, F be a PD-SPT and à = Σ×Γ ♭ , D, Q, q 0 , δ, F be an APT derived from A by Lemma 1. By [START_REF] Muller | Alternating automata on infinite trees[END_REF], à has an equivalent NPT A ′ = Σ × Γ ♭ , D, Q ′ , q ′ 0 , δ ′ , F ′ . Consider the PD-NPT A ′′ = Σ, D, Γ, Q ′ , q ′ 0 , ♭, δ ′′ , F ′ , where for every (p, σ, γ) ∈ Q ′ × Σ × Γ ♭ , we have that δ ′′ (p, σ, γ) is obtained from δ ′ (p, (σ, γ)) by replacing every (d, q) that appears in δ ′ (p, (σ, γ)), with (d, q, δ Γ (σ, γ, d)). Since A ′ is nondeterministic, so is A ′′ . Given a Σ-labeled tree T, V , it is not hard to see that for every x ∈ T , the pushdown store of every copy of A ′′ that visits x contains exactly ∆ Γ (x). Hence, A ′′ accepts T, V iff A ′ accepts the Γ A -annotation of T, V , i.e., iff A accepts T, V . ⊓ ⊔

The Emptiness Problem of PD-SPT.

Looking at the automata transformations performed in Theorem 1 and Lemma 1 we see that the only transformation that incurs a blowup in the size of the automaton is the transformation of the APT Ã to the NPT A ′ . By [START_REF] Muller | Alternating automata on infinite trees[END_REF],

given an APT with n states and index k, running over D * trees, one can build an equivalent NPT with (nk) O(nk) states, an O(nk) index, and a transition relation of size (nk) O(|D|nk) . Hence, starting with a PD-SPT A with n states and index k, our algorithm yields an equivalent PD-NPT A ′′ with (nk) O(nk) states, an O(nk) index, and a transition relation of size (nk) O(|D|nk) . It is worth noting that the blowup is independent of the size of the transition relation of A. By [START_REF] Kupferman | Pushdown specifications[END_REF], the emptiness of A ′′ can be decided in time exponential in the product of the number of states, the index, and the size of the transition relation of A ′′ . Overall, we get the following corollary:

Corollary 1. The emptiness problem for a PD-SPT with n states and index k, running on D * trees, can be solved in time double-exponential in |D|nk.

Solving Pushdown Module Checking with Imperfect State Information

We first show that the pushdown module checking problem with imperfect state information, for µ-calculus, graded µ-calculus, and CTL * , can be reduced to the emptiness problem of PD-SPT.

Basically, we extend the automata theoretic approach used in [AMV07] for CTL pushdown module checking with imperfect state information. Before presenting the formal reduction, let us briefly recap the approach taken by [START_REF] Aminof | Pushdown module checking with imperfect information[END_REF], and discuss the main changes required to adapt it to the problem we address. Given an OPD S, and aCTL formula ϕ, one builds an automaton A S,ϕ that accepts {⊤, ⊥}-labeled trees corresponding to strategies ξ, whose composition with M S is deadlock-free and satisfies ϕ. Intuitively, a run of A S,ϕ on an input strategy tree ξ proceeds by simulating an unwinding of the module M S , pruned at each step accordingly to the strategy ξ; copies of the automaton which simulate nodes in the computation tree of M S that are indistinguishable by the environment are sent to the same direction in the input tree. The resulting run tree of A S,ϕ on ξ is basically a replica of the composition M S ⊳ ξ, and the fact that it satisfies the formula ϕ is checked on the fly, by employing in A S,ϕ the classical alternating-automata approach for model checking CTL.

When considering CTL * or µ-calculus, adapting the construction used in [START_REF] Aminof | Pushdown module checking with imperfect information[END_REF] basically amounts to replacing the embedded alternating automaton that does the on-the-fly model checking: instead of using an automaton that handles CTL, one uses an automaton that handles CTL * (or µ-calculus). Since an alternating automaton that does µ-calculus model checking is linear in the size of the formula, while one that does CTL * model checking is exponential in the size of the formula [KVW00], the automaton A S,ϕ has O(|S| * |ϕ|) states in the case of µ-calculus, and O(|S| * 2 |ϕ| ) states in the case of CTL * . It is important to note that the acceptance condition of A S,ϕ is essentially that of the embedded model checking automaton. Hence, unlike in [START_REF] Aminof | Pushdown module checking with imperfect information[END_REF], where a Büchi condition was enough, for the more expressive logics that we consider here, we need a stronger acceptance condition, namely, a parity condition, for which solving the emptiness problem requires stronger machinery.

The extension of the construction used in [START_REF] Aminof | Pushdown module checking with imperfect information[END_REF] is slightly more delicate when considering graded µ-calculus. Given a graded µ-calculus formula ϕ, one possible approach is to translate ϕ into an equivalent µ-calculus formula (without graded modalities). Essentially, as pointed out in [START_REF] Kupferman | The complexity of the graded µ-calculus[END_REF], one introduces new atomic propositions p 1 , . . . , p b , (where b is the largest number used in the graded modalities in ϕ) and replaces every atleast formula n ψ by {i1,...,in+1}⊆{1,...,b} 1≤j≤n+1 0 (ψ ∧ p ij ), and dually for allbut formulas. One also has to conjoin ϕ with a formula stating that exactly one of the p 1 , . . . , p b holds at each state, and that successors that are labeled with the same p i agree on their label with respect to all the formulas in the closure of ϕ. Unfortunately, since the numbers in the graded modalities are coded in binary, such a translation may result in a µ-calculus formula which is exponentially larger than ϕ; resulting in an overall exponentially worse complexity for the graded µ-calculus, compared to the un-graded one. In order to avoid this extra exponent, in the context of satisfiability, [START_REF] Kupferman | The complexity of the graded µ-calculus[END_REF] introduced graded automata. However, graded automata do not transfer directly to the imperfect information setting. Fortunately, there is another solution. Instead of expanding the graded modalities at the formula stage, as suggested above, we can expand them as we build the transition relation of A S,ϕ . Thus, for example, the transition relation of A S,ϕ will specify that a copy of the automaton, that is responsible for verifying that an atleast formula n ψ holds at a certain configuration of the OPD, should send n + 1 copies of itself to one of the exponentially many possible subsets of n + 1 successors of the current configuration. This expansion of the graded modalities allows A S,ϕ to handle graded µ-calculus formulas using an embedded regular µ-calculus model checker (without graded modalities). This comes at the price of A S,ϕ having an exponentially larger transition relation than if graded modalities were not present; but does not affect the number of states, or the index, of A S,ϕ . Since our algorithm for checking the emptiness of PD-SPT is such that its complexity does not depend on the size of the transition relation of the PD-SPT, we handle graded µ-calculus formulas with the same complexity as we do regular µ-calculus formulas.

Theorem 2. Consider an OPD S and a propositional, or a graded, µ-calculus (resp. CTL * ) formula ϕ, over S's atomic propositions. There is a PD-SPT A S,ϕ with O(|S| * |ϕ|) states (resp. O(|S| * 2 |ϕ| )), and an index O(|ϕ|), such that L(A S,ϕ ) is exactly the set of strategies ξ for which M S ⊳ ξ is deadlock-free and satisfies ϕ.

Proof (Sketch). We give the construction of A S,ϕ for the graded µ-calculus. The construction for the propositional µ-calculus is very similar, and the one for CTL * is obtained by replacing the embedded classical alternating-automata model checker with a CTL * one.

We first give some extra definitions regarding graded µ-calculus. From now on, we refer to µ and ν as fixpoint operators. A propositional variable y occurs free in a formula if it is not in the scope of a fixpoint operator, and bounded otherwise. We use λ to denote a fixpoint operator µ or ν. For a formula λy.ϕ(y), we write ϕ(λy.ϕ(y)) to denote the formula that is obtained from λy.ϕ(y) by one-step unfolding; i.e., ϕ(λy.ϕ(y)) is obtained by replacing each free occurrence of y in ϕ with λy.ϕ(y). For technical convenience, we restrict our attention to formulas without free variables (also called sentences). The closure cl(ϕ) of a graded µ-calculus sentence ϕ is the smallest set of graded µ-calculus formulas that contains ϕ and is closed under sub-formulas (that is, if ψ is in the closure, then so do all its sub-formulas that are sentences) and fixpoint applications (that is, if λy.ϕ(y) is in the closure, then so is ϕ(λy.ϕ(y))). As proved in [START_REF] Bonatti | The complexity of enriched µ-calculi[END_REF], for every graded µ-calculus formula ϕ, the number of elements in cl(ϕ) is linear in the length of ϕ. Accordingly, we define the size |ϕ| of ϕ to be the number of elements in cl(ϕ).

Let S = AP, Q, q 0 , Γ, ♭, δ, η, Env be an OPD, let ϕ be a graded µ-calculus formula (guarded 4 , without free variables, and in positive normal form), and let M S = AP, W s , W e , w 0 , R, L, ∼ = be the module induced by S. We build an automaton A S,ϕ that accepts {⊤, ⊥}-labeled trees corresponding to strategies ξ, whose composition with M S is deadlock-free and satisfy ϕ. Intuitively, a run of A S,ϕ on an input strategy tree ξ, proceeds by simulating an unwinding of the module M S , pruned at each step according to the strategy ξ; copies of the automaton simulating nodes in the computation tree of M S that are indistinguishable by the environment are sent to the same direction in the input tree. The resulting run tree of A S,ϕ on ξ is essentially a replica of the composition M S ⊳ ξ, and the fact that it satisfies the formula ϕ is checked on the fly by employing in A S,ϕ the usual alternating-automata approach for µ-calculus model checking. In the full computation tree of M S , the set of directions is G = {(q, β) | ((p, α), (q, β)) ∈ R for some p, α and β}. Since in S the pushdown store is completely visible to the environment, the set of directions of the input strategy trees is D = {(vis(q), β) | ((p, α), (q, β)) ∈ R for some p, q, α and β}.

Finally, due to the fact that all copies of the automaton sent to direction (vis(q), β) push β into the pushdown store, the resulting automaton A S,ϕ is semi-alternating. As in [START_REF] Kupferman | An Automata-Theoretic Approach to Branching-Time Model Checking[END_REF] we are going to use a function split to avoid the problem of having states with a component in cl(ϕ) that is a disjunction or a conjunction. Without the use of split, a run of the automaton may have no states that correspond to a fixpoint sub-formula of ϕ that is part of a conjunction or 4 A graded µ-calculus formula is guarded if for every variable y, all the occurrences of y that are in a scope of a fixpoint modality λ are also in the scope of a graded modality that is itself in the scope of λ. For example, the formula νy.(p ∨ [0]y) is guarded, but the formula νy.(p ∨ y) is not. Given a graded µ-calculus formula, we can construct in linear time an equivalent guarded formula (see [START_REF] Kupferman | An Automata-Theoretic Approach to Branching-Time Model Checking[END_REF] for a proof for µ-calculus, which is easily extendible to the graded setting). Accordingly, we assume that all formulas are guarded. This is essential for the correctness of our construction (it guarantees that transitions involving fixpoint formulas are well defined).

a disjunction, which makes it impossible to correctly define the acceptance condition.

We formally define A S,ϕ = {⊤, ⊥}, D, Γ, Q ′ , q ′ 0 , ♭, δ ′ , F , where

-Q ′ = (Q × (cl(ϕ) ∪ {p ⊤ }) × {∀, ∃} × {p e , p s }) ∪ {q ′ 0 }.
States with the component p ⊤ are used to check that the composition of M S with the strategy is deadlock-free, while states with a component in cl(ϕ) check that this composition satisfies ϕ. The components p e and p s are used to flag that the currently simulated node, of the computation tree of M S , is a child of an environment or a system node, respectively. Clearly, the simulation should respect the strategy pruning specifications only if they correspond to children of environment nodes; that is, only if the current state q contains p e . Every state is either in an existential or a universal mode, as specified by the ∀ and ∃ components. When the automaton is in a universal state (q, ϕ, ∀, p e ) with a pushdown store content α, it accepts all strategies for which (q, α) in M S is either pruned or satisfies ϕ (where p ⊤ is satisfied iff the root of the strategy is labeled ⊤). When the automaton is in an existential state (q, ϕ, ∃, p e ) with a pushdown store content α, it accepts all strategies for which (q, α) in M S is not pruned and satisfies ϕ.

-δ ′ is a function δ ′ : Q ′ × Σ × Γ ♭ → B + (D × Q ′ × Γ * ♭ )
. Before giving the formal definition, we show an example. Consider, a transition from the configuration ( p, ∀Xψ, ∃, p e , γ • α), where (p, γ) ∈ Env. First, if the transition to (p, γ • α) is disabled (that is, the automaton reads ⊥), then, as the current mode is existential, the run is rejecting. If the transition to (p, γ • α) is enabled, then the successors of (p, γ • α) that are enabled should satisfy ψ. Note that all the successors of (p, γ • α) that are indistinguishable by the environment are sent by the automaton to the same direction v. This guarantees that either all these successors are enabled by the strategy (in case the letter to be read in direction v is ⊤) or all are disabled (in case the letter in direction v is ⊥). In addition, since the requirement to satisfy ψ concerns only successors of (p, γ • α) that are enabled, the mode of the new states is universal. The copies of A S,ϕ that check the composition with the strategy to be deadlockfree guarantee that at least one successor of (p, γ • α) is enabled. As noted earlier, the enable/disable instructions of the strategy are ignored in every configuration (p, γ • α) that is a successor of a system configuration. Also note that since we assume that no configuration in M S has no successors, the conjunctions and disjunctions in δ ′ cannot be empty. We now formally define the transition function δ ′ . For (p, γ • α) ∈ W , we define the set of successors of (p, γ • α) in M S , to be s(p, γ) = {(q, β) | ((p, γ), (q, β)) ∈ δ}. The transition function δ ′ : Q ′ ×Σ×Γ ♭ → B + (D×Q ′ ×Γ * ♭ ) is defined as follows. In the rules below, for the sake of succinctness, we consider m ∈ {∃, ∀}×{p e , p s }, h ∈ AP ∪{true, false}. Also, given a transition from ( p, ψ, m , ⊤, γ), we let p x = p e if (p, γ) ∈ Env and p x = p s , otherwise.

-δ ′ (q ′ 0 , ⊥, ♭) = false and δ ′ (q ′ 0 , ⊤, ♭)= δ ′ ( q 0 , p ⊤ , ∃, p s , ⊤, ♭) ∧ δ ′ ( q 0 , ϕ, ∃, p s , ⊤, ♭).

Finally, we show that A S,ϕ is semi-alternating. It is sufficient to show that for every (t, β) ∈ D, σ ∈ Σ, p, p ′ ∈ Q ′ , and γ ∈ Γ , if ((t, β), p ′ , β ′ ) appears in δ ′ (p, σ, γ) then β = β ′ . To see that, notice that ((t, β), p ′ , β ′ ) appears in δ ′ (p, σ, γ) only if vis(q, β ′ ) = (t, β), for some q ∈ Q. Since by definition (because the pushdown store is completely visible) we have that vis(q, β ′ ) = (vis(q), β ′ ), and we are done. ⊓ ⊔ Theorem 2 implies that M S |= r ψ iff the language of the automaton A S,¬ψ is empty. We can now show the main result of the paper.

Theorem 3. Given an OPD S and a formula ϕ, the pushdown module checking problem with imperfect state information is 2Exptime-complete if ϕ is a propositional or a graded µ-calculus formula, and 3Exptime-complete if ϕ is a CTL * formula.

Proof. The lower bound follows from the known bound for pushdown module checking with perfect information (see [START_REF] Ferrante | Enriched µ-calculus pushdown module checking[END_REF] for propositional and graded µ-calculus, and [START_REF] Bozzelli | Pushdown module checking[END_REF] for CTL * ). For the upper bound, by Theorem 2, it is enough to check that A S,¬ϕ is empty. Recall that when considering propositional and graded µ-calculus (resp. Let M S = AP, W s , W e , w 0 , R, L, ∼ = be the module induced by S. Observe that the set of directions of the strategy trees that are the input of A S,¬ϕ is D = {(vis(q), β) | ((p, α), (q, β)) ∈ R for some p, q, α and β}, and it is bounded from above by |S|. By Corollary 1, the emptiness of A S,¬ϕ can be decided in time double exponential in |D|nk. Thus, deciding if M S |= r ϕ can be done in time double-exponential in |S| * |ϕ| when considering propositional and graded µ-calculus, and triple-exponential in |S| * |ϕ| when considering CTL * . ⊓ ⊔

  CTL * ) A S,¬ϕ is a PD-SPT with n = O(|S| * |ϕ|) (resp. n = O(|S| * 2 |ϕ|) ) states, and index k = O(|ϕ|).

The graded µ-calculus extends the propositional µ-calculus by allowing graded modalities, which enable statements about the number of successors of a state.

Since the emptiness problem of the intersection of two context free languages is undecidable[START_REF] Hopcroft | Introduction to Automata Theory, Languages and Computation[END_REF], the emptiness problem of alternating pushdown automata is undecidable, already in the case of finite words.

The translation used in[START_REF] Aminof | Pushdown module checking with imperfect information[END_REF], for semi-alternating pushdown Büchi tree automata, made a crucial use of the Büchi acceptance condition, and can not be extended to the parity acceptance condition.

Acknowledgment. The first and third author wish to thank Nir Piterman for useful discussions.

-For all p, ψ, and γ, we have δ ′ ( p, ψ, ∀, p e , ⊥, γ) = true and δ ′ ( p, ψ, ∃, p e , ⊥, γ) = false. -For all p, ψ, and γ, we have δ ′ ( p, ψ, ∀, p s , ⊥, γ) = δ ′ ( p, ψ, ∀, p s , ⊤, γ) and δ ′ ( p, ψ, ∃, p s , ⊥, γ) = δ ′ ( p, ψ, ∃, p s , ⊤, γ). -δ ′ ( p, p ⊤ , m , ⊤, γ) = ( (q,β)∈s(p,γ) (vis(q, β), q, p ⊤ , ∃, p x , β))∧ ( (q,β)∈s(p,γ) (vis(q, β), q, p ⊤ , ∀,

The definition of the function split :

-It remains to define the acceptance condition F . Let d be the maximal alternation level of (fixpoint) sub-formulas of ϕ. Denote by G i the set of all ν-formulas in cl(ϕ) of alternation level i. Denote by B i the set of all µ-formulas in cl(ϕ) of alternation depth less than or equal to i. Now, F = {F 0 , F 1 , . . . , F 2d }, where F 0 = ∅ and for every 1 ≤ i ≤ d we have F 2i-1 = F 2i-2 ∪(Q×B i ×{∀, ∃}×{p e , p s }), and F 2i = F 2i-1 ∪(Q×G i ×{∀, ∃}×{p e , p s }).

Clearly,

Since by the definition of PD-SPT a path π of a run r is accepting if the minimal i with Inf(π) ∩ F i = ∅ is even, by our definition of F , such an index i corresponds to the outermost fixpoint formula that was visited infinitely often. Thus, the acceptance condition makes sure that, if a fixpoint formula is visited infinitely often, then this is a greatest fixpoint formula, and that all of its least fixpoint super-formulas are visited only finitely many times.

Let us now discuss the size of A S,ϕ . It is easy to see that |Q


L Houssin

S Lahaye

J.-L Boimond
email: jean-louis.boimond@istia.univ-angers.fr

† S Lahaye

Control of (max, +)-linear systems minimizing delays

Introduction

In this paper, we study Discrete Events Dynamic Systems (DEDS) that can be modeled by a linear representation on (max, +) algebra. This class corresponds to Timed Event Graphs (TEG). A linear system theory has been developed for these particular systems in [START_REF] Baccelli | Synchronization and Linearity[END_REF]. Strong analogies then appear between the classical linear system theory and the (max, +)-linear system theory. Some control problems for these systems have previously been tackled. In all these works, the problematic was to compute an optimal solution in regard to the just-in-time criterion, indeed the proposed control laws satisfy some given control objectives while delaying as much as possible occurrences of input or internal events. In [START_REF] Cottenceau | Model reference control for timed event graphs in dioids[END_REF], the authors compute a greatest feedback controller (which enables to delay as much as possible occurrences of input or internal events) in order that the controlled system behaves as close as possible to a given reference model.

For our concern, the aim of the control is to delay as less as possible the system while ensuring some given specifications. A first study of this problem is [START_REF] Houssin | Control of constrained (max, +)-linear systems minimizing delays[END_REF]. For example, in a railway network, one can aim at limiting the number of trains in a path while minimizing the induced delays. Another possible application concerns production systems subject to critical time constraints, in which sojourn times of pieces must not exceed a given value at some stages. We may then be interested at bounding the sojourn times while delaying as less as possible the system. We consider two control structures: the control is firstly formalized as a state feedback on state and then as a state feedback on inputs.

Originalities of this paper lies in the considered criterion (minimization of delays instead of just-in-time), the specification of the control objective (constraints instead of reference model) and the approach for the controller synthesis (new results on fixed points of antitone mappings, instead of residuation theory used in previous papers about control of (max, +)-linear systems).

In section 2, we recall some results from the dioid theory and introduce results concerning isotone and antitone mappings. Section 3 is devoted to the modeling of DEDS. The proposed control laws are presented in section 4.

Algebraic tools 2.1 Dioid theory

A dioid (D, ⊕, ⊗) is a semi-ring in which the sum, denoted ⊕, is idempotent. The sum (resp. product) admits a neutral element denoted ε (resp. e). A dioid is said to be complete if it is closed for infinite sums and if product distributes over infinite sums too. The sum of all its elements is generally denoted ⊤ (for top).

Example 1

The set Z max = (Z ∪ {-∞}) endowed with the max operator as sum and the classical sum as product is a (non-complete) dioid. If we add ⊤ = +∞ (with convention

⊤ ⊗ ε = +∞ + (-∞) = -∞ = ε) to this set, the resulting dioid is complete and is denoted Z max .
Due to the idempotency of the sum, a dioid is endowed with a partial order relation, denoted and defined by the following equivalence: a b ⇔ a = a ⊕ b. A complete dioid has a structure of complete lattice [1, §4], i.e., two elements in a complete dioid always have a least upper bound, namely a ⊕ b, and a greatest lower bound denoted a ∧ b = {x|x a, x b} x in the considered dioid.

Let D and C be two complete dioids. A mapping f :

D → C is said to be isotone (resp. antitone) if a, b ∈ D, a b ⇒ f (a) f (b) (resp. f (a) f (b)).

Residuation theory

Residuation theory [START_REF] Blyth | Residuation Theory[END_REF] defines "pseudo-inverses" for some isotone mappings defined over ordered sets such as complete dioids [START_REF] Cohen | Residuation and Applications[END_REF]. More precisely, if the greatest element of set {x ∈ D|f (x) b} exists for all b ∈ C, then it is denoted f ♯ (b) and f ♯ is called residual of f . Dually, one may consider the least element satisfying f

(x) b, if it exists for all b ∈ C, it is denoted f ♭ (b) and f ♭ is called dual residual of f . Example 2 The mapping T a : D → D; x → a ⊕ x is dually residuated (proof is available in [1, §4.4.4]). The dual residual is denoted T ♭ a (b) = b • -a. It should be clear that a b ⇔ T ♭ a (b) = ε. If T a is defined over Z max then T ♭ a (b) = b if b > a, ε otherwise.
We recall the following property of T ♭ a which is usefull later :

a(x • -b) ax • -ab. (1)
A relevant remark is that although

T ♭ a (x) = x • -a is isotone, the mapping x → a • -x is antitone since x 1 x 2 ⇔ a • -x 1 a • -x 2 ∀a.
It should be clear that a • x 1 is the least solution of x 1 ⊕ x a and a • x 2 is the least solution of x 2 ⊕ x a (see [1, 4.4.4] for more details).

Fixed points of mappings defined over dioids

Because of their lattice structure, properties about fixed points stated for lattices also apply over dioids.

Notation 1 Let f : D → D with D a complete dioid, we use the following notations:

F f = {x ∈ D|f (x) = x}, P f = {x ∈ L|f (x) x}, Q f = {x ∈ D|f (x) x} and f 2 denotes f • f .
For an isotone mapping f , [START_REF] Tarski | A lattice theorical fixed point theorem and its applications[END_REF] and [START_REF] Cousot | Constructive versions of Tarski's fixed point theorems[END_REF] have shown that sets F f , P f and Q f are nonempty complete lattices. Moreover, it can be shown that the greatest (resp. least) fixed point coincides with the greatest (resp. least) element of P f (resp. Q f ):

Sup P f = Sup F f and Sup F f ∈ F f , Inf Q f = Inf F f and Inf F f ∈ F f . ( 2
)
A lattice is depicted in fig. 1. We represent sets F f , P f and Q f for an isotone mapping f . In the following proposition given without proof, we specify to dioids a well known method to compute the greatest fixed point of an isotone mapping f . Proposition 1 If the following iterative computation

y 0 = ⊤ y k+1 = f (y k ) (3)
converges in a finite number k e of iterations, then y ke is the greatest fixed point of f .

Concerning antitone mappings, properties about fixed points are not that well established, and only few works have tackled this problem [START_REF] Baclawski | Fixed points in partially ordered sets[END_REF], [START_REF] Rade | On fixed edges of antitone self-mappings of complete lattices[END_REF]. To the best of our knowledge, results presented in the sequel are original. However, proposition 6 has been inspired by [7, th. A].

Notice that if f is an antitone mapping then f 2 is isotone. Let us first characterize the structure of P f and Q f . Proposition 2 Let f : D → D be an antitone mapping. Set Q f (resp. P f ) is a complete upper semi-lattice (resp. complete lower semi-lattice).

Proof: Let us consider two elements x, y ∈ Q f , we have f (x⊕y) f (x)∧f (y) f (x)⊕f (y) x ⊕ y, and so x ⊕ y ∈ Q f . This assertion also applies to infinite sums. Set P f is proved to be a complete lower semi-lattice by identical arguments.

Proposition 3 Let f : D → D be an antitone mapping and x ∈ D. We have

x ⊕ f (x) ∈ Q f , x ∧ f (x) ∈ P f . Proof: f (x) ⊕ x x f (x) ⊕ x f (x)
which implies by antitony of f

f (f (x) ⊕ x) f (x) f (x) ⊕ x. Respectively, f (x) ∧ x ∈ P f since f (f (x) ∧ x) f (x) f (x) ∧ x.
Proposition 4 Let f : D → D be an antitone mapping, y ∈ P f and z ∈ Q f . For all x ∈ D such that x y (resp.

x ′ ∈ D such that x ′ z), we have x ∈ P f (resp. x ′ ∈ Q f ).
The proof is based on the antitony of f :

x y ⇒ f (x) f (y) y x x ′ z ⇒ f (x ′ ) f (z) z x ′ Proposition 5 If x is a fixed point of an antitone mapping f : D → D, then x is a minimal (resp. maximal) element of Q f (resp. P f ). Proof: Let x ∈ F f , y ∈ P f and z ∈ Q f such that y x z. Using antitony of f , we obtain f (y) f (x) f (z) ⇒ y f (y) x f (z) z hence y = x = z.
We conclude that there is no element of Q f (resp. P f ) which is less (resp. greater) than x.

As a corollary of this proposition, notice that if f admits several distinct fixed points, then they are not comparable. Furthermore, remark that set F f can be empty.

Proposition 6 Let f : D → D be an antitone mapping. Denoting u = Inf F f 2 and v = Sup F f 2 , we have u ∈ P f and v ∈ Q f . Proof: We show that f (u) = v and f (v) = u (since u v by definition, this proves f (u) u and f (v) v). The expression of f (u) leads to f (u) = f ( x∈F f 2 x) x∈F f 2 f (x) (f antitone ⇒ f (a ∧ b) f (a) ⊕ f (b)). However, elements of {f (x)|x ∈ F f 2 } are fixed points of f 2 too since f 2 (f (x)) = f (f 2 (x)) = f (x). So we can deduce that f |F f 2 is
a permutation, it can be proved by considering x, y ∈ F f 2 , x = y and f (x) = f (y), we would obtain f 2 (x) = f 2 (y) and so x = y which is a contradiction. So last inequality can be rewritten:

f (u) y∈F f 2 y = v.
We previously remark that f (x) with x ∈ F f 2 is a fixed point of f 2 so does f (u) and it leads to f (u) = y∈F f 2 y = v. From last equality, we obtain also

f (f (u)) = u = f (v).
We illustrate the study of sets F f , P f and Q f for an antitone mapping f in fig. 2.

Figure 2: Hasse diagram of sets Q g , P g , F g and F g 2 for an antitone mapping g.

Remark 1

For the following control problem, we are interested in the computation of minimal elements of Q f . The element v, which can be computed using proposition 1, constitutes an interesting approximation since any x ∈ F f , minimal element of Q f (see proposition 5), is such that u x v (since x also belongs to F f 2 ). As mentioned in the following corollary, v may sometimes be the "best approximation".

Corollary 1 If v = u, then F f = {v} and v is a minimal element of Q f .
3 Modeling DEDS using dioids

State and transfer representation

Dioids enable one to obtain linear models for DEDS which involve (only) synchronization and delay phenomena (but not choice phenomena). It corresponds to the class of DEDS which can be modeled by Timed Event Graphs (TEG). The behavior of such systems can be represented by some discrete functions called dater functions (see [START_REF] Baccelli | Synchronization and Linearity[END_REF]). More precisely, a discrete variable x(•) is associated to an event labeled x (firing times of transition labeled x in the corresponding TEG). This variable represents the occurring dates of event x. Notice that a dual representation for these DEDS is called counter representation and it manipulates variables depending on time which represent the cumulated number of firings of transition x.

The considered DEDS can be modeled by a linear state equation

x(k) = Ax(k -1) ⊕ Bu(k), (4)
where x and u are the state and the input vectors.

An analogous transform to Z-transform (used to represent discrete-time trajectories in conventional theory) can be introduced for DEDS considered here: the γ, δ-transform. This transform enables to manipulate formal power series, with two commutative variables γ and δ, representing daters trajectories. The set of these formal series is a complete dioid denoted M ax in γ, δ with e = γ 0 δ 0 as neutral element of product and ε = (γ -1 ) * (δ 1 ) * as neutral element of sum (the construction of this dioid is detailed in [START_REF] Baccelli | Synchronization and Linearity[END_REF]). In the following, we denote x the corresponding element of {x(k)} k∈Z in M ax in γ, δ and we assume that each x ∈ M ax in γ, δ is represented by its minimum representative (see [1, §5]).

In M ax in γ, δ , state representation (4) becomes

x = Ax ⊕ Bu, (5)
in which entries of matrices A and B are elements of M ax in γ, δ . Considering the earliest functioning rule (an event occurs as soon as possible), we select the least solution given by x = A * Bu with A * = i∈N A i [1, Th 4.75], and A * B corresponds to the transfer between u and x.

Assumption 1 Afterwards, we assume that the input matrix B is a diagonal square matrix with entries equal to e or ε. This assumption is not restrictive since it can always be satisfied by extending the state vector. Remark that the assumed structure of B is such that B Id and B n = B for n ≥ 1.

Causality and causal upper approximation

Variables x ∈ M ax in γ, δ used to model TEG have the causality property [START_REF] Baccelli | Synchronization and Linearity[END_REF].

Definition 1 Let x ∈ M ax in γ, δ ,
x is said to be causal if either x = ε or all exponents of x are in N. A matrix is said causal if its entries are all causal. The set of causal elements of

M ax in γ, δ is a complete dioid denoted M ax+ in γ, δ .
Considering a TEG, a causal transfer means that the system does not require any anticipation (time or event). We now introduce the notion of causal upper approximation (see [9, §2.4]).

Proposition 7 Let x ∈ M ax in γ, δ . The two following assertions are equivalent:

(i) x has no negative exponent in γ, (ii) there exists a least x ′ ∈ M ax+ in γ, δ such that x ′ x. It means that x admits a causal upper approximation.

Proof: If x is causal, the demonstration is obvious and x ′ = x. We now consider x not causal. We can limit the proof to the case of monomials since a series is nothing more than a sum of monomials.

(i)⇒(ii) : Let x = γ n δ t , with n 0 and t < 0. It is easy to see that the monomials γ n δ 0 is the least element of M ax+ in γ, δ such that x ′ x. So, x ′ = γ n δ 0 . (ii)⇒(i) : If there exists a least x ′ ∈ M ax+ in γ, δ such that x ′

x with x ′ = γ n ′ δ t ′ and x = γ n δ t , we have n ′ ≤ n and t ′ ≥ t. However x ′ ∈ M ax+ in γ, δ , so n ′ ≥ 0 and we obtain n ≥ 0.

We can remark that proposition ( 7) is also available for matrix. We now demonstrate that if an element x admits a causal upper approximation then every element less than x admits a causal approximation too.

Corollary 2 Let x be an element of M ax in γ, δ which admits a causal approximation. Every element y such that y x admits also a causal approximation.

Proof: The series x can be rewritten x = i∈I γ n i δ t i . Since x admits a causal approximation, we have ∀i ∈ I, n i 0, in other words, min i∈I n i 0. If y = j∈J γ n ′ j δ t ′ j is such as x y, we obtain min j∈J n ′ j min i∈I n i and so ∀j ∈ J, n ′ j 0. We conclude that y has no negative exponent in γ and consequently y admits a causal approximation.

Controllers synthesis for constrained systems 4.1 Problem statement

Considering DEDS modeled by their state equation ( 5), we are interested here in the design of a "state feedback" controller for (max, +)-linear systems.

More precisely, if we consider a DEDS modeled by a TEG, then the feedback controller can be realized by another TEG merged on the initial ones. In this controlled TEG, the additional arcs due to the controller authorize or prohibit the firing of the controlled transitions (see figure 5). This control structure is comparable with some Petri nets methods for controlled DEDS [START_REF] Holloway | A survey of petri net methods for controlled discrete event systems[END_REF].

Synthesis of controllers for DEDS in dioids has previously been tackled in many papers ( [START_REF] Cottenceau | Model reference control for timed event graphs in dioids[END_REF], [START_REF] Maia | Optimal closed-loop control for timed event graphs in dioid[END_REF] is a non exhaustive list). In all these works, authors focus on just-in-time model reference control, that is, the synthesis of a feedback which delays as much as possible events in the system (i.e. the greatest feedback) such that the controlled system is not slower than a reference model. In this paper, the control objective is different :

• we aim at ensuring some given constraints on state (rather than satisfying a reference model matching) for all input u. These constraints are defined by a matrix φ and are formulated as the implicit inequality :

φx x, ∀u. (6)
• we search a feedback which delays as less as possible the functioning of the system (rather than the just-in-time criterion). More precisely, we aim at computing the least feedback such that the state of the controlled system satisfies the constraints given by ( 6).

In the following, we illustrate three constraints which can be imposed on the controlled systems as an inequality [START_REF] Cousot | Constructive versions of Tarski's fixed point theorems[END_REF]. Next, we consider two controller structures. We remind that, for some conditions, a state feedback on state controller is appropriate [START_REF] Houssin | Control of constrained (max, +)-linear systems minimizing delays[END_REF][START_REF] Houssin | Contributions à la commande des systèmes (max,+)-linéaires[END_REF]. We also show that, for some conditions on the specifications, a state feedback on the inputs of the system fits to the problem.

Constraints specification

We now detail three kinds of constraints for DEDS described by a TEG, that can be formulated as an inequality (6):

• Some inner variables can be subject to a minimum time separation between two firings. For a state variable x i and a time separation denoted ∆ min , we claim that x i (k + 1) ∆ min x i (k). Then, the counterpart of this constraint in M ax in γ, δ is γδ ∆ min x i x i .

• We can also aim at bounding the sojourn times of tokens in given paths of the TEG (critical time constraints). Let us consider a path from transition x i to transition x j containing initially α tokens, we denote τ the desired maximum sojourn time in this path. This imposes x j (k + α)x i (k) τ , which can be formulated in M ax in γ, δ by γ -α δ -τ x j x i .

• We may also limit the number of tokens in paths of the TEG. Let us consider a path from x i to x j containing initially α tokens, we denote κ the desired maximum number of tokens in this path. This constraint can be specified by: κ x i (t)x j (t) + α, which leads in M ax in γ, δ to γ κ-α x j x i . In this structure, a controller denoted F , is added between internal states (see figure 3). This particular structure is not usual in control theory, but has a specific interest for DEDS (e.g. the state feedback on state controller has been considered in [START_REF] Lüders | Generalized multivariable control of discrete event systems in dioid[END_REF]).

Synthesis of a state feedback on state controller 4.3.1 Formalization

In fact, if we assume that internal events are measurable, controller F uses this measure to possibly delay occurrences of some internal events.

The state evolution is then described by

x = Ax ⊕ F x ⊕ Bu. ( 7
)
The least solution of this equation which corresponds to the earliest functioning, is given by x = (A ⊕ F ) * Bu. From ( 7), the state of controlled system is s.t.

x Ax ⊕ Bu.

Furthermore, as control objective, we aim at satisfying (6), then

x (A ⊕ φ)x ⊕ Bu.
Since we aim at delaying as less as possible the system, we seek the least controlled state x, that is the least x greater than the least solution x (A ⊕ φ) * Bu. The problem can then be formulated as the search for a least feedback F such that

(A ⊕ F ) * Bu (A ⊕ φ) * Bu, ∀u ⇔ (A ⊕ F ) * B (A ⊕ φ) * B. (8)
Some constraints may be unsuitable, that is, there may not exist a causal feedback enabling to satisfy these constraints. The following proposition furnishes a test on given constraints φ, stating a necessary and sufficient condition for the existence of a causal feedback.

Proposition 8 There exists a causal feedback F satisfying (8) if and only if each entry of (A ⊕ φ) * B has no negative exponent in γ. We then denote G the upper causal approximation of (A ⊕ φ) * B.

Proof: According to proposition 7, there exists a least causal matrix G such that G (A⊕φ) * B if and only if each entry of (A ⊕ φ) * B has no negative exponent in γ. It is always possible to find a causal matrix F such that (A ⊕ F ) * G. Furthermore, by isotony of product, we have

GB (A ⊕ φ) * B 2 = (A ⊕ φ) * B since B 2 = B (see assumption 1)
. The product GB is causal (since G and B are causal) and G is the least causal matrix such that G (A ⊕ φ) * B, so we claim that GB G. However B Id, one has that GB G. Therefore, and since B is causal, there exists a causal F such that (A ⊕ F ) * B GB = G.

Feedback computation

From proposition 8, we aim at computing the least feedback F such that

(A ⊕ F ) * B G (9)
in which G is the upper causal approximation of (A ⊕ φ) * B.

Proposition 9 Solutions of equation ( 9) are elements of Q f (see notation 1) with f :

F → G • -(A ⊕ F ) * .
Proof: We have the following equivalences

G (A ⊕ F ) * B ⇔ G (A ⊕ F ) * since GB = G (see proof of prop. 8) and B Id (ass. 1) ⇔ G (A ⊕ F ) * ⊕ F since (A ⊕ F ) * F ⇔ G • -(A ⊕ F ) * F since T (A⊕F ) * is dually residuated (cf. ex.2)
Notice that mapping f is antitone. From proposition 6, the element v = Sup F f 2 (which can be computed using proposition 1) belongs to Q f and is then a feedback satisfying [START_REF] Houssin | Contributions à la commande des systèmes (max,+)-linéaires[END_REF]. From corollary 1, v is a minimal element of Q f (i.e. a minimal feedback satisfying ( 9)) if v = u. Otherwise, as mentioned in remark 1, v can be used to approximate a minimal feedback satisfying (9).

Synthesis of a state feedback on inputs controller 4.4.1 Formalization

In previous section, the designed controller requires that every state variables are controllable. This assumption is not needed in the case of a state feedback on the inputs of the system. This kind of controller implies that the delayed events are only the inputs one. The concerned variables are the ones belonging to the set U c = {u i |B ii = e} .

By considering the earliest functioning rule, the transfer relation of such controlled system is

x c = (A ⊕ BF ) * Bv = H c v. (10)
The figure 4(b) describes the controlled system. Figure 4: s tate feedback on inputs controller.

Remark 2

The assumption 1 implies that the feedback on inputs has an effect on the state variables directly controllable, i.e. state variables x i such that B ii = e. These state variables x i are such that x i = u i since there is no shift between them. We denote X c = {x i |B ii = e} this set.

From [START_REF] Houssin | Control of constrained (max, +)-linear systems minimizing delays[END_REF], it is obvious that the state of the controlled system is such that

x c A * Bv ∀v.
Furthermore, x c should satisfy the control objective (6), i.e. x c φx c , then

x c A * Bv ⊕ φx c ∀v.
We aim at delaying as less as possible the system, therefore we seek the least controlled x c given by x c φ * A * Bv ∀v.

Using [START_REF] Houssin | Control of constrained (max, +)-linear systems minimizing delays[END_REF], we then seek the least feedback F such that

(A ⊕ BF ) * Bv φ * A * Bv ∀v ⇔ (A ⊕ BF ) * B φ * A * B. (11)
We can easily prove that ( 11) is equivalent to

(A ⊕ BF ) * B φ + A * B, (12) since
(A ⊕ BF ) * B φ + A * B ⇒ (A ⊕ BF ) * B ⊕ A * B φ + A * B ⊕ A * B ⇔ (A ⊕ BF ) * B φ * A * B.
Assumption 2 The matrix of constraints φ is supposed to satisfy Bφ = φ. This assumption comes down to formulating all constraints φ ij x j x i (see §4.2) such that x i ∈ X c .

The following proposition gives a necessary and sufficient condition on given constraints φ for the existence of a causal feedback satisfying [START_REF] Maia | Optimal closed-loop control for timed event graphs in dioid[END_REF].

Proposition 10 There exists a causal feedback F satisfying [START_REF] Maia | Optimal closed-loop control for timed event graphs in dioid[END_REF] if, and only if φ + A * B admits a causal upper approximation. If it exists, the causal upper approximation is denoted G.

Proof:

⇒ If a causal feedback F exists, then (A ⊕ BF ) * B is also causal (since A and B are causal).

We can state from corollary 2 and (12) that φ + A * B admits a causal upper approximation.

⇐ If φ + A * B admits a causal upper approximation, then one can find a causal element X such that X φ + A * B. Since B 2 = B and Bφ + = B(φ ⊕ φφ ⊕ ...) = φ + (by assumption Bφ = φ), we have

(⇐) F B(G • -(A ⊕ BF ) * ) ⇒ BF B 2 (G • -(A ⊕ BF ) * ) ⇒ BF B(G • -(A ⊕ BF ) * ) ⇒ BF BG • -B(A ⊕ BF ) * (since a(x • -b) ax • -ab) ⇒ BF BG • -(A ⊕ BF ) * (x → a • -x is antitone) ⇒ BF G • -(A ⊕ BF ) * ( BG = G).
The computation of v = Sup F g 2 furnishes a feedback ensuring [START_REF] Maia | Optimal closed-loop control for timed event graphs in dioid[END_REF] since v ∈ Q g (see propos. 6).

Example

We consider the DEDS modeled by the TEG of fig. 5, and represented by the following matrices:

A =           ε ε ε ε ε ε ε δ 3 γ 3 δ ε ε ε ε ε ε ε ε ε ε ε ε ε ε δ ε ε ε ε ε ε ε γδ 5 ε ε ε ε δ 4 ε ε γ 2 δ 2 γδ 2 ε ε ε ε ε ε δ 3 ε          
, and B is a diagonal matrix s.t.

B ii = e if i ∈ {1, 3}, ε otherwise.
In a first place, we aim at illustrating that all constraints defined as in §4.2, are not suitable. For example, we can not impose that tokens sojourn less than 2 time units in the place between transitions x 5 and x 6 for all input. In fact, if transition u 1 is not fired, then initial tokens will not be removed from this place, and we can not find any relevant feedback. As stated in proposition 8, the computation of (A ⊕ φ) * B enables to detect this unsuitable constraint since it contains an entry with a negative exponent in γ.

We now consider suitable constraints:

• tokens must not sojourn more than 4 time units in the place between transitions x 2 and x 6 , then δ -4 x 6 x 2 ,

• the number of tokens between x 5 and x 4 must not exceed 3, so γ 2 x 5 x 4 .

We have

φ =           ε ε ε ε ε ε ε ε ε ε ε ε δ -4 ε ε ε ε ε ε ε ε ε ε ε ε γ 2 ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε           . 4.
F = v =           ε ε ε ε ε ε ε γδ 5 (γδ 2 ) * ε γ 3 δ 4 (γδ 2 ) * ε ε ε ε ε ε ε ε ε ε ε ε ε γ 3 δ 6 (γ 3 δ 5 ) * ε ε ε ε ε ε γ 4 δ 11 (γ 3 δ 5 ) * ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε          
which satisfies both constraints. A realization of this controller is represented in thin lines on fig. 5. Let us note that, for this example, we have v = u, and we hence can not argue thanks to corollary 1 that v is a minimal feedback. It can be checked that there exists a relevant feedback F ′ , defined by F ′ ij = v ij for (i, j) = (5, 3) and F ′ 53 = ε, which is less than v. Nevertheless, let us point out that the controlled system with F ′ has the same transfer as the controlled system with v. This observation reinforces our suggestion that v constitutes a good approximated solution for our control problem (see remark 1). Figure 5: A TEG (thick lines) merged with a realization of its state on state feedback controller (thin lines)

The state feedback on inputs case

In the case of the state feedback on inputs, the new constraint matrix φ ′ must ensure assumption 2. Therefore, we have to adapt constraints from §4.5. With that aim, we consider constraints described as the following.

• Tokens must not sojourn more than 7 time units in the path the path between transition

x 1 and transition x 7 . Consequently, tokens can't remain more than 4 time units in the place between transitions x 2 and x 6 .

• The number of tokens in the path from x 3 to x 5 must not exceed 3. It follows to the limitation of the place between x 4 and x 5 to 3 tokens.

We have

φ ′ =           ε ε ε ε ε δ -7 ε ε ε ε ε ε ε ε ε ε ε ε γ 2 ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε          
.

The computation of the state feedback on inputs yields

F ′ =           γδ 2 (γδ 2 ) * ε γ 3 δ(γδ 2 ) * ε ε ε ε ε ε ε ε ε ε ε ε ε γ 3 δ 6 ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε ε           .
A realization of F ′ is given in fig. 6. It's worth mentioning that, if we consider x 7 as the output of the system, the transfer of the controlled system is the same for the two controllers since

Conclusion

We have presented a new control problem in (max, +)-linear system theory: ensure some given constraints while delaying as less as possible the system. Using results on antitone and isotone mappings, two state feedback structures are proposed. However, it must be noted that the obtained controllers are not necessarily minimal. In the near future, we will focus on improvements of our control approach in that sense. We also plan to consider TEG with uncontrollable transitions and non linear constraints.

Figure 1 :

 1 Figure 1: Hasse diagram and sets F f , P f and Q f for an isotone mapping f .

Figure 3 :

 3 Figure 3: state feedback on state controller

( 11 )

 11 ⇒ (12) : φ * A * B φ + A * B, and (11) ⇐ (12) :

C

  (A ⊕ BF ′ ) * B = C(A ⊕ F ) * B = δ 10 (γδ 2 ) * γ 3 δ 11 (γδ 2 ) * , with C = ε ε ε ε ε ε e .

Figure 6 :

 6 Figure 6: A TEG (thick lines) merged with a realization of its state on inputs feedback controller (thin lines)

  5.1 The state feedback on state case According to §4.3.2, we can compute the following state feedback on state

which proves that a causal feedback (here denoted X) satifying ( 12) exists.

Corollary 3

The causal upper approximation G, if it exists, is such that GB = G and BG = G.

Proof:

We first demonstrate that GB = G. Since B Id, we have GB G. From proposition 10, G is such that G φ + A * B and we have GB φ + A * B (B 2 = B). GB is causal since G and B are, and as G is the least causal element greater than φ + A * B, we deduce GB G. By the same reasonning, We can easily prove BG = G.

Feedback computation

In this section, we tackle how to compute a solution to [START_REF] Maia | Optimal closed-loop control for timed event graphs in dioid[END_REF].

Proposition 11 Suppose that φ + A * B admits a causal upper approximation denoted G. Solutions of ( 12) are elements of Q g (see notation 1) with g :

Proof: Causal feedbacks we are interested in are such that

For the last equivalence :