5th Asian Computing Science Conference, ASIAN ’99 Proceedings: P.S. Thiagarajan and R. Yap (eds.) Springer Lecture Notes in Computer Science 1742 (1999), 227–238.

Faster Model Checking for Open Systems

Madhavan Mukund^{1}, K. Narayan Kumar^{1}, and Scott A. Smolka^{2}

1 Chennai Mathematical Institute, 92 G.N. Chetty Road, Chennai 600 017, India.

                   E-mail: {madhavan,kumar}@smi.ernet.in

2 Department of Computer Science, State University of New York at Stony Brook, NY 11794-4400, USA. E-mail: sas@cs.sunysb.edu.

Abstract. We investigate Orex, a temporal logic for specifying open systems. Path properties in Orex are expressed using ω-regular expressions, while similar logics for open systems, such as ATL^{∗} of Alur et al., use LTL for this purpose. Our results indicate that this distinction is an important one. In particular, we show that Orex has a more efficient model-checking procedure than ATL^{∗}, even though it is strictly more expressive. To this end, we present a single-exponential model-checking algorithm for Orex; the model-checking problem for ATL^{∗} in contrast is provably double-exponential.

1 Introduction

Reactive systems are computing systems where the computation consists of an ongoing interaction between components. This is in contrast to functional systems whose main aim is to compute sets of output values from sets of input values. Typical examples of reactive systems include schedulers, resource allocators, and process controllers.

Pnueli [Pnu76] proposed the use of linear-time temporal logic (LTL) to specify properties of reactive systems. A system satisfies an LTL specification if all computations of the system are models of the formula. Later, branchingtime temporal logics such as CTL and CTL^{∗} [CE81,EH86] were developed, which permit explicit quantification over computations of a system. For both linear-time and branching-time logics, the model checking problem—verifying whether a given system satisfies a correctness property specified as a temporal logic formula—has been well studied. Model checkers such as Spin for LTL [Hol97] and SMV for CTL [McM93] are gaining acceptance as debugging tools for industrial design of reactive systems.

Alur et al. [AHK97] have argued that linear-time and branching-time temporal logics may not accurately capture the spirit of reactive systems. These logics treat the entire system as a closed unit. When specifying properties of reactive systems, however, it is more natural to describe how different parts of the system behave when placed in contexts. In other words, one needs to specify properties of open systems that interact with environments that cannot be controlled.

A fruitful way of modelling open systems is to regard the interaction between the system and its environment as a game. The system’s goal is to move in such a way that no matter what the environment does, the resulting computation satisfies some desired property. In this formulation, the verification problem reduces to checking whether the system has a winning strategy for such a game.

The alternating temporal logic ATL^{∗} proposed in [AHK97] reflects the gametheoretic formulation of open systems. In ATL^{∗}, the property to be satisfied in each run of the system is described using an LTL formula, and LTL formulas may be nested within game quantifiers. The quantifiers describe the existence of winning strategies for the system. Moreover, a restricted version of ATL^{∗} called ATL has an efficient model-checking algorithm. However, the modelchecking problem for the considerably more expressive logic ATL^{∗} is shown to be 2EXPTIME-complete which compares unfavourably with the PSPACEcompleteness of CTL^{∗}.

In this paper, we propose a logic for open systems called Orex, which is interpreted over Σ-labelled transition systems and uses ω-regular expressions rather than LTL formulas to specify properties along individual runs. As in ATL^{∗}, ω-regular expressions may be nested within game quantifiers. Since ω-regular expressions are more expressive than temporal logics for specifying properties of infinite sequences, our logic is more expressive than ATL^{∗}. Moreover, it turns out that Orex has an exponential-time model checking algorithm, which is considerably better than the complexity of ATL^{∗}.

The paper is organized as follows. Section 2 contains some basic definitions about transition systems and games. Section 3 introduces the syntax and semantics of Orex and gives some examples of how to write temporal specifications in the logic. Section 4 describes an automata-theoretic algorithm for Orex’s model-checking problem. Section 5 discusses related work and Section 6 offers our concluding remarks.

2 Transition Systems, Games, Strategies

Transition systems A Σ-labelled transition system is a tuple T S = ⟨X, Σ, ⟶⟩ where X is a finite set of states, Σ is a finite alphabet of actions and ⟶ ⊆ X ×Σ ×X is the transition relation. We use x, y, … to denote states and a, b, … to denote actions.

