Nicolas Markey

Temporal logics

Keywords:

Chapter 1 Introduction Logic (from classical Greek lìgoc, meaning word or thought) aims at studying statements and arguments of reasoning. According to [START_REF] Shapiro | Classical logic[END_REF],

Typically, a logic consists of a formal or informal language together with a deductive system and/or a model-theoretic semantics. The language is, or corresponds to, a part of a natural language like English or Greek. The deductive system is to capture, codify, or simply record which inferences are correct for the given language, and the semantics is to capture, codify, or record the meanings, or truth-conditions, or possible truth conditions, for at least part of the language.

Historically, the study of logic independently started in India and China, during the 6th century B.C., but has been much more developped by Greek philosophers after the 4th century B.C. However, logic was really formalized in the second half of the 19th century [START_REF] Frege | Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens[END_REF], and has been much developped since then.

It has been remarked since Aristotle that classical logic cannot express subtler points such as possibility or necessity: that something is possible does not mean that it is true or false, but rather that it might be true or false. The problem of the future contingents, aiming at expressing that There will be a sea battle tomorrow.

is an example of a sentence that cannot be captured by classical logic. Again, while several philosophers studied the question since then, modal logics have only been formally defined in 1918 [START_REF] Irving | A Survey of Symbolic Logic[END_REF]. Several flavours of modal logics have been developped since then: alethic logic is the logic to handle possibility and necessity, deontic logic aims at reasoning about permission and obligation, while epistemic logic deals with knowledge... Basically, all those logics use the same two modalities ♦ (for possibly) and (for necessarily), but with different sets of axioms.

Chapter 2

From propositional logic to temporal logic

Propositional logic

If temporal logic is seen as a language for describing a movie, then propositional logic can be seen as a language for describing a picture [START_REF] Goranko | Temporal logics of computations[END_REF]. The basic blocks are atomic propositions, that can be combined with Boolean operators: Definition 1 The syntax of propositional logic over a set AP of atomic propositions is given by the following grammar:

PL φ ::= p | ¬φ | φ ∨ φ | φ ∧ φ
where p ranges over AP.