An element (x, a, y) ∈ ⟶ is called an a-transition. For S ⊆ Σ, the set of S-transitions is given by ⟶_{S} = {(x, a, y) | a ∈ S}. As usual, we write x ⟶^{a} y to denote that (x, a, y) ∈ ⟶. The set of transitions enabled at a state x, denoted enabled(x), is the set of transitions of the form x ⟶^{a} y that originate at x. To simplify the presentation, we assume that there are no deadlocked states—that is, for each x ∈ X, enabled(x) ≠ ∅.

A path in T S is a sequence x_{0} ⟶^{a_{1}} x_{1} ⟶^{a_{2}} ⋯ x_{i} ⟶^{a_{i+1}} x_{i+1} · · ·. Let paths(T S)

and finite paths(T S) denote the set of infinite and finite paths in T S, respectively. For a finite path p, let last(p) denote the final state of p.

Games and strategies Let S ⊆ Σ. An S-strategy is a function f from finite paths(T S) to the set of S-transitions ⟶_{S} such that for each p ∈ finite paths(T S), f(p) ⊆ enabled(last(p)). If ⟶_{S} ∩ enabled(last(p)) ≠ ∅, we require that f(p) ≠ ∅.

An infinite path ρ = x_{0} ⟶^{a_{1}} x_{1} ⟶^{a_{2}} ⋯ x_{n} ⟶^{a_{n}} ⋯ in paths(T S) is said to be consistent with the S-strategy f if for each n ≥ 1 the transition x_{n−1} ⟶^{a_{n}} x_{n} belongs to the set f(x_{0} ⟶^{a_{1}} ⋯ ⟶^{a_{n−1}} x_{n−1}) whenever a_{n} ∈ S.

A game over T S is a pair (Π, x) where Π is a subset of paths(T S) and x is a state in X. We say that S has a winning strategy for the game (Π, x) if there is an S-strategy f such that every infinite path that begins at x and is consistent with f belongs to Π.

Often, we are interested in restricting our attention to fair computations. An infinite path ρ ∈ paths(T S) is said to be weakly S-fair if there are infinitely many states along ρ where no S-transition is enabled or if there are infinitely many S-transitions in ρ. The path is said to be strongly S-fair if there are only finitely many positions where an S-transition is enabled or if there are infinitely many S-transitions in ρ.

We can relativize our notion of winning strategies to fair paths in the obvious way—S has a weakly (strongly) fair winning strategy for (Π, x) if there is an S-strategy f such that every weakly (strongly) S-fair path that begins at x and is consistent with f belongs to Π.

3 The Logic

3.1 Syntax

Fix an alphabet Σ and a set of propositions Prop. We simultaneously define the sets FPE of finite path expressions, PE of (infinite) path expressions, and Φ of state formulas as follows. We use e to denote a typical element of FPE, α to denote a typical element of PE, and φ to denote a typical element of Φ.

\begin{aligned}e & ::= & φ ∈ Φ | a ∈ Σ | e · e | e + e | e^{∗} \\ α & ::= & e · e^{ω} | α + α \\ φ & ::= & tt | P ∈ Prop | ¬φ | φ ∨ φ | E_{S}α, (S ⊆ Σ) | A_{S}α, (S ⊆ Σ) \end{aligned}

Observe that finite path expressions are just regular expressions whose alphabet may include state formulas. Similarly, path expressions are traditional ω-regular expressions [Tho90] built from finite path expressions. For state formulas, we can use ¬ and ∨ to derive the usual Boolean connectives such as ∧ and ⇒. Finally, note that the wffs of Orex are just the state formulas.

3.2 Semantics

Orex formulas are interpreted over Σ-labelled transitions systems equipped with valuations. Let T S = ⟨X, Σ, ⟶⟩ be a Σ-labelled transition system. A valuation v : X → 2^{Prop} specifies which propositions are true in each state.

We interpret finite path expressions over finite paths in T S, path expressions over infinite paths in T S, and state formulas at states of T S. If p ∈ finite paths(T S) and e ∈ FPE, we write T S, p ⊧ e to denote that e is satisfied along p. Similarly, for ρ ∈ paths(T S) and α ∈ PE, T S, ρ ⊧ α denotes α is satisfied along ρ. Finally, for x ∈ X and φ ∈ Φ, T S, x ⊧ φ denotes that φ is satisfied at the state x.

We define concatenation of paths in the usual way. Let p = x_{0} ⟶^{a_{1}} ⋯ ⟶^{a_{n}} x_{n}

and p′ = x′_{0} ⟶^{a′_{1}} ⋯ ⟶^{a′_{m}} x′_{m} be paths such that x_{n} = x′_{0}. The path p · p′ is the

path x_{0} ⟶^{a_{1}} ⋯ ⟶^{a_{n}} x_{n} ⟶^{a′_{1}} ⋯ ⟶^{a′_{m}} x′_{m}. The concatenation of a finite path p with an infinite path ρ is defined similarly.

The three forms of the satisfaction relation ⊧ are defined through simultaneous induction as follows.

Finite path expressions

T S, p ⊧ φ  iff p = x_{0} and T S, x_{0} ⊧ φ.
T S, p ⊧ a  iff p = x_{0} ⟶^{a_{1}} x_{1} and a_{1} = a.
T S, p ⊧ e_{1} · e_{2} iff p = p_{1} · p_{2}, T S, p_{1} ⊧ e_{1} and T S, p_{2} ⊧ e_{2}
T S, p ⊧ e_{1} + e_{2} iff T S, p ⊧ e_{1} or T S, p ⊧ e_{2}

T S, p ⊧ e^{∗} iff p = x_{0} or

p = p_{1} · p_{2} ⋯ p_{m} and for i ∈ {1, 2, …, m}, T S, p_{i} ⊧ e

Path expressions T S, ρ ⊧ e_{1} · e_{2}^{ω} iff there is a prefix p_{0} · p_{1} · p_{2} ⋯ of ρ such that

T S, p_{0} ⊧ e_{1} and for i ∈ {1, 2, …}, T S, p_{i} ⊧ e_{2}

T S, ρ ⊧ α_{1} + α_{2} iff T S, ρ ⊧ α_{1} or T S, ρ ⊧ α_{2}

We can associate with each path expression α a set Π_{α} of infinite paths in T S in the obvious way—Π_{α} = {ρ ∈ paths(T S) | T S, ρ ⊧ α}. We let Π_{¬α} denote the set paths(T S) \ Π_{α}.

State formulas

T S, x ⊧ tt  always.
T S, x ⊧ P ∈ Prop iff P ∈ v(x).
T S, x ⊧ ¬φ  iff T S, x |̸= φ.
T S, x ⊧ φ_{1} ∨ φ_{2} iff T S, x ⊧ φ_{1} or T S, x ⊧ φ_{2}.
T S, x ⊧ E_{S}α  iff S has a winning strategy for the game (Π_{α}, x).
T S, x ⊧ A_{S}α  iff S does not have a winning strategy for the game (Π_{¬α}, x).

It is useful to think of E_{S}α as asserting that S has a strategy to enforce α along every path. Conversely, A_{S}α asserts that S does not have a strategy to avoid α along every path—in other words, no matter what strategy S chooses, there is at least one path consistent with the strategy along which α holds.

In the absence of fairness constraints, the games we have described are determined and E_{S}φ is logically equivalent to A_{Σ\S}φ. In other words, we can derive one quantifier from the other. However, once we introduce fairness constraints, the games are no longer determined, in general, and the two quantifiers need to be introduced independently, as we have done here. However, even with fairness constraints, E_{S}φ implies A_{Σ\S}φ.

3.3 Examples

Let e be a finite path expression. We shall use the following abbreviations for convenience.

– The formula E_{S}e (respectively, A_{S}e) abbreviates the formula E_{S}ett^{ω} (respectively, A_{S}ett^{ω}). Every path in Π_{ett^{ω}} has a finite prefix that satisfies the property e.

– The formula E_{S}e^{ω} (respectively, A_{S}e^{ω}) abbreviates the formula E_{S}tte^{ω} (respectively, A_{S}tte^{ω}).

The operators E and A of logics like CTL^{∗} are just abbreviations for E_{Σ} and E_{∅}, respectively. Using these branching-time operators, we can specify some traditional temporal properties as follows. Let the set of actions be {a_{1}, a_{2}, …, a_{m}}. In the examples, Σ abbreviates the finite path expression (a_{1} + a_{2} + ⋯ + a_{m}).

– The LTL formula φUψ (φ holds until ψ holds) is captured by the path expression (φΣ)^{∗} · ψ. Thus, the state formula A(φΣ)^{∗} · ψ asserts that φUψ is true of every computation path.