The semantics of the Boolean operators ¬ (negation), ∨ (disjunction) and ∧ (conjunction) are given as truth table displayed at table 2.1. p ¬p false true true false p q p ∨ q false false false false true true true false true true true true p q p ∨ q false false false false true false true false false true true true Example. If AP = {"the sky is blue", "the grass is green"}, then the following formula is well-formed: ¬("the sky is blue" ∨ ¬"the grass is green).

It is true exactly when the sky is not blue and the grass is green.

Definition 2 Two Boolean formulas φ and ψ are equivalent if, under each possible valuation v : AP → {true, false}, the truth values of φ and ψ are equal. This is denoted by φ ≡ ψ.

From that semantics, it is easy to derive the following results:

Theorem 3 (De Morgan's laws)

¬(φ ∧ ψ) ≡ ¬φ ∨ ¬ψ ¬(φ ∨ ψ) ≡ ¬φ ∧ ¬ψ
Several other boolean operators can be defined from the main three ones. For instance, it is usual to define the implication, denoted with ⇒, as p ⇒ q def ≡ ¬p ∨ q.

Similarly, exclusive or, written ⊕, is defined as

p ⊕ q def ≡ (p ∨ q) ∧ ¬(p ∧ q).
We conclude this section with a famous result, due to Stephen Cook [Coo71]:

Theorem 4 Deciding the satifiability of a formula of PL is NP-complete.

On the other hand, evaluating the truth value of a formula given a valuation of the atomic propositions is NC 1 -complete (i.e., ALOGTIME-complete) [START_REF] Samuel | An optimal parallel algorithm for formula evaluation[END_REF]. We refer to [START_REF] Papadimitriou | Computational Complexity[END_REF] for more details about those complexity classes.

Exercice 2.1.

Prove Theorem 3.

Exercice 2.2.

From De Morgan's laws, we could define the syntax of PL with only negation and conjunction (or only negation and disjunction), since the third operator can be defined from the first two.

Prove that negation cannot be defined in terms of conjunction and disjunction. Is it possible to define another binary boolean operator such that negation, conjunction and disjunction can be defined using only that operator? Exercice 2.3.

Prove Theorem 4.

First-and second-order logics

First-order logic is an extension of propositional logic with quantification over a set of items X. In that setting, atomic propositions are replaced by monadic predicates, i.e., functions p : X → {true, false}.

Definition 5 The syntax of first-order monadic logic is defined as:

FOML φ ::= p(x) | ¬φ | φ ∨ ψ | φ ∧ ψ | ∃x ∈ X.φ | ∀x ∈ X.φ
where p ranges over the set MP of monadic predicates, x and y range over the fixed set X, with the extra requirement that any variable that appears as the argument of a predicate must be bound by an existential or universal quantifier.

The semantics is the natural one: a formula ∃x ∈ X.φ(x) holds if the function φ : X → {true, false} is not always false, while ∀x ∈ X.φ(x) is true if φ always equals true. In particular:

Theorem 6 ¬(∃x ∈ X.φ(x)) ≡ ∀x ∈ X.¬φ(x).

Example. If X = {sky, grass} and MP = {is blue, is green}, then the following is a well-formed formula: ∀x ∈ X.(is green(x) ∨ is blue(x)).

In the (interesting) case when X can be ordered, first-order logic can be extended to also be able to use that order: Definition 7 Let (X, ≤) be an ordered set. The syntax of first-order monadic logic of order is defined as:

FOMLO φ ::= p(x) | x ≤ y | ¬φ | φ ∨ ψ | φ ∧ ψ | ∃x ∈ X.φ | ∀x ∈ X.φ
The semantics is immediately derived from that of FOML. Of course, since the order is reflexive, it is possible to test for the equality of two items of X.

Example. If X is the set of nonnegative integers equipped with its classical order, using predicates is odd and is even, the following formulas hold:

• Z + has a minimal element: ∃x ∈ Z + . ∀y ∈ Z + . x ≤ y.

• among two successive integers, exactly one is odd:

∀x ∈ Z + . ∀y ∈ Z + . (x ≤ y) ⇒ (∀z ∈ Z + . (z ≤ x ∨ y ≤ z)) ⇒ (is odd(x) ⊕ is odd(y)) .
In this case, we have a theorem similar to Theorem 4, but with a much higher complexity:

Theorem 8 The satisfiability of a formula of FOMLO is decidable (and has non-elementary complexity).

10CHAPTER 2. FROM PROPOSITIONAL LOGIC TO TEMPORAL LOGIC Note that such a result depends on the underlying order. The result above holds for classical linear orders such as Z + , ≤ [START_REF] Stockmeyer | The Complexity of Decision Problems in Automata Theory and Logic[END_REF] or R + , ≤ [START_REF] Burgess | The decision problem for lineasr temporal logic[END_REF].

Exercice 2.4.

Over the set of nonnegative integers, using the monadic predicate is prime, write a formula in FOMLO expressing (the conjecture) that there exists infinitely many twin primes [START_REF]Twin prime conjecture -Wikipedia, the free encyclopedia[END_REF].

Second-order logic is an extension of first-order logic in which one can also quantify over subsets of the set X: Definition 9 Let (X, ≤) be an ordered set. The syntax of monadic second-order logic of order is defined as:

SOMLO φ ::= p(x) | x ≤ y | x ∈ Y | ¬φ | φ ∨ ψ | φ ∧ ψ | ∃x ∈ X.φ | ∀x ∈ X.φ | ∃Z ⊆ X.φ | ∀Z ⊆ X.φ.
where p ranges over the set MP of monadic predicates, x and y range over the fixed set X, Y ranges over the set of all subsets of X, with the extra requirement that any variable that appears as the argument of a predicate must be bound by an existential or universal quantifier.

Notice that we directly defined SOMLO, but obviously SOML can also be defined, as in the case of first-order logic. Again, the semantics is rather obvious, and we omit it. Also, clearly, Theorem 6 also holds for second-order quantification. Last, we have the following:

Theorem 10 The satisfiability problem for SOMLO is decidable (and has nonelementary complexity).

Let us insist again on the fact that this general result only holds in some (interesting) special cases: discrete and continuous linear orders [START_REF] Büchi | Weak second-order arithmetic and finite automata[END_REF]Rab], and discrete tree orders [Rab].

Remark. Note that it is of course possible to define higher-order logics, with quantification over sets of sets of X, and so on. In that hierarchy, propositional calculus is sometimes refered to as zeroth-order logic.

Example. Assume that X is a totally ordered set. FOMLO can express that X is has no minimal element: ∃x ∈ X. ∀y ∈ X. x ≤ y.

But FOMLO cannot express that X is well-ordered, i.e., that any non-empty subset has a minimum element: this requires second-order quantification:

∀Y ⊆ X.(∃x ∈ Y. ∀y ∈ Y. x ≤ y)

Modal logics

Roughly speaking, modal logics are extensions of propositional logic with new operators that express possibility or necessity. Basically: Definition 11 The syntax of modal logic is:

ML φ ::= p | ¬φ | φ ∨ φ | φ ∧ φ | ♦ φ | φ
where p ranges over the set AP of atomic propositions.

The semantics of modal logics is generally defined over Kripke structures:

Definition 12 Let AP be a (finite) set of atomic propositions. A Kripke structure is a 3-tuple W, R, l s.t.:

• W is a non-empty set whose items are called worlds,

• R is a binary relation over W (often refered to as the accessibility relation).

It is required that for any w ∈ W , there exists w ∈ W s.t. (w, w ) ∈ R (i.e., each world must have at least one successor).

• l : W → 2 AP maps each world to the set of atomic propositions that hold in that world.

A Kripke structure is in fact nothing more than a lebeled transition system, and the name is only kept in honour of Saul Kripke, who used them in order to define the semantics of modal logics.

Definition 13 Let K be a Kripke structure, w ∈ W be a world, and φ ∈ ML. That formula φ holds in the world w (denoted w |= φ) is defined through the following recursive rules:

• w |= p if, and only if, p ∈ l(p), for any atomic proposition p,

• w |= ¬ψ if, and only if, w |= ψ,

• w |= ψ 1 ∨ ψ 2 if, and only if, w |= ψ 1 or w |= ψ 2 , • w |= ψ 1 ∧ ψ 2 if, and only if, w |= ψ 1 and w |= ψ 2 , • w |= ♦ ψ if, and only if, ∃w ∈ W.((w, w ) ∈ R ∧ w |= ψ), • w |= ψ if, and only if, ∀w ∈ W.((w, w ) ∈ R ⇒ w |= ψ).
This captures the intuitive meaning that something possible is true in one of the accessible worlds, while something necessary holds in any. Depending on the nature (alethic, epistemic, ...) of the modal logic under study, Kripke structures might be required to be reflexive, transitive, ...

The following result directly follows from this definition:

Theorem 14 ¬♦ φ ≡ ¬φ.
12CHAPTER 2. FROM PROPOSITIONAL LOGIC TO TEMPORAL LOGIC

Temporal logics

Temporal logic is, originally, a derivative of modal logic that focuses on the succession of events along time. With no constraint on the Kripke structure, modalities ♦ and have their standard meaning, concerning the set of next states. If we require that the Kripke structure be transitive (modeling the fact that "being in the future" is transitive), then

• ♦ φ means that φ will be true some time in the future, along some evolution.

• φ means that φ will always hold, at any time in the future, and along any evolution.

Still, this definition does not allow to express properties such as "φ is unavoidable", i.e., that φ will eventually occur along any evolution. In fact, temporal logic now comprises two main frameworks: the linear-time framework, and the branching-time framework. The former aims at expressing properties along each single evolution in the Kripke structure, while the latter adds quantification over the possible evolutions.

In the linear-time setting, modalities ♦ and are often written F and G, resp., and are read "eventually in the future" and "always in the future". It is of course possible to define extra modalities. In a broad sense, a modality is a n-ary predicate whose definition can be expressed in FOMLO. For example, extra modalities have been defined for dealing with what happened in the past: it is now standard to write them as F -1 and G -1 , and to read them "sometime in the past" and "always in the past", resp. Two binary modalities are also classically used: U, read "until", and S, read "since". Those modalities have been introduced by Hans Kamp after he proved that they could not be expressed with only unary modalities [START_REF] Kamp | Tense Logic and the Theory of Linear Order[END_REF]. The formal semantical definitions, as well as many related results, will be given and explained in Chapter 3, which is entirely devoted to the linear-time framework.

The branching-time framework can be seen as an extension of linear-time temporal logics with path quantifiers, namely E ("there exists an evolution such that...") and A ("along any evolution, ..."). The intuition (which will be made formal in Chapter 4, which entirely focuses on branching-time temporal logics) indicates that EF φ corresponds to ♦ φ, that AG φ corresponds to φ, while AF φ expresses that φ will eventually occur along any evolution.

Temporal logics in computer science

In 1977, Amir Pnueli introduced the use of (linear-time) temporal logics in computer science [START_REF] Pnueli | The temporal logic of programs[END_REF], in order to (automatically) verify that a reactive system (modeled as a Kripke structure, i.e., a labeled transition system) satisfies some properties (expressed, for instance, as temporal logic formulas). Branchingtime logic have also quickly been introduced in this framework [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching-time temporal logic[END_REF][START_REF] Queille | Specification and verification of concurrent systems in CESAR[END_REF].

This technique, now called model-checking, has been much developped since then: efficient algorithms and powerful data-types have been introduced and This course is mainly devoted to the study of temporal logics for modelchecking. The advantage of temporal logics in that framework is that they are expressive enough (and not too difficult to manipulate) for most applications, and have reasonably efficient verification algorithms. Satisfiability of a temporal logic formula is a connected problem, and it will also be studied in this course. Formally, those two problems are defined as follows:

Definition 15 satisfiability: Input a formula φ;

Output true if there exists a structure on which φ evaluates to true.

model checking:

Input a formula φ and a structure s;

Output true if φ holds in the structure s.

Chapter 3

Linear-time temporal logics

In the sequel, AP represents a non-empty, finite set of atomic propositions.

Linear structures

Linear-time temporal logics are those temporal logics that express properties over each single evolution of the system. We first define formally how such an evolution is represented.

Definition 16 A (labeled) linear structure is a tuple S = T, ≤, where:

• T, ≤ is a totally-ordered infinite set with a minimal element;

• : T → 2 AP labels each point of T with a subset of AP.

In the sequel, we will always assume that T is (isomorphic to) either the set of nonnegative integers, or the set of nonnegative reals. The set T is often refered to as the time-line: when T = Z + , we say that the time-line is discrete, while T = R + corresponds to a continuous time-line.

Example. Let KS = W, R, l be a Kripke structure, and w ∈ W . Informally, an evolution of K from w is the infinite sequence of worlds (w i ) i∈Z + that are successively traversed. In our formalism, this is represented as a linear-structure

Z + , ≤, s.t. (i) = l(w i ).
Remark. It is often handy to represent and manipulate discrete linear structures as words over the alphabet 2 AP . A linear structure Z + , ≤, would then be represented as the word σ = σ 0 σ 1 . . ., with σ i = (i). In the sequel, we might go from one representation to the other without further notice, as both are very similar.

Linear-time temporal logic formulas will generally be evaluated at one precise point along such a linear structure: Definition 17 A pointed linear structure is a couple S, s where S = T, ≤, is a linear structure, and s ∈ T . We write M lin(T ) for the set of pointed linear structures built on the time-line T .

A special subclass of pointed linear structures is that of initially pointed linear structures, i.e., couples S, 0 where S = T, ≤, and 0 is the minimal element of T (refered to as the origin of the time-line). We write M 0 lin(T ) for the set of initially pointed linear structures built on T .

Linear-time temporal logics

We now define the formal semantics of the modalities that we already mentionned in the introduction.

Definition 18 Let S, s ∈ M lin(T ) be a pointed linear structure. We define the following one-place modalities, together with their (inductive) semantics:

• F (eventually):

S, s |= F φ def ⇔ ∃t. (s ≤ t ∧ S, t |= φ).
• G (always in the future):

S, s |= G φ def ⇔ ∀t. (s ≤ t ⇒ S, t |= φ). • X (next): S, s |= X φ def ⇔ ∃t. (s < t ∧ ∀u. (u ≤ s ∨ t ≤ u) ∧ S, t |= φ).
• F -1 (sometime in the past):

S, s |= F -1 φ def ⇔ ∃t. (t ≤ s ∧ S, t |= φ).
• G -1 (always in the past):

S, s |= G -1 φ def ⇔ ∀t. (t ≤ s ⇒ S, t |= φ). • X -1 (previous): S, s |= X -1 φ def ⇔ ∃t. (s < t ∧ ∀u. (s ≤ u ∨ u ≤ t) ∧ S, t |= φ).
We also define two two-place modalities:

• U (until):

S, t |= φ U ψ def ⇔ ∃t. (s ≤ t ∧ ( S, t |= ψ) ∧ ∀u. ((s ≤ u ∧ u < t) ⇒ S, u |= φ)).
• S (since):

S, t |= φ S ψ def ⇔ ∃t. (t ≤ s ∧ ( S, t |= ψ) ∧ ∀u. ((u ≤ s ∧ t < u) ⇒ S, u |= φ)).
Remark. Several remarks are in order here:

• modalities X and X -1 are only interesting over discrete time-lines;

• one-place modalities, except X and X -1 , can be expressed using only twoplace ones;

• it is possible to define strict versions of the above modalities, that would not take the current position into account. Those modalities are denoted with a tilde. For instance:

-Ũ (strict until):

S, t |= φ Ũ ψ def ⇔ ∃t. (s < t ∧ ( S, t |= ψ) ∧ ∀u. ((s < u ∧ u < t) ⇒ S, u |= φ)).
-S (strict since):

S, t |= φ S ψ def ⇔ ∃t. (t < s ∧ ( S, t |= ψ) ∧ ∀u. ((u < s ∧ t < u) ⇒ S, u |= φ)).
With those definitions, all modalities (both strict and non-strict) can be defined from the above two.

Using those modalities, we can define different linear-time temporal logics:

Definition 19 Given a set of n modalities {M 1 , ..., M n }, the logic L(M 1 , ..., M n ) is the set of formulas built on the following grammar:

L(M 1 , ..., M n ) φ ::= p | ¬φ | φ ∨ φ | φ ∧ φ | M 1 (φ, ..., φ) | • • • | M n (φ, ..., φ).
Several logics built on this schema have a special name:

LTL = L( U , X ) LTL s = L( Ũ ) LTL+Past = L( U , X , S , X -1 ) LTL+Past s = L( Ũ , S )
It might be surprising to define two flavours of LTL and LTL+Past. However, both definitions coexist in the literature: LTL s and LTL+Past s are the standard definitions for the general case, while LTL and LTL+Past are often prefered in the discrete-time case.

Note that, in the remarks above, we did not formally defined what we mean with "can be expressed". The formal definition relies on the notion of equivalence of two formulas: Definition 21 A formula φ can be expressed in a logic L over a set of structures M whenever there exists a formula ψ ∈ L that is equivalent to φ over M.

Exercice 3.5.

Prove all claims of the remarks following Definition 18. Prove that LTL and LTL s are equally expressive.

Exercice 3.6.

This exercice aims at showing that modality U cannot be expressed in the logic L(F , F -1 ). We restrict here to discret-time, but a similar proof could be carried out for other time-lines.

For each positive integer i, consider the word σ i defined with the following rules:

• for any j = i, σ i 3j = a, σ i 3j+1 = b, σ i 3j+2 = c; • σ i 3i = a, σ i 3i+1 = c, σ i 3i+2 = b;
That is, σ i almost equals (abc) ω , except that b and c are swapped in the i-th copy. Prove the following three results:

• the set of positions where formula

F (c ∧ c U b) hold along σ i is [0, 3i + 1].
• if φ is a formula containing at most i modalities among F, G, F -1 and G -1 (and no other modalities), then if φ holds at some position k ≥ 3i, then φ also holds at position k + 3.

• formula F (c ∧ c U b) cannot be expressed in L(F , F -1 ).

Deduce that also modality X cannot be defined in L(F , F -1 ).

Exercice 3.7.

A fairness property is a property stating that something occurs repeatedly, infinitely often. Prove that fairness properties can be expressed in LTL. Symmetrically, what is the meaning of formula F -1 G -1 φ?

Before we study the complexity of satisfiability and model-checking of those logics, we have to define the notion of size of a formula. In fact, two definition coexist:

Definition 22 The size of a formula φ ∈ L(M 1 , ..., M n ) is defined inductively as follows:

|p| = 1 |¬φ 1 | = 1 + |φ 1 | |φ 1 ∨ φ 2 | = 1 + |φ 1 | + |φ 2 | |φ 1 ∧ φ 2 | = 1 + |φ 1 | + |φ 2 | |M (φ 1 , ..., φ n | = 1 + |φ 1 | + • • • + |φ n | .

EXPRESSIVE COMPLETENESS OF LTL+PAST AND LTL

In other words, the size of a formula is the number of symbols (excluding parenthesis) needed for writing a formula. The size of a formula could also be defined as the number of nodes of the tree-representation of the formula (where, for instance, formula M (φ 1 , ..., φ n ) would correspond to one node with n successors corresponding to subformulas φ 1 to φ n ).

If, in such a tree-representation, we merge the states correpsonding to identical subformulas, we get a directed acyclic graph (DAG for short). The number of nodes of this DAG is another way of defining the size of the corresponding formula, called the DAG-size. There is another way of defining this measure:

Definition 23 The DAG-size of a formula φ, written |φ| DAG is the number of subformulas of φ, where the set of subformulas is defined inductively as follows:

SFp = {p} SF¬φ 1 = {¬φ 1 } ∪ SFφ 1 SFφ 1 ∨ φ 2 = {φ 1 ∨ φ 2 } ∪ SFφ 1 ∪ SFφ 2 SFφ 1 ∧ φ 2 = {φ 1 ∧ φ 2 } ∪ SFφ 1 ∪ SFφ 2 SFM i (φ 1 , ..., φ n ) = {M (φ 1 , ..., φ n )} ∪ SFφ 1 ∪ • • • ∪ SFφ n .
Both definitions satisfy the following relation:

Theorem 24 For any φ ∈ L(M 1 , ..., M n ), we have |φ| ≤ |φ| DAG ≤ a |φ|
where a is the maximal arity of the modalities in {M 1 , ..., M n }.

Exercice 3.8.

Prove Theorem 24.

Expressive completeness of LTL+Past and LTL

We keep on focusing on the expressiveness of LTL and LTL+Past in this section.

Theorem 25 Any formula in LTL or LTL+Past can be expressed in FOMLO using at most three variables.

Exercice 3.9. Prove Theorem 25.

In many cases, the converse fails to hold, and FOMLO, even with only three variables, contains formulas that can't be expressed in LTL or LTL+Past. However, there are some interesting special cases: Theorem 26 ( [START_REF] Kamp | Tense Logic and the Theory of Linear Order[END_REF]) Over M lin(Z + ) and M lin(R + ) , any formula of FOMLO can be expressed in LTL+Past.

Theorem 27 ([GPSS80]) Over M 0 lin(Z + ) , any formula of FOMLO can be expressed in LTL.

Those theorems state that, in certain circumstances, LTL or LTL+Past contain all the expressive power of the formalism it is built on (namely first-order logic). This property is called expressive completeness.

The proofs of those results are very technical, and way beyond the scope of this course. In fact, the important point is the following corollary:

Corollary 28 Over M 0 lin(Z + ) , any formula in LTL+Past can be translated in LTL.

Exercice 3.10.

Prove that Theorem 27 does not hold over M lin(Z + ) (i.e., over general pointed linear structure) and over M 0 lin(R + ) . For this second part, consider the following two linear structures:

• S 1 = R + , ≤, 1 with 1 (t) = a if t ∈ Z + ∅ otherwise • S 2 = R + , ≤, 2 with 2 (t) = a if t ∈ Z + or 1/t ∈ Z + ∅ otherwise
and prove that they satisfy exactly the same set of LTL formulas, while there exists a formula in LTL+Past that holds only of S 1 , 0 .

Several other expressiveness results exist. Related to the above ones is the following:

Theorem 29 ([EVW02]) Any formula of FOMLO involving at most two variables can be expressed in L( F , F-1 ), and conversely.

Again, the proof of this result is rather technical, and the interested reader is invited to consult the original paper.

We conclude this section with another important expressiveness result:

Theorem 30 ([Wol83]) Over discrete time, that "φ holds at any even position along a linear structure" cannot be expressed in LTL+Past.

Exercice 3.11.

Explain why the tentative formulas below do not express the property of Theorem 30:

φ ∧ G (φ ⇔ X ¬φ) φ ∧ G (φ ⇒ X X φ)
Considering the following family of words, prove Theorem 30:

σ i = a i • b • a ω .

SATISFIABILITY OF LTL IS PSPACE-HARD

Satisfiability of LTL is PSPACE-hard

In this and the next sections of this chapter, we only consider the case of discrete time. This section is again (slightly) related to expressiveness: we prove that LTL and LTL+Past can encode, with a polynomial-size formula, the behavior of a linear-space Turing machine.

Theorem 31 ([SC85]) Satisfiability of an LTL formula is PSPACE-hard.

Note that satisfiability here means the existence of a Kripke structure all of whose executions satisfy the LTL formula.

Proof. The proof is based on the following lemma:

Lemma 32 Let T be a linear-space deterministic Turing machine. Then one can build, using logarithmic space, a polynomial-size LTL formula φ such that:

T halts on the empty word if, and only if, φ is satisfiable.

Proving this lemma obviously completes the proof of Theorem 31, since the halting problem for linear-space deterministic Turing machines is known to be PSPACE-complete.

Proof (of Lemma 32). We fix the notations: T = Q, q i , q f , Σ, #, δ, n , where Q is the set of states of the Turing machine, q i and q f are the initial and final states, Σ is the alphabet, # is a special symbol (required not to belong to Σ) representing an empty cell, δ :

Q × (Σ ∪ {#}) → Q × Σ × {←,
→} is the transition function (remember that our machine is deterministic), and n, given in unary, is the size of the tape.

The intuition of the reduction is as follows: we build a formula that will be true only on words that represent the successive configurations of the Turing machine. The set of atomic propositions is defined as follows:

AP = Q ∪ Σ ∪ {#, }
where the new symbol will be used as a configuration separator. In order to be accepted, a word will thus have to begin with the following pattern:

q, # # # # # 1 configuration = n letters a q , # # #
This example corresponds to a transition δ(q, #) = (q , a, →).

We have several properties to enforce:

1. the path should begin with , and this symbol must repeat precisely every n + 1 letters: in order to express this, we first define

φ sep = ∧ p∈AP,p = ¬p.
Then

φ 1 = φ sep ∧ G (φ sep ⇒ X (¬ ∧ X (¬ ∧ X . . . X (¬ n times ∧X φ sep ) . . .)))
2. exactly one tape head (whose position is represented by writing the current state in the correspondig cell) must appear in each configuration: we first define φ head = q∈Q q ∧ q ∈Q,q =q ¬q .

Then

φ 2 = G (φ sep ⇒ ((¬φ head ) U (φ head ∧ X ((¬φ head ) U φ sep ))))
3. there is one letter (possibly #) in each cell: we first define

φ letter = p∈Σ∪{#} p ∧ p ∈Σ∪{#},p =p ¬p .
Then:

φ 3 = G (¬ ⇒ φ letter ).
4. we have to ensure that the content of the tape is preserved from one configuration to the next one, except for the cell the tape is on:

φ 4 = G ¬φ head ⇒ p∈Σ∪{#} (p ⇒ X n+1 p) .
5. if a transition can be applied from a configuration, then the next configuration must be modified accordingly:

φ 5 = δ(q,a)=(q ,b,→) G ((q ∧ a) ⇒ X n+1 (b ∧ X q )).
Several technical details are omitted here: of course, the same kind of formula has to be written for transitions in which the tape head goes to the left, but we should also take care of the left-and right-end of the tape, as well as the case where no transition can be applied. Those details are left to the meticulous reader.

6. last, we require that the tape is initially empty, and that the execution must reach the accepting location:

φ 6 = X (# U φ sep ) ∧ F q f .
It is now a matter of bravery to prove that this formula satisfies the conditions of the lemma.

As direct corollaries, we obtain the following results:

Corollary 33 ([SC85]) LTL model-checking in PSPACE-hard.
Corollary 34 Model-checking and satisfiability are PSPACE-hard for LTL+Past.

Exercice 3.12. Prove Corollary 33.

Exercice 3.13. Quantified boolean formula (QBF) is another instance of a PSPACE-complete problem. An instance of QBF is a formula

∃p 1 . ∀p 2 . . . . ∀p 2n . φ(p 1 , p 2 , . . . , p 2n )
where φ(p 1 , p 2 , . . . , p n ) is a formula of PL built on atomic propositions p 1 to p 2n (which can be assumed to be in conjunctive normal form). Give a direct reduction (in logarithmic space) of QBF to LTL model-checking.

LTL+Past and Büchi automata

The main goal of this section is to prove that LTL+Past satisfiability (and modelchecking) are PSPACE-complete. Several proofs of this result exist, and we present below the automata-theoretic approach to LTL+Past model-checking.

Büchi automata

This approach involves finite-state automata on infinite words. We first define this formalism:

Definition 35 A finite-state automaton is a tuple A = Q, Q 0 , Σ, δ where:
• Q is a finite set of states (or locations);

• Q 0 ⊆ Q is the set of initial locations; • Σ is a finite alphabet; • δ ⊆ Q × Σ × Q it the transition relation.
Here is how an automaton "reads" words on the alphabet Σ:

Definition 36 Let A = Q, Q 0 , Σ,
δ be an automaton, and σ ∈ Σ ω be an infinite word on Σ. An execution of A over σ is an infinite sequence ρ = (q i ) i∈Z + of locations of the automaton s.t.:

• q 0 ∈ Q 0 ; • for any i ∈ Z + , (q i , σ i , q i+1 ) ∈ δ.
It remains to define when such an automaton accepts its input word. This decision is based on the set of repeated locations along the execution: Definition 37 Let ρ = (q i ) i∈Z + be an execution of an automaton A = Q, Q 0 , Σ, δ over a word σ. The set of repeated states of the execution is defined as

Inf(ρ) = {q ∈ Q | ∀i ∈ Z + . ∃j ∈ Z + . (j ≥ i ∧ q j = q)} (i.e., Inf(ρ)
is the set of locations that are traversed infinitely often along ρ).

Note that, since we required that Q be finite while executions are infinite, the set of repeated states is always non-empty.

Definition 38 A generalized Büchi automaton is a tuple A = Q, Q 0 , Σ, δ, F where: • Q, Q 0 , Σ, δ is a finite-state automaton; • F = {F 1 , ..., F p } ⊆ P(Q) is a set of sets of states.
We are now in a position to define when a word is accepted by such an automaton:

Definition 39 Let A = Q, Q 0 , Σ, δ,
F be a generalized Büchi automaton, and σ ∈ Σ ω be an infinite word on Σ. Then w is accepted by A if, and only if, there exists an execution ρ = (q i ) i∈Z + s.t.

for each set F i ∈ F , Inf(ρ) ∩ F = ∅.
We write L(A) ⊆ Σ ω for the language of A, i.e., the set of words that are accepted by A.

Example. Figure 3.1 is a graphical representation of a Büchi automaton over Σ = {a, b} that accepts precisely the words containing an infinite number of a's. In this simple example, there is only one set of accepting sets (i.e., F = {{q a }}), and that state is marked with a double line. Definition 38 defined generalized Büchi automata. Classical Büchi automata are a special case of generalized üchi automata where the acceptance condition is based on only one set of states: F = {F 1 }. Prove that generalized Büchi automata are not more expressive than classical ones, in the sense that any generalized Büchi automaton can be transformed (using at most logarithmic space) into a polynomial-size classical Büchi automaton accepting the same language.

Exercice 3.15.

Prove that the set of languages definable by Büchi automata is closed under union and intersection. Prove that this result still holds for deterministic Büchi automata.

Theorem 40 The set of languages accepted by deterministic Büchi automata is not closed under complementation.

Proof. The proof is based on a characterization of languages recognized by deterministic Büchi automata in terms of languages recognized by deterministic automata on finite words:

Definition 41 A finite-state automaton over finite words is a tuple A = Q, Q 0 , Σ, δ, F where • Q, Q 0 , Σ, δ is a finite-state automaton; • F ⊆ Q is the set of final states.
Similarly to the case of infinite words, an execution is an automaton over a finite word σ = σ 0 • • • σ k is a finite sequence ρ = q 0 • • • q k+1 s.t. q 0 ∈ Q 0 and (q i , σ i , q i+1 ) ∈ δ for each i ≤ k. Then σ is accepted whenever q k+1 ∈ F .

We prove that a language is accepted by a deterministic Büchi automaton if, and only if, it is the limit of a language accepted by a deterministic automaton over finite words:

Definition 42 Let L be an infinite set of finite words. The limit of L is defined as

lim(L) = {σ ∈ Σ ω | ∀i ∈ Z + . ∃j ≥ i. σ 0 • • • σ j ∈ L}.
That is, lim(L) is the set of infinite words having infinitely many prefixes in L.

Exercice 3.16.

Compute the following languagues lim({ba

• b n | n ∈ Z + }) lim({a m • b • a n | m, n ∈ Z + }) lim({(ab) m • b n | m, n ∈ Z + }) lim({a n b n | n ∈ Z + })
Theorem 43 A set of infinite words L is accepted by a deterministic Büchi automaton if, and only if, there exists a set of finite words L that is accepted by a deterministic automaton and s.t. L = lim(L).

Proof. Let A = Q, {q 0 }, Σ, δ, F be a deterministic automaton over finite words, and A = Q, {q 0 }, Σ, δ, F be the same automaton, but seen as a deterministic Büchi automaton. Let σ ∈ Σ ω . Then if σ ∈ L(A ), the execution ρ of A over σ enters infinitely many times in one of the states of F , say q f . Each prefix of ρ is an execution of A over a corresponding prefix of σ. Thus, infinitely many prefixes of σ are accepted by A. The converse implication follows the same lines.

Theorem 44 The set L of infinite words over Σ = {a, b} containing only finitely many a's is not accepted by a deterministic Büchi automaton.

Proof. Assume L is accepted by such an automaton. Then L = lim(L), for some language L of finite words. Then b ω ∈ L, thus b n1 ∈ L for some n 1 . In the same way,

b n1 • a • b ω ∈ L, which entails that b n1 • a • b n2 ∈ L for some n 2 .
Repeating the same argument again and again, we obtain an infinite sequence (w i ) i∈Z of words of L s.t. w i is a prefix of w i+1 and w i contains i occurrences of a. Since L is the limit of L, it contains a word having infinitely many a's, which is a contradiction.

We complete the proof by remarking that the automaton of Fig. 3.1 accepts precisely the complement of the language L used in the above theorem.

Exercice 3.17.

Prove that non-deterministic Büchi automata are closed under complement. From Theorem 40, it follows that Büchi automata are not determinizable.

From LTL+Past to Büchi automata

This section is entirely devoted to the proof of the following result:

Theorem 45 ([LPZ85]) Let φ be a formula in LTL+Past. Then one can build a (generalized) Büchi automaton A over the alphabet Σ = 2 AP , having at most 2 2|φ| states, and such that:

for any word w ∈ Σ ω . w ∈ L(A) ⇔ w, 0 |= φ.
Note that we cite [START_REF] Lichtenstein | The glory of the past[END_REF] here because it handles LTL+Past, but a the original translation of LTL to Büchi automata appeared in [START_REF] Wolper | Reasoning about infinite computation paths[END_REF].

Proof. We begin with the intuition behind this construction, and then give the technical details.

Each state of our automaton will correspond to a set of subformulas of φ that are or have to be fulfilled if the execution is accepting. For example, from a state corresponding to (among others) X ψ, outgoing transitions will go to states corresponding to (among others) ψ. That way, the automaton will "propagate" the subformulas that still have to be fulfilled. The (generalized) Büchi condition will enforce that "until" formulas are eventually fulfilled.

We now turn to the formal proof. We first need to define the set of subformulas:

Definition 46 Let φ be a formula in LTL+Past. The closure Cl(φ) of φ is the smallest set of formulas containing φ and closed under the following rules:

• for any ψ ∈ LTL+Past, ψ ∈ Cl(φ) if, and only if, ¬ψ ∈ Cl(φ) (where we identify ¬¬ψ with ψ);

• if ψ 1 ∧ ψ 2 ∈ Cl(φ) or if ψ 1 ∨ ψ 2 ∈ Cl(φ), then both ψ 1 and ψ 2 are in Cl(φ); • if X ψ ∈ Cl(φ) or if X -1 ψ ∈ Cl(φ), then ψ ∈ Cl(φ); • if ψ 1 U ψ 2 ∈ Cl(φ), then ψ 1 , ψ 2 and X (ψ 1 U ψ 2 ) are in Cl(φ); • if ψ 1 S ψ 2 ∈ Cl(φ), then ψ 1 , ψ 2 and X -1 (ψ 1 S ψ 2 ) are in Cl(φ).
With this definition, we have the following result:

Proposition 47 |Cl(φ)| ≤ 4 |φ| .
Exercice 3.18. Prove Proposition 47.

Of course, we have to enforce that a state cannot represent both a subformula ψ and its negation. Conversely, we will also require that each state represent exactly one of ψ and ¬ψ:

Definition 48 Let φ be a formula in LTL+Past. A subset S of Cl(φ) is said to be maximal consistent if the following conditions are fulfilled:

• for any ψ ∈ Cl(φ), ψ ∈ S if, and only if, ¬ψ / ∈ S;

• for any ψ 1 ∧ ψ 2 ∈ Cl(φ), ψ 1 ∧ ψ 2 ∈ S if, and only if, both ψ 1 and ψ 2 are in S;

• for any ψ 1 ∨ ψ 2 ∈ Cl(φ), ψ 1 ∨ ψ 2 ∈ S if, and only if, at least one of ψ 1 and ψ 2 is in S;

• for any

ψ 1 U ψ 2 ∈ Cl(φ), ψ 1 U ψ 2 ∈ S if
, and only if, either ψ 2 ∈ S, or both ψ 1 and X (ψ 1 U ψ 2 ) are in S;

• for any ψ 1 S ψ 2 ∈ Cl(φ), ψ 1 S ψ 2 ∈ S if, and only if, either ψ 2 ∈ S, or both ψ 1 and X -1 (ψ 1 S ψ 2 ) are in S.

Note that this definition does not forbid that a maximal consistent set contains both X p and X ¬p.

Proposition 49 For any LTL+Past formula φ, there are at most 2 2|φ| maximal consistent subsets of Cl(φ).

This result directly follows from Proposition 47.

We now turn to the formal definition of the automaton corresponding to φ. As should now be clear, the set of states will precisely be the set of maximal consistent subsets of Cl(φ). And if a subset contains a subformula X ψ, its successors will have to contain ψ.

Definition 50 Let φ be a formula in LTL+Past. The Büchi automaton associated to φ is the generalized Büchi automaton A φ = Q, Q 0 , 2 AP , δ, F satisfying the following conditions:

• Q is the set of maximal consistent subsets of Cl(φ);

• Q 0 is the subset of Q consisting of those maximal consistent subsets that contain φ and contain ¬X -1 ψ for any subformula X -1 ψ ∈ Cl(φ);

• (q, σ, q ) ∈ δ if, and only if, the following conditions are fulfilled:

for any p ∈ AP, we have p ∈ q if, and only if, p ∈ σ;

for any subformula X ψ ∈ Cl(φ), we have X ψ ∈ q if, and only if, ψ ∈ q ;

for any subformula X -1 ψ ∈ Cl(φ), we have ψ ∈ q if, and only if, X -1 ψ ∈ q .

• the set of accepting sets of states is defined as follows:

F = {q ∈ Q | ψ 2 ∈ q or ¬(ψ 1 U ψ 2 ) ∈ q} ψ 1 U ψ 2 ∈ Cl(φ) .
The size of this automaton clearly fulfills the requirements of Theorem 45. The following lemma will conclude the proof that our construction is correct:

Lemma 51 Let φ ∈ LTL+Past, and w ∈ (2 AP ) ω . Let ρ = (q i ) i∈Z + be an execution of A φ on input word w, starting in some initial state q 0 , and accepted by A φ . Then for any ψ ∈ Cl(φ), and for any n ∈ Z + ,

ψ ∈ q n ⇔ w, n |= ψ.
Proof. The proof is by induction of the structure of ψ:

• if ψ is an atomic proposition p, the proof is rather obvious: assuming p ∈ q n , we get, by construction of the transitions, that, for any (q n , σ, q ) ∈ δ, p ∈ σ. Thus p ∈ w n and w, n |= p. The converse follows the same lines;

• the proofs for boolean combinators is straightforward;

• if ψ = X ψ 1 : by construction, ψ ∈ q n if, and only if, ψ 1 ∈ q n+1 . By induction hypothesis, this is equivalent to w, n + 1 |= ψ 1 , which in turns exactly means that w, n |= ψ. The proof for ψ = X -1 ψ 1 is similar;

• if ψ = ψ 1 S ψ 2 , we prove both implications by induction on n. First, if ψ ∈ q 0 , since q 0 is an initial state, we know that is does not contain X -1 (ψ 1 S ψ 2 ). By construction, q 0 must contain ψ 2 , and by induction hypothesis, w, 0 |= ψ 2 , hence w, 0 |= ψ. The converse follows the same lines.

Now, if the result holds up to some posittion n -1, assume that φ ∈ q n . Then, by construction of maximal consistent sets, either ψ 2 ∈ q n , or both ψ 1 and X -1 (ψ 1 S ψ 2 ) are in q n . The former case is straightforward. In the latter, by construction, we get that ψ 1 S ψ 2 ∈ q n-1 . We get that w, n |= ψ 1 (from the induction hypothesis on ψ) and w, n -1 |= φ 1 S ψ 2 (by induction hypothesis in n). This immediately yields that w, n |= ψ 1 S ψ 2 . Again, the other direction is symmetric.

• we conclude this proof with the case ψ = ψ 1 U ψ 2 . Assume ψ ∈ q n . Since the run is accepted by the automaton, we know that one state of {q ∈ Q | ψ 2 ∈ q or ¬(ψ 1 U ψ 2 ) ∈ q} will be encountered after q n along ρ. We reason by induction on the distance d between q n and the next such state. If d = 0, then ψ 2 ∈ q n , since it can't be the case that ¬(ψ 1 U ψ 2 ) ∈ q n . By induction hypothesis, we get the result. Now, assuming the result holds up to distance d -1 with d > 1, suppose the distance between q n and the next accepting state for ψ 1 U ψ 2 is d. Then q n is not accepting, and thus it does not contain ψ 2 . It shall then contain both ψ 1 and X (ψ 1 U ψ 2 ). It follows that q n+1 contains ψ 1 U ψ 2 . The distance between q n+1 and the next accepting state is then d -1, which entails, by indcution on d, that w, n + 1 |= ψ 1 U ψ 2 . now, since q n contains ψ 1 , we obtains that w, n |= ψ 1 U ψ 2 .

Conversely, if w, n |= ψ 1 U ψ 2 , then there exists an integer d s.t. w, n + d |= ψ 2 , and for any i ∈ [0, d), w, n + i |= ψ 1 . By induction hypothesis, q n+d contains ψ 2 , thus also ψ 1 U ψ 2 , and all q n+i contain ψ 1 . An easy inductive argument proves that ψ 1 U ψ 2 ∈ q n , and concludes the proof.

Example. Figure 3.2 displays the Büchi automaton corresponding to formula a U (b ∧ X -1 b). the closure of this formula contains 12 subformulas, thus the automaton could contain up to 2 6 , i.e., 64 states. Still, consistency requirements lower this value to 16. For the sake of clarity, labels are not shown on transitions, since they correspond, by construction, to the set of atomic propositions labeling the source state.

Exercice 3.19.

Compute the Büchi automaton corresponding to a U (b∧ X -1 b). Can you build a smaller Büchi automaton that accepts the same language? Can you build a deterministic Büchi automaton that accepts the same language?

Application to verification

The transformation above has very interesting algorithmic consequences: the satisfiability of an LTL+Past formula is equivalent to the non-emptiness of the language accepted by the associated Büchi automaton. While testing for the non-emptiness for Büchi automata is NLOGSPACE-complete (this in PTIME), the naive approach only yields an EXPTIME algorithm since the Büchi automaton associated to an LTL+Past formula has exponential size. This does not match the lower bound that we established in Theorem 31.

Still, this automata-theoretic approach can yield an optimal algorithm:

Theorem 52 Satisfiability of an LTL+Past formula can be achieved in PSPACE.

Proof. Instead of building the whole Büchi automaton associated to the formula φ under study, the technique consists in building an accepting execution of the automaton "on the fly", in a non-deterministic manner (which is fine since PSPACE = NPSPACE).

The algorithm first guesses an initial state q 0 and a set of accepting states q 1 to q p (one state per set of accepting states of the generalized Büchi condition). It then guesses, on the fly, sequences of states of the Büchi automaton that run from q 0 to q 1 , from q 1 to q 2 , and so on, and from q p to q 1 . Here, "on the fly" means that the algorithm generates a set of subformulas of φ, check that it is maximal consistent, and that there is a transition from the previous state to this one.

Clearly, the language of the automaton is non-empty if, and only if, such choices are possible. Now, this algorithm only needs polynomial space, since it only has to store the states q 0 to q p , plus the previous-and current state of the sequence it is guessing during the second phase, and a small amount of auxiliary informations.

This algorithm runs in space O(|φ| 2 ) and in time O(|φ| 2 × 2 2|φ| ).

Exercice 3.20.

Explain the above space-and time bounds of the algorithm for LTL+Past satisfiability.

An immediate corollary of this algorithm is the "ultimately-periodic model property" for LTL+Past:

Corollary 53 If a formula φ in LTL+Past is satisfiable, then there exist two finite words u, v ∈ (2 AP ) * s.t. u • v ω , 0 |= φ and |u| + |v| ≤ |φ| • 2 2|φ| .
The same complexity can be achieved for model-checking:

Theorem 54 LTL+Past model-checking is in PSPACE.
Proof. The algorithm is very similar, but the algorithm now guesses pairs of states: one state of the Büchi automaton corresponding to the formula φ, and one state of the Kripke structure K.

While Remark. It is important to notice that, practically, the time-complexity of LTL+Past model-checking is exponential only in the size of the formula (which is generally rather small), while it is linear in the size of the Kripke structure (which is often very large). The same difference applies to space-complexity: the algorithm is (non-deterministic) logarithmic space in the size of the Kripke structure, and polynomial only in the size of the formula.

As a corollary of these results and those of Section 3.4, we get:

Theorem 55 Model-checking and satisfiability for LTL and LTL+Past are PSPACEcomplete.

When the full expressiveness of LTL+Past is not needed, it is possible to find sublogics that enjoy better complexity. We present one such case here.

Definition 56 The fragment of LTL without temporal nesting, denoted with LTL 1 , is the fragment of LTL defined by the following grammar:

LTL 1 φ m ::= φ p | ¬φ m | φ m ∨ φ m | φ m ∧ φ m | X φ p | φ p U φ p φ p ::= | p | ¬φ p | φ p ∨ φ p | φ p ∧ φ p
where p ranges over AP.

We now prove that, from the ultimately-periodic-model property of LTL+Past, we can derive a small-model property, that is claimed as follows:

Proposition 57 ([DS02]) If a formula φ in LTL 1 is satisfiable, then there exist two finite words u, v ∈ (2 AP ) * s.t. u • v ω , 0 |= φ and |u| + |v| ≤ |φ| • 2 |φ|.
Proof. The proof consists in "extracting" polynomialy many witnesses from the exponential ultimately-periodic witness given by Corollary 53.

Let φ ∈ LTL 1 , and w = u • v ω be an ultimately-periodic word witnessing φ. We select a family of witnesses as follows:

• 0 is a witness;

• if φ contains a subformula of the form X ψ, then 1 is a witness;

• for any subformula ψ 1 U ψ 2 of φ, several cases may arise:

-if w, 0 |= ψ 1 U ψ 2 , then the smallest i s.t. w, i |= ψ 2 is a witness; -if w, 0 |= ψ 1 U ψ 2 but w, 0 |= F ψ 2 , then the smallest i s.t. w, i |= ψ 1
is a witness;

otherwise, we select no witness.

Clearly, this procedure selects at most |φ| integers, all of which are less than |u| + |v|. We write {i 0 , i 1 , ..., i k } for the (ordered) set of witnesses, with i 0 = 0. We define two words

u = w i0 w i1 • • • w ip and v = w ip+1 w ip+2 • • • w i k , with i p < |u| ≤ i p+1 .
That way, u is a subword of u, v is a subword of v, and both subwords have size linear in the size of φ. It remains to show that u • v ω satisfies φ. In the sequel, we write w for u • v ω . The proof is by induction on the structure of φ: the base cases (including the case where φ = X φ 1 ) are obvious, and we focus on the case where φ = φ 1 U φ 2 . We prove that w |= φ iff w |= φ.

Assume w, 0 |= φ. Then there exists a position i s.t. w, i |= φ 2 , and such that all intermediate positions satisfy φ 1 . If we assume that i is the smallest such position, then state w i occurs in w as w i (and we have w , i |= φ 2 since φ 2 is a propositional logic formula), and all intermediate positions along w correspond to intermediate positions along w (and each of them thus satisfy φ 1 ). As a consequence, w , 0 |= φ.

Conversely, if w, 0 |= φ, then two cases may arise: either w, 0 |= F φ 2 , in which case it is also the case for w , or w, 0 |= F φ 2 , but some earlier position not satisfying φ 1 occurs in w . In both cases, w , 0 |= φ.

Theorem 58 Deciding the satisfiability of a formula of LTL 1 is NP-complete.

Proof. The algorithm consists in guessing an ultimately-periodic witness u • v ω , and verifying that it really satisfies the formula. We know that the first part can be achieved in polynomial time. The second part is an easy labeling algorithm: it consists in labeling each state of the witness with the subformulas it satisfies (using the obvious fact that two positions p and p + |v|, with p ≥ |u|, satisfy the same subformulas).

Theorem 59 Model-checking LTL 1 is NP-complete.

Proof. The argument is similar: from a path satisfying φ ∈ LTL 1 , we know that only polynomialy many witnesses are needed. Clearly, there exists a polynomial path containing those witnesses. The algorithm consists again in guessins a path and checking that it really satisfies the formula.

Application to expressiveness

The automata-theoretic approach also gives a surprising way of proving the following expressiveness result: Theorem 60 ([LMS02]) LTL+Past can be exponentially more succinct than LTL.

That is, there exists a sequence of formulas of LTL+Past whose translations in LTL are exponentially larger.

Proof. We consider the following property:

Any two states that agree on atomic propositions p 1 to p n also agree on proposition p 0 .

p i = a i )) ⇒ (G (( i∈[1,n] p i = a i ) ⇒ p 0 = a 0 )).
The set of words satisfying this property can thus be accepted by a Büchi automaton. It turns out that we have the following lemma: Lemma 61 ([EVW02]) Any Büchi automaton that accepts exactly the set of words satisfying Equation (3.1) has at least 2 2 n states.

Proof. Let {a 0 , a 1 , ..., a 2 n -1 } be the set of letters built on atomic propositions {p 1 , ..., p n } (note that p 0 is not included here). There are 2 n such letters.

For each subset K ⊆ {0, 1, ..., 2 n -1}, we define a set of letters {b 0 , ..., b 2 n -1 } as follows:

b i = a i if i / ∈ K a i ∪ {p 0 } otherwise.
Then, with each subset K, we associate a finite word w K = b 0 b 1 ... b 2 n -1 . Clearly, whenever K = K , then w K = w K . Thus, this construction defines 2 2 n different finite words. It is clear also that for any K, the word w K ω satisfies Equation (3.1), while the word w K • w K ω does not, as soon as K = K . Now, let A be an automaton accepting exactly the words satisfying Equation (3.1). Let S K be the set of states that can be reached from an initial state of A after reading the finite word w K . Clearly, this set is non-empty, since w K is the prefix of an accepted word. Now, if S K ∩ S K = ∅ for two different sets K and K , then the word w K • w K ω would be accepted by the automaton. Thus the sets S K do not intersect, which entails that A has at least 2 2 n states.

As a corollary of Theorem 45, any LTL+Past formula expressing the property of equation (3.1) has size at least 2 n-1 .

We now consider a slightly different property:

Any state that agrees with the initial state on atomic propositions p 1 to p n also agree with the initial state on proposition p 0 .

(3.2) This formula can be captured by a polynomial-size LTL+Past formula:

G   ( i∈[1,n] (p i ⇔ F -1 G -1 p i )) ⇒ (p 0 ⇔ F -1 G -1 p 0 )   . (3.3)
It can thus also be expressed in LTL (again, possibly by enumerating the set of initial valuations). Let φ be an LTL formula expressing the property of Equation (3.2). Since φ is a pure-future formula, formula G φ precisely expresses the property of Equation (3.1), and thus has size at least 2 n-1 . Thus |φ| ≥ 2 n-1 -1. Thus LTL can only express the LTL+Past formula (3.3) with exponentialsize formulas.

Exercice 3.22.

The proof above requires infinitely many atomic propositions. This is in contradiction with our original requirement that the set AP must be finite. Prove that the result still holds with only a finite number of atomic propositions.

Chapter 4

Branching-time temporal logics 4.1 Tree structures

Similarly to linear-time temporal logics, branching-time temporal logics express properties on the evolutions of a system along time. The difference is that branching-time logics consider the whole set of possible evolutions of the system, while linear-time logics only deal with one execution at a time. We begin with formally defining tree structures, which are the branching-time equivalent to linear structures (see Definition 16).

Definition 62 A (labeled) tree structure is a tuple S = T, ≤, where:

• T, ≤ is a tree-ordered (infinite) set (i.e., a partially-ordered set such that, for each t ∈ T , the set {u ∈ T | u ≤ t}, ≤ is totally ordered and has a least element) with the following two additional requirements:

a branch is a maximal totally-ordered subset of T . Each branch of a tree structure is required to be infinite. We write Br(t) for the set of branches of T containing t;

a root is a minimal element of T . It is required that a tree structure has finitely many roots (and, sometimes, only one);

• : T → 2 AP labels each point of T with a subset of AP.

It should be remarked that a branch is well-ordered, and can thus be seen as a linear structure. As in the case of linear time, only two kinds of tree structures are really relevant to computer science: those in which all branches are isomorphic to R + , and those in which all branches are isomorphic to Z + . In the sequel, we will only consider discrete-time, where all branches are isomorphic to Z + . Definition 63 Let K = W, R, l be a Kripke structure, and w ∈ W . The computation tree of K from w is the tree structure T, ≤, where • T is the set of finite words over W whose first letter is w, and s.t., for any two consecutive letters w i and w i+1 , (w i , w i+1 ) ∈ R;

• ≤ is the lexicographic order over T ;

• maps each word to the label of its last letter: (w 0 , w 1 , ..., w n ) = l(w n ).

Exercice 4.23.

Prove that the computation tree of a finite-state Kripke structure is a tree structure whose branches are isomorphic to Z + . Definition 64 A pointed tree structure is a couple S, s where S = T, ≤, is a tree structure, and s ∈ T . We write M br(T ) for the set of pointed tree structures built on the time-line T .

Branching-time temporal logics

There are two ways of defining branching-time temporal logics:

• either as an extension of LTL (or LTL+Past) with path quantifiers;

• or as a truly modal logic, i.e., a logic built on boolean operators and a set of modalities.

We will mostly use the first definition here, and will only mention links with the second definition as exercises. Thus, given a pointed tree structure S, s , we define two path quantifiers as follows:

• E (there exists a path):

S, s |= Eφ def ⇔ ∃b ∈ Br(s). b, s |= φ.
• A (for all paths):

S, s |= Aφ def ⇔ ∀b ∈ Br(s). b, s |= φ.
This definition is rather informal for the moment, but will be make more precise at Definition 67.

Example. Formula E(F p ∧ F q) means that, along some path, a state labeled with p and one labeled with q are reachable. This is of course different from EF (p ∧ q), which requires that one state labeled with both p and q is reahcable, but also from EF p ∧ EF q, which states that p is reachable in one branch and q in another (but, of course, possibly the same) branch.

Similarly, AG p means that all reachable states are labeled with p. This is equivalent to saying that any state that is not labeled with p is not reachable.

In fact, we again have an obvious duality between our two new operators:

Proposition 65 Both path quantifiers are dual to each other: for any φ ∈ LTL+Past, Aφ ≡ ¬ E¬φ.

We now define the syntax of three important families of branching-time temporal logics: Definition 66 Given a set {M 1 , ..., M n } of n first-order definable modalities, we define the following three branching-time logics:

• the syntax of B(M 1 , ..., M n ) is given by:

B(M 1 , ..., M n ) φ b ::= p | ¬φ b | φ b ∨ φ b | φ b ∧ φ b | Eφ l | Aφ l φ l ::= M 1 (φ b , ..., φ b ) | • • • | M n (φ b , ..., φ b )
where p ranges over AP.

• the syntax of B + (M 1 , ..., M n ) is given by:

B + (M 1 , ..., M n ) φ b ::= p | ¬φ b | φ b ∨ φ b | φ b ∧ φ b | Eφ l | Aφ l φ l ::= ¬φ l | φ l ∨ φ l | φ l ∧ φ l | M 1 (φ b , ..., φ b ) | • • • | M n (φ b , ..., φ b )
where p ranges over AP.

• the syntax of B * (M 1 , ..., M n ) is given by:

B * (M 1 , ..., M n ) φ b ::= p | ¬φ b | φ b ∨ φ b | φ b ∧ φ b | Eφ l | Aφ l φ l ::= φ b | ¬φ l | φ l ∨ φ l | φ l ∧ φ l | M 1 (φ l , ..., φ l ) | • • • | M n (φ l , ..., φ l )
where p ranges over AP.

Formulas defined as φ l are called path formulas, while those defined as φ b are state formulas.

Again, for modalities U and X, the corresponding logics have been given special names ("CTL" stands for "computational tree logic"):

CTL = B( U , X ) CTL s = B( Ũ ) CTL + = B + ( U , X ) CTL + s = B + ( Ũ ) CTL * = B * ( U , X ) CTL * s = B * ( Ũ )
Example. In CTL, each modality has to be preceeded with a path quantifier: EF p is a CTL formula, but E(F p ∧ F q) and E(F G p) are not (at least, syntactically).

Clearly enough, CTL + contains CTL: CTL + allows boolean combinations of modalities in the scope of path quantifiers. Still, modalities cannot be directly nested. Thus, EF p and E(F p ∧ F q) are two formulas of CTL + , but E(F G p) does not follow the syntax of CTL + .

Last, it is clear again that CTL * subsumes CTL + : CTL * allows the nesting of modalities. All three formulas EF p, E(F p ∧ F q) and E(F G p) are CTL * formulas.

We now define the precise semantics of CTL * . The semantics of the other logics will follow.

Definition 67 Let S = T, ≤, be a tree structure, s ∈ T , and b ∈ Br(s). Let φ b , ψ b be two state formulas for CTL * semantics, and φ l , ψ l be two path formulas for CTL * semantics. We recursively define two relations, denoted with |= b and |= l , for the satisfaction of state-and path formulas, respectively:

S, s |= b p ⇔ p ∈ (t) S, s |= b ¬φ b ⇔ S, s |= b φ b S, s |= b φ b ∨ ψ b ⇔ S, s |= b φ b or S, s |= b ψ b S, s |= b φ ∧ ψ ⇔ S,
|= l ψ l S, b, s |= l X φ l ⇔ ∃t ∈ b. t > s ∧ ∀u. (u ≤ s ∨ t ≤ u) ∧ S, b, t |= l φ l S, b, s |= l φ l U ψ l ⇔ ∃t ∈ b. (s ≤ t ∧ ( S, b, s |= l ψ l ))∧ ∀u ∈ b. ((s ≤ u ∧ u ≤ t) ⇒ S, b, u |= l φ l )
In the sequel, we write |= for |= b . Given a Kripke structure K = W, R, l , some state w ∈ W , and a CTL formula φ, we write K, w |= φ when S K,w , w |= φ, where S K,w is the computation tree of K from w.

Of course, in a similar way as for linear-time, we can define a strict version Ũ of U . It is also possible to define other one-place modalities, e.g. F and G, from U. Exercice 4.24.

Prove, by exhibiting a witnessing Kripke structure, that the following formulas are satisfiable: Prove that two states are bisimilar if, and only if, they satisfy the same formulas of CTL. Prove that E(p U q ∧ ¬(r U s)) can be expressed in CTL over discrete time. Prove that CTL + is not more expressive than CTL.

E(F p ∧ F q) ∧ ¬ EF (p ∧ EF q) EG (¬p ∧ EF p) EG ( EF p) ∧ ¬ EG F p EG F p ∧ ¬ EG ( AF p)
Exercice 4.27.

As mentionned at the beginning of this section, it is possible to define CTL in a really modal way. Define two one-place modalities EX and AX, and two two-place modalities EU and AU, and prove that CTL is equivalent to the logic defined from atomic propositions, boolean combinators, and those four modalities.

There is a characterization of CTL * in terms of monadic second-order logic, analogous to Theorems 25, 26 and 27:

Lemma 68 CTL * can be expressed in SOMLO.

Exercice 4.28.

Prove Lemma 68.

Exercice 4.29. Show that monadic second-order logic is strictly more expressive than CTL * .

Still, there exists a fragment of monadic second-order logic that precisely characterizes CTL * : monadic path logic (MPL) is the restriction of monadic second-order logic where second-order quantification is restricted to quantify only on infinite branches, rather than on any set of states. MPL is then still more expressive than CTL * because it can express that a state has, for instance, exactly two successors labeled with p, while CTL * can only say that one or all of the successors have that property. By refining a little bit more:

Theorem 69 ([MR99]) Any formula in MPL that is invariant under bisimulation can be expressed in CTL * .

Bisimulation has been defined at Exercice 4.25: it allows here to consider only formulas of MPL that, roughly, will not count the number of successors of nodes.

Between CTL and CTL *

A fairness property is a property stating that something occurs infinitely often (cf. Exercise 3.7). LTL can express this class of properties: formula G F p precisely states that p occurs infinitely often along p (along infinite paths).

Of course, CTL * can express fairness: formula AG F p states that p occurs infinitely often along any path. Unfortunately, CTL cannot express fairness.

Exercice 4.30.

Using the families of Kripke structures depicted on Figure 4.2 prove that CTL cannot express fairness. Of course, CTL * can express fairness, but also much more. Intermediate logics have been defined in order to extend CTL with only fairness: Definition 70 Let S = T, ≤, be a tree structure, s ∈ T , and b ∈ Br(s). Let φ l be a path formula for CTL * semantics. Modality ∞ F is defined as follows:

S, b, s |= l ∞ F φ l ⇔ ∀t ∈ b. ∃u ∈ b. t ≤ u ∧ S, b, u |= l φ l
With this definition, formula E ∞ F φ is precisely equivalent to the CTL * formula EG F φ. With this modality, the following two logics are defined:

ECTL = B( U , X , ∞ F ) ECTL + = B + ( U , X , ∞ F )

Model-checking branching-time logics

One important feature of CTL is that it enjoys very efficient model-checking algorithms:

Theorem 71 CTL model-checking is PTIME-complete.

Proof. We begin with PTIME-hardness, proving that the CIRCUIT-VALUE problem can be encoded in a CTL model-checking problem. CIRCUIT-VALUE consists in computing the value of the root of a directed acyclic graph whose nodes represent boolean connectives, and having two leaves and ⊥. An example of such a circuit is depicted on Figure 4.3. This problem is known to be

∧ ∨ ∧ ¬ ∧ ∨ ∨ ∧ ⊥ Figure 4.3: The CIRCUIT-VALUE problem PTIME-complete [GHR95].
It is now rather easy to build a Kripke structure K and a CTL formula φ s.t. K |= φ if, and only if, the circuit evaluates to true.

We now prove that CTL model-checking can be achieved in PTIME. We are given a Kripke structure K = W, R, l , one of its states w ∈ W , and a CTL formula φ. The principle of the algorithm is to recursively label each state of K with the subformulas that hold at that state. For this proof, we use the modal definition of CTL, as presented at Exercise 4.27. Moreover, it is easy to prove that the whole expressive power of CTL can be obtained from only modalities EX , E U and AF . We thus only describe our labeling algorithm for those modalities, plus atomic propositions and boolean operators:

• for atomic propositions: a state q ∈ W is labeled with an atomic proposition p if, and only if, p ∈ l(q);

• if φ 1 ∨ φ 2 is a subformula of φ, assuming the labeling procedure has already been applied to subformulas φ 1 and φ 2 , we label each state q ∈ W with φ 1 ∨ φ 2 if, and only if, it is already labeled with φ 1 or with φ 2 ;

• the algorithm is similar for conjunction and negation of subformulas;

• if EX φ 1 is a subformula of φ, a state q ∈ W is labeled with EX φ 1 if, and only if, one of its successors by R is labeled with φ 1 ;

• if E(φ 1 U φ 2 ) is a subformula, we begin with labeling each state satisfying φ 2 with E(φ 1 U φ 2 ); Then, each state labeled with φ 1 and having one of its successors by R labeled with E(φ 1 U φ 2 ) is in turn labeled with E(φ 1 U φ 2 ). The procedure is applied until a fixpoint is reached;

• if AF φ 1 is a subformula, we begin with labeling states satisfying φ 1 with AF φ 1 . Then, if all the successors of a state have been labeled with AF φ 1 , then we also label that state with AF φ 1 . This procedure is applied until a fixpoint is reached.

In the end, K, w |= φ if, and only if, w has been labeled with φ. That the algorithm terminates (i.e., that a fixpoint is reached in each procedure described above) is rather obvious: the number of labeled states can only increase, and it is bounded with the size of W . For each subformula, it is easy to implement the above procedures so that they execute in time

O(|W | 2 ). The global algorithm is thus in time O(|φ| • |W | 2 )
. We now prove that this algorithm is correct. Following the algorithm, the proof is by induction on the structure of φ: we prove that each procedure describes above labels exactly the set of states that satisfy the corresponding formula:

• it is obvious for atomic propositions and for boolean combinations;

• for subformula EX φ 1 : a state is labeled with this subformula if, and only if, it has an immediate successor satisfying φ 1 , i.e., if, and only if, it satisfies EX φ 1 ;

• for subformula E(φ 1 U φ 2 ): a state is labeled with this formula either because it is labeled with φ 2 , or because it is labeled with φ 1 and has a successor labeled with E(φ 1 U φ 2 ). By an obvious induction, this entails that it satisfies E(φ 1 U φ 2 ). Conversely, if a state q satisfies E(φ 1 U φ 2 ), then there is a finite path from q to a state satisfying φ 2 with intermediary states labeled with φ 1 . It is then obvious that all the states of that path will eventually be labeled with E(φ 1 U φ 2 );

• for AF φ 1 : again, a state can be labeled with AF φ 1 either because it is labeled with φ 1 , or because all of its successors are labeled with AF φ 1 . An easy inductive argument proves that it then satisfies AF φ 1 . Conversely, if a state q satisfies AF φ 1 , then there exists a finite "distance" within which all paths issued from this state will have encountered φ 1 (because the Kripke structure is finite). Again, by induction on this distance, we prove that q will be labeled with AF φ 1 .

Exercice 4.31.

Write the reduction of CIRCUIT-VALUE to CTL modelchecking.

Exercice 4.32.

Using the programming language of your choice, write the complete labeling algorithms for CTL model-checking.

Exercice 4.33.

Our algorithm only involves modalities EX, EU and AF, as we explained that any CTL formula can be written with only those modalities. Prove this fact. From a formula φ ∈ CTL, prove that the size of the resulting formula can be exponential in the size of the original formula. Does our algorithm suffer from this exponential blowup? Exercice 4.34.

Prove that, unless NP = PTIME, CTL + cannot be model-checked in polynomial time.

Exercice 4.35.

Prove that ECTL model-checking is PTIME-complete.

Since CTL * contains LTL, we know that CTL * model-checking is PSPACE-hard. It turns out that this lower bound is optimal:

Theorem 72 ([EH86]) CTL * model-checking is PSPACE-complete.
Proof. The algorithm again consists in labeling states with the subformulas they satisfy. Given a formula Aφ, we transform φ into a pure LTL formula be replacing its state subformulas with new, fresh atomic propositions, assuming (by induction) that the Kripke structure has already been labeled with those atomic propositions. It then suffices to apply the standard LTL model-checking algorithm, for each state of the Kripke structure, on order to find all the states that satifsy Aφ.

Subformulas Eφ are handled as ¬ A¬φ. From the complexity of LTL modelchecking, the time-complexity of the algorithm is

O(|φ| 3 • |K| 2 • 2 2|φ| ), and
space-complexity O(|K| • |φ| 2 ).
Remark. As for LTL (see the remark following Theorem 54), the time-complexity is only exponential in the formula, and remains polynomial in the size of the Kripke structure. Still, the space needed for this algorithm is polynomial also in the size of the Kripke structure. In fact, compared to LTL and CTL, CTL * is often considered to be too complex and too expressive. The logic ECTL + is often considered to be the rigth extension of CTL in terms of its expressiveness.

The model-checking problem for this logic is ∆ P 2 -complete (i.e., higher than NP and coNP, and below PSPACE) [START_REF] Laroussinie | Model checking CTL + and FCTL is hard[END_REF].

Using a similar argument and the result of Theorem 58, we get an upper bound for CTL + model-checking:

Theorem 73 Model-checking CTL + is in ∆ P 2 .
The class ∆ P 2 , also written PTIME NP , is the class of problem solvable in deterministic polynomial time with an access to an NP oracle (i.e., a device that answers in one step to instances of an NP-complete problem). This class contains NP and co-NP, and is contained in PSPACE. It is not known whether those inclusions are strict.

We now prove that this algorithm is optimal:

Theorem 74 Model-checking CTL + is ∆ P 2 -hard.
Proof. We first have to find a starting point, i.e., a ∆ P 2 -complete problem. We will use the following one:

SNSAT:

Input: p families of variables Z r = {z 1 r , ..., z m r }, p variables x r , p boolean formulae φ r in 3-CNF, with φ r involving variables in Z r ∪ {x 1 , ..., x r-1 }.

Output: The value of z p , defined by

               x 1 def = ∃Z 1 . φ 1 (Z 1 ) x 2 def = ∃Z 2 . φ 2 (z 1 , Z 2 ) x 3 def = ∃Z 3 . φ 3 (z 1 , , z 2 , Z 3 ) . . . x p def = ∃Z p . φ k (z 1 , ..., z p-1 , Z p )
This problem is obviously in ∆ P 2 , and turns out to be complete for that class [START_REF] Laroussinie | Model checking CTL + and FCTL is hard[END_REF][START_REF] Cadoli | An algorithm to evaluate quantified boolean formulae[END_REF]. We prove that it can be encoded as a CTL + modelchecking problem. The Kripke structure used in this reduction is depicted on Figure 4.4. As is usual in this kind of reduction, a valuation of the variables will correspond to a trajectory in that structure (visiting v if, and only if, variable v is false). Nodes C will be used for ensuring that, when a variable x i is set to false, then it is really the case that there is no valuation that fulfills φ i .

We now recursively define a sequence of formulas as follows:

ψ 0 = ψ k = E G [(x 1 ∨ . . . ∨ x p ) ⇒ EX (C ∧ EX ¬ψ k-1 )] ∧ G ¬C ∧ p i=1 [(F x i ) ⇒ φ F i (x 1 , ..., x i-1 , Z i )]
where

φ F i (x 1 , ..., x i-1 , Z i ) is the formula φ i in which each variable v ∈ {x 1 , ..., x i-1 }∪ Z i is replaced with F v.
Roughly, formula ψ k selects a trajectory that nevers goes in a C-state, thus defining a valuation for variables in x 1 , ..., x n , and ensures that the valuation of the x i 's are correct. Formally:

Lemma 75 For any k ∈ Z + and r ≤ p, Proof. The proof is by induction on k. The case when k = 0 holds vacuously.

(1) if k ≥ 2r -1, then v I (x r ) = if,
Assume the result holds up to some k ≥ 0. Let r ≤ p.

• Let w be a valuation of all the variables of Z 1 ∪ • • • ∪ Z p ∪ {x 1 , ..., x p } that coincides with v I on {x 1 , ..., x p }, and such that w(x i ) = iff φ i (w(x 1 ), ..., w(x i-1 ), w(Z i )).

To w corresponds a trajectory π w of the Kripke structure. We consider the suffix of π w that starts in x r or x r . We prove that if k ≥ 2r -1 (resp. k ≥ 2r), then π witnesses the fact that x r |= ψ k (resp. x r |= ψ k ).

Clearly, π satisfies G ¬C. From the requirement on w, we also have that

π |= p i=1 [(F x i ) ⇒ φ i (x 1 , ..., x i-1 , Z i )].
Now, when π visits a state x i , then v I (x i ) = ⊥. If i = r (in which case we are proving (2), since otherwise π cannot visit x i ), then k ≥ 2r ≥ 2i; otherwise, i < r, and also k ≥ 2i. Thus k -1 ≥ 2i -1, and by induction hypothesis, since it is not the case that v I (x i ) = , we get that

x i |= ψ k-1 . Thus x i |= EX (C ∧ EX ¬ψ k-1 ).
Conversely, assume k ≥ 2r -1 and x r |= ψ k (resp. k ≥ 2r and x r |= ψ k ). Then there is a trajectory π from x r (resp. x r ) witnessing ψ k , thus satisfying G ¬C and defining a valuation w of variables Z 1 ∪ • • • Z p ∪ {x 1 , ..., x r }. We prove, by induction on i, that w(x i ) = v I (x i ) for i ≤ r.

When i = 1, if w(x 1 ) = , then π visits x 1 , and thus valuation w is a witness that φ 1 (Z 1 ) is satisfiable. Conversely, if w(x 1 ) = ⊥, then π visits x 1 , and we get that x 1 |= ¬ψ k-1 . We claim that k -1 ≥ 1: indeed, the contrary would mean that r = 1 and that π starts in x 1 . Thus we can apply the induction hypothesis: that x 1 |= ¬ψ k-1 implies that v I (x 1 ) = ⊥.

Assume w(x j ) = v I (x j ) for any j < i.

if w(x i ) = , then we know that φ i (w(x 1 ), ..., w(x i-1 ), Z i ) is true.

Since w(x j ) = v I (x j ), it follows that φ i (v (x 1 ), ..., v I (x i-1 ), Z i ) is satisfiable, and that v I (x i ) = .

conversely, if w(x i ) = ⊥, then x i |= EX (C ∧ EX ¬ψ k-1 ), and x i |= ψ k-1 . If i < r, then k -1 ≥ 2i -1, and the induction hypothesis yields v I (x i ) = ⊥. If i = r, then we know that π visits x r , so that we must be in the case where k ≥ 2r. Then k -1 ≥ 2i -1, and the induction hypothesis entails that v I (x i ) = ⊥.

As an immediate consequence, we get that v I (x n ) = if, and only if, x n |= ψ 2n-1 , which concludes the proof.

Corollary 76 Model-checking CTL + is ∆ P 2 -complete.

4.5 CTL and alternating tree automata 4.5.1 Alternating tree automata

In the case of LTL and LTL+Past, satisfiability and model-checking are handled very similarly (by the automata-theoretic approach). In the case of branchingtime logics, this is not the case: satisfiability is much harder. Still, satisfiability can be checked very nicely with automata theory. This requires some new stuff to be introduced.

Definition 77 A tree automaton is a tuple A = Q, Q 0 , Σ, δ where

• Q is a finite set of states;

• Q 0 ⊆ Q is the set of initial states;

• Σ is a finite alphabet;

• δ ⊆ Q × σ × { , ♦ } × Q is the transition relation.
A tree automaton takes a tree as input:

Definition 78 Let A = Q, Q 0 , Σ, ∆ be a tree automaton, and T = T, ≤, be a tree-structure (with a single root t 0 ) with : T → Σ. An execution of A on the input tree T is a labeled tree T A = T, ≤, sith : T → Q s.t.:

• (t 0 ) ∈ Q 0 ;
• for any t ∈ T , there exists (m, q) ∈ { , ♦ } × Q s.t. :

-( (t), (t), m, q) ∈ δ;

if m = ♦ , then there exists a successor node t of t s.t. (t ) = q;

if m = , then for any immediate successor t of t, (t ) = q.

The acceptance condition is again given in terms of the states that repeat infinitely often along branches:

Definition 79 A Büchi tree automaton is a tuple A = Q, Q 0 , Σ, δ, F where • Q, Q 0 , Σ, δ is a tree automaton; • F ⊆ Q is a set of accepting states.
Definition 80 A single-root tree T = T, ≤, is accepted by a Büchi tree automaton A = Q, Q 0 , Σ, δ, F is there exists an execution T A = T, ≤, of A over T s.t., for any branch b of T A ,

Inf(b) ∩ F = ∅ where Inf(b) = {q ∈ Q | ∀t ∈ b. ∃u ∈ b. t ≤ u ∧ (t) = q}.
Example. Let A = {q a , q b }, {q a }, {a, b}, δ, {q a } be the automaton with the following transition relation: δ = {(q a , a, , q a ), (q a , b, , q b ), (q b , a, , q a ), (q b , b, , q b )}. q b qa qa q b q b q b q b qa qa q b q b Figure 4.5: Execution of a tree automaton entered each time an a is read. Since that state must appear infinitely often, the intuition is that A accepts exactly those trees whose all branches contain infinitely many a's. It can easily proved that this intuition is correct: this automaton accepts the set of tree structures satisfying formula A ∞ F a.

Exercice 4.36.

Let A = {q 0 , q 1 , q 2 }, {q 0 }, {a, b}, δ, {q 0 , q 1 } be the automaton with the following transition relation: δ = {(q 0 , a, ♦ , q 1 ), (q 0 , b, ♦ , q 1 ), (q 1 , a, ♦ , q 1 ), (q 1 , b, ♦ , q 2 ), (q 2 , a, ♦ , q 2 ), (q 2 , b, ♦ , q 2 )}.

Prove that this automaton accepts exactly the set of trees satisfying a CTL formula.

We now extend non-deterministic automata (on both words or trees) to alternating automata. The intuition is as follows: compared to a deterministic automaton, a non-deterministic one may propose several possible transitions at each step, and one of them has to be fired. This is a disjunctive choice. Symmetrically, we could imgaine an automaton in which several of the possible transitions has to be fired: that is, several executions would be launched from from one single state. Alternating automata extend non-deterministic automata with such "conjunctive choices".

Definition 81 A positive boolean formula over a set AP of atomic propositions is a formula built on the ofllowing grammar:

PBF(AP) φ ::= | ⊥ | p | φ ∨ φ | φ ∧ φ
where p ranges over AP.

That a valuation of AP satisfies such a formula is defined in the obvious way. Given a subset T ⊆ AP, and φ ∈ PBF(AP), we will use the convenient notation T |= φ to mean that v T |= φ where v T (t) = if, and only if, t ∈ T , and v(t) = ⊥ otherwise.

In an alternating automaton, the transition function maps each pair (q, a) to a positive boolean formula on the states (roughly). For instance, if δ(q, a) = q 1 ∧ (q 2 ∨ q 3 ), then one execution must continue in state q 1 , and another one either in state q 2 or in state q 3 . Of course, non-deterministic automata are a special case of alternating automata.

We now formalize this notion for tree automata:

Definition 82 An alternating tree automaton is a tuple A = Q, δ 0 , Σ, δ where

• Q is a finite set of states;

• δ 0 ∈ PBF({♦ , } × Q) is the initial condition;
• Σ is a finite alphabet;

• δ : Q × Σ → PBF({♦ , } × Q) is the transition function.
Definition 83 Let A = Q, Q 0 , Σ, δ be an alternating tree automaton, and T = T, ≤, be a single-root tree. An execution of A on input T is a tree T A = T , , where

• : T → T × Q associates, with each node of T , a corresponding node in the input tree and a state of the automaton. We write T and Q for the first and second component of ;

• the set of roots of T satisfy the initial condition (in a sense that will be made clear later);

• for any state t ∈ T , the set of successors of t satisfy the transition formula δ( Q (t ), ( T (t ))), in a sense that is made clear below.

We now explain what it means for a formula in PBF({♦ , } × Q) to be satisfied. Let t be a node of T A , t = T (t ) be the corresponding node in T , and S be the set of successors of t in T . Let S be the set of successors of t in T A . Then:

• S |= (♦ , q) if, and only if, S contains a node labeled with (u, q) where u ∈ S;

• S |= ( , q) if, and only if, for each u ∈ S, S contains a node labeled with (u, q).

Boolean combinations keep their usual meaning. For the initial condition, the rules are the same, but S is made of only the root of the input tree.

Now, the acceptance condition is a Büchi condition:

Definition 84 An alternating Büchi tree automaton is a tuple A = Q, δ 0 , Σ, δ, F where Q, δ 0 , Σ, δ is an alternating tree automaton and F ⊆ Q is the set of accepting states. An input tree T is accepted if there exists an execution tree T A s.t. any branch runs infinitely often in at least one state of F .

A special subclass of alternating automata will be useful here:

Definition 85 An alternating automaton A = Q, δ 0 , Σ, δ is linear-weak if there exists an order on Q s.t., for any σ ∈ Σ, for any q ∈ Q, for any q that occurs in δ(q, σ), q q.

From CTL to alternating Büchi tree automata

We can now state the important result linking CTL and linear-weak alternating Büchi tree automata:

Theorem 86 ([KVW00, Wil99]) Given a CTL formula φ, one can construct, in linear time, a linear-weak alternating Büchi tree automaton A φ s.t. a singleroot tree T is accepted by A φ if, and only if, it satisfies φ.

Proof. The set of states of the automaton is the set of subformulas of φ that are not conjunctions or disjunctions of subformulas, and their negations. The initial condition is δ 0 = φ: it only requires to begin from states corresponding to φ (note that possibly no state corresponds to φ, if it is a boolean combination of subformulas). The alphabet is 2 AP .

The transition function is defined as follows:

δ(p, σ) = if,
, σ) = (♦ , φ 1 ) δ( AX φ 1 , σ) = ( , φ 1 ) δ( E(φ 1 U φ 2 ), σ) = δ(φ 2 , σ) ∨ (δ(φ 1 , σ) ∧ (♦ , E(φ 1 U φ 2 )) δ( A(φ 1 U φ 2 ), σ) = δ(φ 2 , σ) ∨ (δ(φ 1 , σ) ∧ ( , A(φ 1 U φ 2 )) δ(¬ E(φ 1 U φ 2 ), σ) = δ(¬φ 2 , σ) ∧ (δ(¬φ 1 , σ) ∨ ( , ¬ E(φ 1 U φ 2 )) δ(¬ A(φ 1 U φ 2 ), σ) = δ(¬φ 2 , σ) ∧ (δ(¬φ 1 , σ) ∨ (♦ , ¬ A(φ 1 U φ 2 ))
It is clear enough that this automaton is linear-weak (the order being given by the "subformula" relation). Last, a state is in the accepting set if, and only if, it corresponds to a formula of the form ¬ E(φ 1 U φ 2 ) or ¬ A(φ 1 U φ 2 ).

We now prove that this construction is correct, i.e., that a tree is accepted by this automaton if, and only if, it satisfies φ. To that aim, for each subformula ψ of φ, we define the automaton A ψ to be the same automaton as A φ , but with formula ψ as initial condition. We prove that a tree T = T, ≤, is accepted by A ψ if, and only if, T , 0 |= ψ.

The proof is by induction on the structure of the formula:

• for atomic propositions and negations thereof, this is immediate;

• if ψ = ψ 1 ∨ ψ 2 of ψ = ψ 1 ∧ ψ 2
, the result follows rather easily from the induction hypothesis;

• if ψ = EX ψ 1 : if T , 0 |= EX ψ 1 , then one successor of node 0 satisfies ψ 1 , and, by induction hypothesis, the corresponding subtree is accepted by A ψ1 . It then suffices to add an extra node, labeled with (0, ψ), at the root of an accepting execution tree in order to get an accepting execution tree for A ψ on input T .

Conversely, if T is accepted by A ψ , then an accepting execution tree will start with a node labeled with (0, ψ), having one single son labeled with (t, ψ 1 ), where t is a successor of 0. By induction, the subtree of T rooted at t satisfies ψ 1 , which entails that T , 0 |= EX ψ 1 .

• the arguments are similar for AX ψ 1 ;

• if ψ = E(ψ 1 U ψ 2 ): first assume that T , 0 |= E(ψ 1 U ψ 2 ).
Then there exists a node t s.t. T , t |= ψ 2 , while each intermediate node u i (numbered from 0 to n -1 with u 0 = 0 and t being a successor of u n-1 ) satisfy T , u i |= ψ 1 . By induction, there exist accepting execution trees for the corresponding subtrees in the corresponding automata. From those

Alternating-time temporal logics

Alternating-time temporal logics are special kinds of branching-time logics that are especially powerful in order to reason about "game structures", in which several agents concurrently act upon the system. This approach is very interesting for modeling systems that are embedded in an environment (assumed to be hostile), and that we want to control in order to enforce some properties. We begin with some definitions of all those notions.

Game structures

Definition 88 ([AHK02]) A Concurrent Game Structure ( CGS for short) is a 6-tuple C = A, Q, AP, , c, δ s.t:

• A = {A 1 , ..., A k } is a finite set of agents (or players);

• Q is a finite set of locations;

• AP is a finite set of atomic propositions, resp.;

• : Q → 2 AP is a function labeling each location by the set of atomic propositions that hold for that location;

• c : Q × A → P(Z + ) {∅} defines the (finite) set of possible moves of each agent in each location.

• δ : Q × Z + k → Q,
where k = |A|, is a (partial) function defining the transition table. With each location and each set of moves of the agents, it associates the resulting location.

The intuitive semantics is as follows: in a given state q, each agent A i has several possible moves, represented as integers given by c(q, A i ). Once all the agents have chosen a move, the transition table returns the successor state, where the execution can continue.

Definition 89 Let C = A, Q, AP, , c, δ be a CGS, and q ∈ Q. The set of successors of q, denoted with succ(q), is defined as

succ(q) = {q ∈ Q | ∃a 1 , ..., a k ∈ Z + s.t. q = δ(q, a 1 , ..., a k ) and for all i ≤ k, a i ∈ c(q, A i )}.
Definition 90 Let C = A, Q, AP, , c, δ be a CGS. A computation of C is an infinite sequence ρ = (q i ) i∈Z + s.t. for any i, q i+1 ∈ succ(q i ).

Definition 91 A strategy for player A i ∈ A is a function s i : Q * → Z + that maps each finite prefix of a computation to a move, with the requirement that, for any finite sequence (q 0 , ..., q n ), s i (q 0 , ..., q n ) ∈ c(q n , A i ).

If B ⊆ A is a set of agents (also called a coalition), then a strategy for coalition B is a set of strategies, one for each agent in B. It can be noticed that our definition of a CGS does not allow for non-determinism: one all the payers have chosen their move, there is exactly one possible next state. However, non-determinism can be modeled by adding one extra player, that would, in some sense, "resolve" non-determinism.

Definition 94 Let n ∈ Z + . A (labeled) alternating tree structure is a tuple S = T, ≤, , m s.t.:

• T, ≤, is a tree structure;

• m labels each edge (t, t ) with a set of n-tuples of integers, with the requirement that, for any t ∈ T , there exist sets of integers C 1 , ..., C n such that the set { a 1 , ..., a n | ∃t ∈ T. m(t, t ) = a 1 , ..., a n } is equal to the set { a 1 , ..., a n | ∀i ≤ n. a i ∈ C i }.

Of course, this definition corresponds to computation trees of CGSs, in the following sense: Definition 95 Let C = A, Q, AP, , c, δ be a CGS. Let q ∈ Q, B ⊆ A be a coalition of agents, and s B be a strategy for this coalition. The computation tree of C from q under strategy s B is the alternating tree structure T, ≤, , m where • T is the set of finite words (q 0 , q 1 , ..., q k ) on Q s.t. q 0 = q and, for any two consecutive letters q i and q i+1 , q i+1 ∈ succ((q 0 , ..., q i ), s B );

• ≤ is the lexicographical order;

• (q 0 , ..., q k ) = (q k );

• m(q i , q i+1 ) is the set { a 1 , ..., a n | q i+1 = δ(q i , a 1 , ..., a n ) and a j = s Aj (q 0 , ..., q i ) if A j ∈ B}.

Exercice 4.39.

Prove that the computation tree of a CGS is indeed an alternating tree structure.

Of course, CTL can be evaluated on such a computation tree, but it can also be enriched in order to take the extra labeling of the edges into account. This yields the logic ATL (for Alternating-time Temporal Logic): Definition 96 Given a set M 1 , ..., M n of first-order definable modalities, the syntax of the alternating-time temporal logic A(M 1 , ..., M n ) is given by: where p ranges over AP and B ranges over the subsets of A. The logic ATL is then defined as A(X , U ) .

The semantics is as follows:

Definition 97 Let S = T, ≤, , m be an alternating tree structure, t ∈ T , (t 0 , ..., t n-1 ) be the (ordered) set of predecessors of t, and φ l be a path formula of ATL. We define the semantics of ATL as an extension of the semantics of CTL * (see Definition 67) with the following two rules: Quantifiers B and B quantify over strategies: formula B φ l is read "there is a strategy for coalition B to enforce φ l ", while B φ l is dual, and can be read "coalition B has no strategy to prevent φ l from happening".

It should be remarked that ATL subsumes CTL, because both existential and universal path quantifiers can be expressed in terms of • :

Eφ l ≡ A φ l Aφ l ≡ ∅ φ l
Remark. The original definition of ATL, which appeared in [AHK97, AHK02],

is not exactly the one described above: it was a "modal" definition, where formulas are built from atomic propositions, boolean combinators, and the following three kinds of modalities: B X, B U and B G. However, this definition is strictly less expressive than the above one [START_REF] Laroussinie | Expressiveness and complexity of ATL[END_REF].

Exercice 4.40.

The "weak until" modality is a relaxed version of the "until" modality, where the eventuality might not occur. It is defined as

φ W ψ def ≡ φ U ψ ∨ G φ.

ATL model-checking

This section is devoted to proving the following result:

Theorem 98 If the number of players is fixed, then ATL model-checking is PTIME-complete.

Remark. It is important to insist here on the fact that the number of players must be fixed in order to achieve this complexity. The problem comes from the fact that, if each of the n players have m possible moves, the transition table given by δ has size m n , but could be encoded is a more succinct way than just the whole explicit table. The above complexity result still holds if the number of players is a parameter of the problem provided that the transition table is given explicitely.

Proof. Hardness in PTIME follows from that of CTL, and we only have to develop a PTIME algorithm in order to prove our statement. The algorithm is similar to that of CTL: it consists in recursively label the states of the structures with the subformulas that hold true in those states.

Let C = A, Q, AP, , c, δ be a CGS with a fixed number of players, and φ ∈ ATL. For each subformula ψ of φ, we label the states of C according to the following rules (omitting the trivial cases of atomic propositions and boolean combinators, for which the algorithm is similar to that of CTL):

• if ψ = B X ψ 1 : assuming the labeling algorithm has already been applied for ψ 1 , we label a state q with ψ if, and only if, there exists a set of moves a i1 , ..., a i |B| , one for each player in B, s.t.

{q ∈ Q | ∃a j1 , ..., a j |A|-|B| . q = δ(q, a 1 , ..., a n )} ⊆ {q ∈ Q | q is labeled with ψ 1 }.

This can easily be proved in linear-time by reading the transition table.

• if ψ = B X φ 1 : we label with ψ those states from which coalition B cannot avoid going in a location labeled with ψ 1 . Formally, we label a state q if, for any set of moves a i1 , ..., a i |B| , we have {q ∈ Q | ∃a j1 , ..., a j |A|-|B| . q = δ(q, a 1 , ..., a n )}∩ {q ∈ Q | q is labeled with ψ 1 } = ∅.

• if ψ = B (ψ 1 U ψ 2 ): we recursively label the states of the structure: at the first stage, the states that have been labeled with ψ 2 are labeled with ψ. We then apply the following procedure until a fixpoint is reached: if a state q is labeled with ψ 1 , and if there is a set of moves a i1 , ..., a i |B| , one for each player in B, s.t.

{q ∈ Q | ∃a j1 , ..., a j |A|-|B| . q = δ(q, a 1 , ..., a n )} ⊆ {q ∈ Q | q is labeled with ψ} then we label q with ψ.

• last, if ψ = B (ψ 1 U ψ 2 ), then we again begin with labeling with ψ all the states that are labeled with ψ 2 , and then recursively label with ψ each state that is labeled with ψ 1 and satisfies the following condition:

{q ∈ Q | ∃a j1 , ..., a j |A|-|B| . q = δ(q, a 1 , ..., a n )}∩ {q ∈ Q | q is labeled with ψ} = ∅.

The procedure stops when a fixpoint is reached.

That the algorithm terminates in polynomial time is rather obvious: it runs in time O(|δ| • |φ|). That it is correct can be proved following the same lines as for the algorithm for CTL.

Exercice 4.41.

Prove that the algorithm is correct.

Remark. The algorithm above only computes the set of states in which formula φ holds, but, for each subformula of the form B φ and for each state, a winning strategy is easily obtained from the sets of moves that witness the fact that we label this state. This entails in particular that if there exists a strategy for coalition B to enforce φ, with φ a path formula in ATL, then there exists a memoryless strategy, i.e., a strategy that only depends on the current state, and not on the whole history of the computation.

Exercice 4.42.

Prove that memoryless strategies still exist if we extend ATL with the modality ∞ F (with the semantics derived from that of CTL * ). Prove that ATL + , where we allow boolean combinations of modalities in the scope of strategy quantifiers, can be translated in ATL, and thus also benefits from memoryless strategies.

Figure 2 . 1 :

 21 Figure 2.1: Principles of model-checking

Definition 20

 20 Two linear-time temporal logic formulas φ and ψ are equivalent over a set of pointed structures M when ∀m ∈ M. (m |= φ ⇔ m |= ψ).

Figure 3 . 1 :

 31 Figure 3.1: An example of a Büchi automaton

  Figure 3.2: The Büchi automaton corresponding to formula a U (b ∧ X -1 b).

(3. 1 )

 1 This formula can easily be expressed in LTL, e.g. by enumerating the set of valuations for p 1 to p n : a0,a1,...,an∈{ ,⊥}(F ( i∈[0,n]

  s |= b φ b and S, s |= b ψ b S, s |= b Eφ l ⇔ ∃b ∈ Br(s). S, b, s |= l φ l S, s |= b Aφ l ⇔ ∀b ∈ Br(s). S, b, s |= l φ l S, b, s |= l φ b ⇔ S, s |= b φ b S, b, s |= l ¬φ l ⇔ S, b, s |= l φ l S, b, s |= l φ l ∨ ψ l ⇔ S, b, s |= l φ l or S, b, s |= l ψ l S, b, s |= l φ l ∧ ψ l ⇔ S, b, s |= l φ l and S, b, s

Exercice 4. 25 .

 25 Let A = W A , R A , l A and B = W B , R B , l B be two Kripke structures. A bisimulation on A and B is a relation B ⊆ W A × W B s.t.: • for any (a, b) ∈ B, l A (a) = l B (b); • for any (a, b) ∈ B, for any (a, a ) ∈ R A , there exists (b, b ) ∈ R B s.t. (a , b ) ∈ B; • symmetrically, for any (a, b) ∈ B, for any (b, b ) ∈ R B , there exists (a, a ) ∈ R B s.t. (a , b ) ∈ B; Two states a ∈ A and b ∈ B are bisimilar if there exists a bisimilation B s.t. (a, b) ∈ B. As a classical counter-example, the initial states of the Kripke structures depicted on Figure 4.1 are not bisimilar. Find a CTL formula that holds on only one of those Kripke structures.

Figure 4 . 1 :

 41 Figure 4.1: Two Kripke structures that are not bisimilar

Figure 4 . 2 :

 42 Figure 4.2: Two families of structures that CTL cannot distinguish.

Figure 4

 4 Figure 4.4: The Kripke structure used for encoding SNSAT

Figure 4 .

 4 Figure 4.5 displays an example of an input tree, and an execution tree. State q a is

  Figure 4.6: A simple CGS

A

  (M 1 , ..., M n ) φ b ::= p | ¬φ b | φ b ∨ φ b | φ b ∧ φ b | B φ l | B φ l φ l ::= M 1 (φ b , ..., φ b ) | • • • | M n (φ b , ..., φ b )

S

  , t |= b B φ l ⇔ ∃ strategy s B . ∀b ∈ Br(t). if b ∈ Out((t 0 , ..., t n-1 ), s B ), then S, b, t |= l φ l S, t |= b B φ l ⇔ ∀ strategy s B .∃b ∈ Br(t). b ∈ Out((t 0 , ..., t n-1 ), s B ) and S, b, t |= l φ l

  Prove the following equivalences (over discrete time):Eφ W ψ ≡ Eφ U ψ ∨ EG φ φ W ψ ≡ ¬(¬ψ U (¬φ ∧ ¬ψ)) Eφ W ψ ≡ ¬ A(¬ψ U (¬φ ∧ ¬ψ))Give counter-examples proving that the following tentative formulas do not express B W:B φ U ψ ∨ A G φ ≡ B φ W ψ ¬ A B (¬ψ U (¬φ ∧ ¬ψ)) ≡ B φ W ψProve that those formulas are equivalent on turn-based CGSs.

Table 2 .

 2 1: Truth table of the three basic Boolean operators

  one state of the Büchi automaton is stored in space O(|φ|), one state of the Kripke structure only requires space O(log(|K|)). This algorithm thus performs in space O(|φ|

2

• log(|K|)), and time O(|φ| 2 × |K| × 2 2|φ| ).

Exercice 3.21.

Explain the above space-and time bounds of the algorithm for LTL+Past model-checking.

  and only if, x r |= ψ k ; (2) if k ≥ 2r, then v I (x r ) = ⊥ if, and only if, x r |= ψ k .

trees, we build a new one as follows: from the root of the execution tree for u 0 , add an extra edge to the root of the execution tree of A ψ1 for u 1 ; from this node, add an extra edge to the root of the execution tree for u 2 , and so on. Last, from the root of the execution tree for u n-1 , add an edge to to execution tree of A ψ2 on the subtree rooted at t. We then set the labeling as follows: nodes labeled with (u i , ψ 1 ) are now labeled with (u i , ψ). It is then easy to check that this is an execution tree of A ψ on input tree T , and that it is accepting.

Conversely, assume that T is accepted by A ψ , and consider an accepting execution tree. There can't be an infinite branch whose nodes are labeled with ψ as second item, since this would contradict acceptance. Thus, there exists a finite sequence of nodes t 0 , ..., t n , with t 0 = 0 and t i+1 being a successor of t i , and labeled with (t i , ψ) where t i+1 is a successor of t i in T . Since the transition condition must be fulfilled, it must be the case at each t i , i < n, has successors satisfying δ(ψ 1 , (t i )). From each corresponding subtrees, we can easily build execution trees showing that the subtree of T rooted at t i is accepted by A ψ1 and, by induction hypothesis, that T , t i |= ψ 1 . Similarly, t n has a set of successors satisfying δ(ψ 2 , (t n )), from which we can prove that T , t n |= ψ 2 . This entails that T , 0 |= ψ.

• the arguments for the other cases are very similar, and left to the intrepid reader.

Exercice 4.37.

Given an alternating Büchi tree automaton A, prove that there exists a Büchi tree automaton A that accepts exactly the same set of trees, and has size at most exponential in the size of A.

Application to verification

Since checking the emptiness of the language accepted by an alternating Büchi (tree) automaton is in EXPTIME, we get the following result:

By encoding the behavior of a linear-space alternating Turing machine (see [START_REF] Papadimitriou | Computational Complexity[END_REF]), prove that CTL satisfiability is EXPTIME-hard.

Remark. Note that the automaton can also be used for model-checking, and yields a polynomial-time algorithm [START_REF] Kupferman | An automatatheoretic approach to branching-time model-checking[END_REF].

Remark. Infinite words are a special case of infinite trees, and CTL, when interpreted on infinite words, is obviously equivalent to LTL. It follows that the construction above can be adapted to the linear-time case. A direct construction is given in [START_REF] Vardi | An automata-theoretic approach to linear temporal logic[END_REF]. In this case, the converse translation is also possible: linearweak alternating Büchi automata are exactly as expressive as LTL.

An important class of stratgies consists in those strategies that only depend on the current state, and not on the whole history:

Definition 92 A strategy s is memoryless is, for any two finite sequences (q 0 , ..., q n ) and (q 0 , ..., q m ), if q n = q m , then s(q 0 , ..., q n ) = s(q 0 , ..., s m ).

We should now define what it means to play according to a strategy: ,c, δ be a CGS, B ⊆ A be a coalition of agents, s B be a strategy for this coalition, and (q 0 , ..., q n ) be a finite prefix of a computation. We write succ((q 0 , ..., q n ), s b ) for the set of possible successors under the strategy s B , defined formally as succ((q 0 , ..., q n ), s B ) = {q ∈ succ(q n ) | ∃a 1 , ..., a k ∈ Z + s.t. q = δ(q, a 1 , ..., a k ) and for all i ≤ k, a i ∈ c(q, A i ) and for all i ≤ k. (A i ∈ B ⇒ a i = s Ai (q 0 , ..., q n ))}.

A computation ρ = (q i ) i∈Z + is an outcome of the strategy s B with history (q 0 , ..., q n ) if, for any i, we have q i+1 ∈ succ((q 0 , ..., q n , q 0 , ..., q i ), s B ).

We write Out((q 0 , ..., q n ), s B ) for the set of outcomes of s B with history (q 0 , ..., q n ).

Example. We consider a very simple example, with only two players, depicted on Figure 4.6. In such a representation, edges are labeled with tuples, with the following meaning: an edge (q, q ) is labeled with a 1 , a 2 when δ(q, a 1 , a 2 ) = q . That is, this transition corresponds to move a 1 of player A 1 and to move a 2 of player A 2 .

In the example of Figure 4.6, player A 1 has only one possible move in state p, and two moves in q. Conversely, A 2 has only one move from q, and two from p. This is an example of a turn-based CGS, where, in each state, at most one player has several moves. Example. Consider the example of Figure 4.7. This example is not turn-based anymore, since both players have two possible moves in the topmost state. From that state, it is clear enough that player A 1 has no strategy to be sure to go to state p: whichever move she plays, the other player simply has to play the opposite in order to avoid state p. Conversely, player A 2 has no strategy to avoid state p: whatever she plays, the opponent simply has to play the same move in order to end up in state p.

This property is called non-determinedness. It must be mentionned that many cases of asynchronous games are determined: if a player has no strategy to achieve some goal, then the opponent has a strategy to avoid that goal. Synchronous games do not have this property.

Prove that if we combine both extensions (modality ∞ F and boolean combinations of modalities), we lose the existence of a memoryless strategy.

Exercice 4.43.

It should be noticed that we did not specify the way the transition table should be represented. The naive representation is as a (huge) table of size O(|Q| × M |A| ), where M is the maximal number of possible choices af any agent in any location. Still, there are more succinct representations, e.g. involving boolean formulas on the choices of the agents. Prove that, under this encoding, ATL model-checking is NP-hard.

Index