– In LTL, the formula ◇φ (φ holds eventually) can be written as ttUφ. The corresponding path expression is (ttΣ)^{∗} · φ, which we shall denote Eventually(φ).

– Let Invariant(φ) denote the path expression (φΣ)^{ω}. The expression Invariant(φ) asserts that the state formula φ is invariant along the path, corresponding to the LTL formula □φ. Thus, the state formula A Invariant(φ) says that along all paths φ always holds.

– The formula A((E(Σ^{∗} · φ) · Σ)^{ω}) asserts that along every path φ is always attainable (Branching Liveness). This property has been used in the verification of the Futurebus protocol [CGH^{+}95].

We can also assert properties that are not expressible in CTL^{∗} (or ATL^{∗}). For instance, A(Σa)^{ω} asserts that along all paths, every even position is an a.

Now, let us see how to use Orex to describe properties of a typical open system. Figure 1 shows a variant of the train gate controller described in [AHK97]. In this system, the atomic propositions are {in gate, out of gate, waiting, admitted}. In the figure, the labels on the states indicate the valuation. The actions can be partitioned into two sets, train and ctr, corresponding to two components of the system, the train and the controller. The set train is given by {idle, request, relinquish, enter, leave} while ctr is given by {grant, reject, eject}.

Here are some properties that one might like to assert about this system.

– If the train is outside the gate and has not yet been granted permission to enter the gate, the controller can prevent it from entering the gate:

A Invariant((out of gate ∧ ¬admitted) ⇒ EctrInvariant(out of gate))

out of gate in gate  request  grant reject enter relinquish idle idleleave eject  admitted out of gate out of gate waiting

Fig. 1. A train gate controller

– If the train is outside the gate, the controller cannot force it to enter the

gate:

A Invariant(out of gate ⇒ ActrInvariant(¬in gate))

This property can also expressed by the dual assertion that the train can choose to remain out of the gate.

A Invariant(out of gate ⇒ EtrainInvariant(¬in gate))

– If the train is outside the gate, the train and the controller can cooperate so that the train enters the gate:

A Invariant(out of gate ⇒ E Eventually(in gate))

– If the train is in the gate, the controller can ensure that it eventually leaves the gate.

A Invariant(in gate ⇒ EctrEventually(out of gate))

Notice that this property is not satisfied by the system unless fairness is introduced—after entering the gate, the train may execute the action idle forever. However, since eject is continuously enabled at this state, even weak fairness suffices to ensure that the controller can eventually force the train to leave the gate.

– Actually, it is unrealistic to assume that the controller can eject the train once it is in the gate. If we eliminate the transition labelled eject, we can make the following assertion which guarantees that as long as the train does not idle continuously, it eventually leaves the gate.

A Invariant(in gate ⇒ (¬(idle)^{ω} ⇒ Eventually(out of gate))

To state this property, we need to integrate assertions about actions and states in the formula. This formula cannot be conveniently expressed in ATL^{∗}, where formulas can only refer to properties of states.

4 The Model-Checking Algorithm

We now describe an automata-theoretic model checking algorithm for Orex formulas. As we remarked earlier, path expressions can be regarded as ω-regular expressions over the infinite alphabet consisting of the finite set of actions Σ together with the set of all state formulas. However, if we fix a finite set of state formulas Ψ, we can regard each path expression which does not refer to state formulas outside Ψ as an ω-regular expression over the finite alphabet Σ ∪Ψ. We can associate with each such path expression α a language L(α) of infinite words over Σ ∪ Ψ using the standard interpretation of ω-regular expressions [Tho90].

Unfortunately, this naïve translation does not accurately reflect the meaning of path expressions: \overline{L(α)}, the complement of L(α), may contain sequences that are models of α. For instance, if L(α) contains aφ_{1}φ_{2}b^{ω} but does not contain aφ_{2}φ_{1}b^{ω}, the second path will be present in \overline{L(α)} though it models α. We require more structure in the infinite sequences we associate with path expressions to faithfully translate logical connectives into automata-theoretic operations.

We begin by defining an alternative model for finite path expressions and path expressions in terms of sequences over an extended alphabet. Let Ψ be a finite set of state formulas. A Ψ-decorated sequence over Σ is a sequence in which subsets of Ψ alternate with elements of Σ. More precisely, a Ψ-decorated sequence over Σ is an element of (2^{Ψ} · Σ)^{∗}(2^{Ψ}) ∪ (2^{Ψ} · Σ)^{ω}. We use s to denote a finite Ψ-decorated sequence and σ to denote an arbitrary (finite or infinite) Ψ-decorated sequence. A finite Ψ-decorated sequence s can be concatenated with a Ψ-decorated sequence σ if the last element of s is identical to the first element of σ. The concatenation is obtained by deleting the last element of s.

We denote the set of finite path expressions and path expressions that do not refer to any state formulas outside Ψ as FPE_{Ψ} and PE_{Ψ}, respectively. We can interpret expressions from FPE_{Ψ} and PE_{Ψ} over Ψ-decorated sequences. The satisfaction relation is defined as follows:

s ⊧ φ  iff s = X_{0} and φ ∈ X_{0}
s ⊧ a  iff s = X_{0}aX_{1}
s ⊧ e_{1} · e_{2} iff s = s_{1} · s_{2}, s_{1} ⊧ e_{1} and s_{2} ⊧ e_{2}
s ⊧ e_{1} + e_{2} iff s ⊧ e_{1} or s ⊧ e_{2}
s ⊧ e^{∗}  iff s = X_{0} or {s = s_{1} · s_{2} ⋯ s_{n} \atop and for i ∈ \{1, 2, …, n\}, s_{i} ⊧ e}

σ ⊧ e_{1} · e_{2}^{ω} iff there is a prefix s_{0} · s_{1} · s_{2} ⋯ of σ such that

s_{0} ⊧ e_{1} and for i ∈ {1, 2, …}, s_{i} ⊧ e_{2}
σ ⊧ α_{1} + α_{2} iff σ ⊧ α_{1} or σ ⊧ α_{2}

Let T S = ⟨X, Σ, ⟶⟩ be a Σ-labelled transition system and v : X → Prop be a valuation over T S. For each path ρ = x_{0} ⟶^{a_{1}} x_{1} … in T S, the corresponding Ψ-decorated sequence σ_{ρ} is X_{0}a_{1}X_{1} … where X_{i} = {φ | φ ∈ Ψ and T S, x_{i} ⊧ φ}. Then, for any path expression α ∈ PE_{Ψ}, T S, ρ ⊧ α if and only if σ_{ρ} ⊧ α.

There is a natural connection between the language L(α) defined by α ∈ PE_{Ψ} and the semantics of α in terms of Ψ-decorated sequences. To formalize this, we need to define when a Ψ-decorated sequence embeds a sequence over Σ ∪ Ψ.

Embedding Let w = w_{0}w_{1} … be an infinite word over Σ ∪ Ψ and σ = σ_{0}σ_{1} … be a Ψ-decorated sequence. Observe that σ_{i} ⊆ Ψ if i is even and σ_{i} ∈ Σ if i is odd. We say that σ embeds w if there is a monotone function f : ℕ_{0} → ℕ_{0} mapping positions of w into positions of σ such that:

(i) If i is in the range of f, j < i and j is odd, then j is in the range of f. (ii) If w_{i} ∈ Σ then w_{i} = σ_{f(i)}. (iii) If w_{i} ∈ Ψ then w_{i} ∈ σ_{f(i)}.

We can then establish the following connection between L(α) and the set of Ψ-decorated sequences that model α.

Lemma 4.1. A Ψ-decorated sequence σ models a path expression α ∈ PE_{Ψ} if and only if σ embeds at least one of the sequences in the language L(α) over the alphabet Σ ∪ Ψ.

Let |α| denote the number of symbols in a path expression α. From the theory of ω-regular languages [Tho90], we know that for each path expression α ∈ PE_{Ψ}, we can construct a nondeterministic Büchi automaton A_{α} over Σ ∪Ψ whose size is polynomial in |α| and whose language is precisely L(α).

Using our notion of embedding, we can associate with each Büchi automaton A over Σ ∪ Ψ an extended language L^{+}(A) of Ψ-decorated sequences as follows:

L^{+}(A) = {σ | ∃w ∈ L(A) : σ embeds w}

Lemma 4.2. For any Büchi automaton A over Σ ∪Ψ, we can construct a Büchi automaton A^{+} over Σ ∪ 2^{Ψ} such that A^{+} reads elements from Σ and 2^{Ψ} alternately, L^{+}(A) = L(A^{+}) and the number of states of A^{+} is polynomial in the number of states of A.

Proof Sketch: Let A = (Q, δ, q_{0}, F) be a given nondeterministic Büchi automaton over Σ ∪ Ψ. For states p, q ∈ Q and U ⊆ Ψ, we write p ⇒^{U} q if there is a sequence of transitions from p ending in q whose labels are drawn from the set U. We write p ⇒^{U}_{F} q to indicate that there is a sequence of transitions from p to q that passes through a state from F, all of whose labels are drawn from the set U. We write p ⇒^{U}_{A} if there is an accepting run starting at p, all of whose labels are drawn from the set U.

The automaton A^{+} = (Q^{+}, Σ ∪ 2^{Ψ} , δ^{+}, F^{+}, q_{0}) where:

\begin{matrix}Q^{+} = & (Q × \{0, 1, 2\}) ∪ \{q_{f}, p_{f}\} \\ F^{+} = & (Q × \{2\}) ∪ \{p_{f}\} \\ δ^{+} = & \begin{matrix}\{((p, 0), U, (q, 1)) | p ⇒^{U} q\} ∪ \{((p, 0), U, (q, 2)) | p ⇒^{U}_{F} q\}∪ \\ \{((p, 0), U, q_{f}) | p ⇒^{U}_{A}\}∪ \\ \{((p, 1), a, (q, 0)), ((p, 2), a, (q, 0)) | (p, a, q) ∈ δ\}∪ \\ \{((p, 0), U, (p, 1)) | p ∈ Q, U ⊆ Ψ\} ∪ \{(q_{f}, a, p_{f}) | a ∈ Σ\}∪ \\ \{(p_{f}, U, q_{f}) | U ⊆ Ψ\} \end{matrix} \end{matrix}

⊓ ⊔

The construction allows us to convert a path expression α ∈ PE_{Ψ} into an automaton A_{α}^{+} over Σ ∪ 2^{Ψ} whose state space is polynomial in |α|. Notice that the alphabet, and hence the number of transitions, of A_{α}^{+} is exponential in |α|.

The lemma assures us that if we complement A_{α}^{+}, we obtain an automaton that accepts precisely those Ψ-decorated sequences that do not model α. As we remarked earlier, this is not true of the original automaton A_{α}: \overline{L(α)} may contain sequences that can be embedded into Ψ-decorated sequences that model α. In a sense, L^{+}(A) can be thought of as the semantic closure of L(A).

Lemma 4.3 ([Saf88,EJ89]). A Büchi automaton A can be effectively determinized (complemented) to get a deterministic Rabin automaton whose size is exponential in the number of states of A and linear in the number of transitions of A and whose set of accepting pairs is linear in the number of states of A. This automaton can be constructed in time exponential in the number of states of A and polynomial in the number of transitions of A.

Lemma 4.4 follows from the previous two lemmas.

Lemma 4.4. From a path expression α ∈ PE_{Ψ}, we can construct a deterministic Rabin automaton A_{α}^{R} (\overline{A}_{α}^{R}) that accepts exactly those Ψ-decorated paths that do (do not) model α. The number of states of A_{α}^{R} (\overline{A}_{α}^{R}) is exponential in |α| and the number of accepting pairs of A_{α}^{R} (\overline{A}_{α}^{R}) is polynomial in |α|.

Theorem 4.5. Given a transition system T S, a state x in T S and an Orex formula φ, the model checking problem T S, x ⊧ ? φ can be solved in time O((mk)^{k}), where m is given by 2^{O(|φ|)} · |T S| and k is a polynomial in |φ|.

Proof Sketch: We use the bottom-up labelling algorithm of CTL^{∗} and ATL^{∗}. The only interesting case is when the formula φ to be checked is of the form E_{S}α (or A_{S}α). Each S-strategy f at a state x can be represented as a tree by unfolding T S starting at x, retaining all Σ \ S edges in the unfolding, but discarding all S-transitions that are not chosen by the strategy. Conversely, if we unfold T S at x and prune S-transitions while ensuring that at least one Stransition is retained at each state y where enabled(y) ∩ ⟶_{S} ≠ ∅, we obtain a representation of some S-strategy at x.

Let Ψ be the set of state formulas that appear in α. We may assume that each state of the transition system T S is labelled with the formulas from Ψ that hold at that state. In the trees that we use to represent strategies, each state is labelled by the same subset of formulas as the corresponding state in T S.

The trees that represent strategies carry labels on both the states and the edges. We can convert these to state-labelled trees by moving the label on each edge to the destination state of the edge.

Given a transition system T S, we can construct a Büchi tree automaton T_{T S} that accepts precisely those trees labeled by Σ ∪ 2^{Ψ} that arise from strategies, as described in [KV96]. The size of T_{T S} is linear in the size of T S.

An S-strategy f is a witness for T S, x ⊧ E_{S}α if and only if every infinite path in the tree corresponding to f models α. Equivalently, every infinite path in this tree, when treated as a sequence over Σ ∪ 2^{Ψ}, is accepted by the Rabin automaton A_{α}^{R} constructed from A_{α}^{+} as described in Lemma 4.4. Since A_{α}^{R} is deterministic, we can convert it into a Rabin tree automaton T_{α} that runs A_{α}^{R} along all paths and accepts exactly those trees in which all infinite paths model α. The automaton T_{α} has the same size as A_{α}^{R}—that is, the number of states is exponential in |α| and the number of accepting pairs is polynomial in |α|.

Finally, we construct the product of T_{T S} and T_{α} to obtain a tree automaton that accepts a tree if and only if it corresponds to a strategy f such that all infinite paths in T S consistent with f satisfy α. We can then use the algorithm of Emerson and Jutla [EJ88] to check whether this product automaton accepts a nonempty set of trees. The Emerson-Jutla algorithm solves the emptiness problem for a tree automaton with i states and j accepting pairs in time O((ij)^{3j}). From this, we can derive that the emptiness of the product tree automaton we have constructed can be checked in time O((mk)^{k}), where m is given by 2^{O(|α|)} · |T S| while k is a polynomial in |α|.

The case A_{S}α is similar to E_{S}α with one modification—use the construction due to Emerson and Jutla [EJ89] instead of Safra’s construction to obtain a deterministic Rabin automaton \overline{A}_{α}^{R} that accepts exactly those sequences over Σ ∪ 2^{Ψ} that do not model α.

In the constructions above, we have not taken into account the case when we are interested only in (weakly or strongly) S-fair computations. Fairness constraints can be handled by adding a simple Rabin condition to the automaton T_{T S} that accepts all trees corresponding to S-strategies. This extra structure does not materially affect the overall complexity of the procedure.

⊓ ⊔

5 Related Work

In [AHK97], the logic ATL^{∗} is interpreted over two kinds of transition systems: synchronous structures and asynchronous structures. In each case, the notion of agent plays a prominent role in the definition. In a synchronous structure, each state is associated with a unique agent. An important subclass of synchronous structures is the one with two agents, one representing the system and the other the environment. Such systems have been studied by Ramadge and Wonham [RW89] in the context of designing controllers for discrete-event systems.

In an asynchronous structure, each transition is associated with an agent. A synchronous structure can be thought of as a special kind of asynchronous structure where all transitions out of a state are associated with a single agent. Our Σ-labelled transition systems correspond to asynchronous structures, where the set of agents corresponds to the alphabet Σ.

The notion of strategy described in [AHK97] is slightly different from the one we use here. In their framework, each agent has a strategy and an S-strategy at a state allows any move permitted by all the individual strategies of the agents in S. Our definition of global strategy is more generous. We believe that decompositions of strategies where each agent has a view of the global state do not arise naturally and have therefore chosen not to incorporate this into our logic. Nevertheless, we can easily simulate the framework of [AHK97] in our setup without changing in the complexity of the construction.

In the Introduction, we mentioned that Orex subsumes ATL^{∗} in expressive power since ω-regular expressions are more powerful than LTL. We also note that in the context of open systems, it is natural to refer to properties of both states and actions in a transition system. If we use LTL to express properties of paths, as is the case with ATL^{∗}, we have to encode actions in the states of the system since LTL can only talk about properties of states. On the other hand Orex provides a seamless way of interleaving assertions about actions and states along a path. This makes for more natural models of open systems—for instance, compare our example of the train gate controller with explicit action labels with the version in [AHK97] where the action labels are encoded as propositions.

There has been earlier work on game logics that mention actions. In [Par83], Parikh defines a propositional logic of games that extends propositional dynamic logics [Har84]. The logic studied in [Par83] is shown to be decidable. A complete axiomatization is provided, but the model-checking problem is not studied.

6 Conclusions

As Theorem 4.5 indicates, the model-checking complexity of Orex is at least one exponential better than that of ATL^{∗}, though Orex subsumes ATL^{∗} in expressive power. If we restrict the quantifiers of Orex to the normal branchingtime interpretation A and E, we obtain a system called Brex that corresponds to the branching-time logic ECTL^{∗}. The model-checking algorithm for Brex is exponential, which is comparable to the complexity of model-checking CTL^{∗}.

Why does going from CTL^{∗} to ATL^{∗} add an exponential to the complexity of model-checking, unlike the transition from Brex to Orex? The construction in [VW86] can be used to build nondeterministic Büchi automata for LTL formulas α and ¬α with exponential blow-up. Thus the complexity of model-checking CTL^{∗} stays exponential. When we translate Brex path formulas into automata we only incur a polynomial blowup in size, but we may have to complement the automaton for α to get an automaton for ¬α. Complementation is, in general, exponential and, consequently, model-checking for Brex is also exponential.

When going from CTL^{∗} to ATL^{∗}, we need to determinize the Büchi automaton constructed from the LTL formula α so that we can interpret the automaton over trees. This blows up the automaton by another exponential, resulting in a model-checking algorithm that is doubly exponential in the size of the input formula. In Orex the automaton we construct for path formulas is already determinized, so we avoid the second exponential blow-up.

Finally, we note that if we restrict our syntax to only permit the existential path quantifier Eα, we can model-check Brex in polynomial time — essentially, it suffices to construct a nondeterministic automaton for α. On the other hand, the model-checking problem for Orex remains exponential even with this restriction because we have to determinize the automaton for α. Since ω-regular languages are closed under complementation, we can reduce any formula in Brex or Orex to one with just existential path quantifiers. However, in the process, we have to complement ω-regular expressions. Since this is, in general, an exponential operation, the cost of this translation is exponential (perhaps nonelementary, since nested negations introduce nested exponentials). Thus, the full language that we have presented here permits more succinct specifications and more efficient verification than the reduced language with just existential quantifiers.

References

[AHK97] R. Alur, T.A. Henzinger, and O. Kupferman. Alternating-time temporal logic. In Proceedings of the 38th IEEE Symposium on the Foundations of Computer Science. IEEE Press, 1997.

[CE81] E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In D. Kozen, editor, Proceedings of the Workshop on Logic of Programs, Yorktown Heights, volume 131 of Lecture Notes in Computer Science, pages 52–71. Springer-Verlag, 1981.

[CGH^{+}95] E. M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D. E. Long, K. L. McMillan, and L. A. Ness. Verification of the Future+ cache coherence protocol. Formal Methods in System Design, 6:217–232, 1995.

[EH86] E. A. Emerson and J. Y. Halpern. ‘Sometime’ and ‘not never’ revisited: On branching versus linear time temporal logic. Journal of the ACM, 33(1):151– 178, 1986.

[EJ88] E.A.Emerson and C. Jutla. The complexity of tree automata and logics of programs. In Proceedings of the IEEE FOCS, 1988.

[EJ89] E.A.Emerson and C. Jutla. On simultaneously determinising and complementing ω-automata. In Proceedings of the IEEE FOCS, 1989.

[Har84] David Harel. Dynamic logic. In Handbook of Philosophical Logic, Volume II. Reidel, 1984.

[Hol97] G. J. Holzmann. The model checker SPIN. IEEE Trans. on Software Engineering, 23(5):279–295, 1997.

[KV96] Orna Kupferman and Moshe Vardi. Module checking. In Proceedings of CAV’96, LNCS 1102. Springer-Verlag, 1996.

[McM93] K. L. McMillan. Symbolic Model Checking. Kluwer Academic, 1993.

[Par83] R. Parikh. Propositional game logic. In Proceedings of 24th IEEE FOCS, pages 195–200, 1983.

[Pnu76] A. Pnueli. The temporal logic of programs. In Proceedings of the IEEE Symposium on the Foundations of Computing Science. IEEE Press, 1976.

[RW89] P.J.G. Ramadge and W.M. Wonham. The control of discrete-event systems. IEEE Trans. on Control Theory, 77:81–98, 1989.

[Saf88] S. Safra. On complexity of ω-automata. In In the Proceedings of the 29th FOCS, 1988.

[Tho90] W. Thomas. Automata on infinite objects. In Handbook of Theoretical Computer Science, Volume B. Elsevier Science Publishers, 1990.

[VW86] M. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Symposium on Logic in Computer Science (LICS ’86), pages 332–344, Cambridge, Massachusetts, June 1986. Computer Society Press.