Stéphane Demri
email: demri@lsv.ens-cachan.fr

Gastin Paul
email: gastin@lsv.ens-cachan.fr

Lsv

Specification and Verification using Temporal Logics *

Keywords: temporal logic, model-checking, Büchi automaton, temporal operator, context-free language

This chapter illustrates two aspects of automata theory related to lineartime temporal logic LTL used for the verification of computer systems. First, we present a translation from LTL formulae to Büchi automata. The aim is to design an elementary translation which is reasonably efficient and produces small automata so that it can be easily taught and used by hand on real examples. Our translation is in the spirit of the classical tableau constructions but is optimized in several ways. Secondly, we recall how temporal operators can be defined from regular languages and we explain why adding even a single operator definable by a context-free language can lead to undecidability.

Introduction

Temporal logics as specification languages. Temporal logics (TL) are modal logics [START_REF] Blackburn | Modal Logic[END_REF] designed to specify temporal relations between events occurring over time. They first appear as a branch of logic dedicated to reasoning about time, see e.g. [START_REF] Rescher | Temporal Logic[END_REF]. The introduction of TL for reasoning about program behaviours is due to [START_REF] Pnueli | The temporal logic of programs[END_REF]. Among the desirable properties of formal specification languages, the temporal logics have an underlying flow of time in its models, define mathematically the correctness of computer systems, express properties without ambiguity and are useful for carrying out formal proofs. Moreover, compared with the mathematical formulae, temporal logic notation is often clearer and simpler. This is a popular formalism to express properties for various types of systems (concurrent programs, operating systems, network communication protocols, programs with pointers, etc.). An early success of the use of TL has been the verification of finite-state programs with TL specifications, see e.g. [START_REF] Queille | Specification and verification of concurrent systems in CESAR[END_REF][START_REF] Clarke | Automatic verification of finitestate concurrent systems using temporal logic specifications: A practical approach[END_REF].

Automata-based approach. Model-checking [START_REF] Queille | Specification and verification of concurrent systems in CESAR[END_REF][START_REF] Clarke | Model Checking[END_REF] is one of the most used methods for checking temporal properties of computer systems. However, there are different ways to develop theory of model-checking and one of them is dedicated to the construction of automata from temporal logic formulae. In that way, an instance of a model-checking problem is reduced to a nonemptiness check of some automaton, typically recognizing infinite words [START_REF] Thomas | Automata on infinite objects[END_REF]. This refines the automata-based approach developed by R. Büchi for the monadic second-order theory of N, < in [START_REF] Büchi | On a decision method in restricted second-order arithmetic[END_REF] (for which nonelementary bounds are obtained if the translation is applied directly). This approach has been successfully developed in [START_REF] Vardi | Reasoning about infinite computations[END_REF] for linear-time temporal logics and recent developements for branching-time temporal logics with best complexity upper bounds can be found in [START_REF] Harel | On the complexity of verifying concurrent transition systems[END_REF], see also a similar approach for description logics, program logics or modal logics [START_REF] Blackburn | Modal Logic[END_REF].

On the difficulty of presenting simple automata The translations from temporal formulae into automata providing best complexity upper bounds, often require on-the-fly algorithms and are not always extremely intuitive. For instance, on-thefly algorithms for turning specifications into automata and doing the emptiness check can be found in [START_REF] Courcoubetis | Memory efficient algorithms for the verification of temporal properties[END_REF][START_REF] Gerth | Simple on-the-fly automatic verification of linear temporal logic[END_REF][START_REF] Daniele | Improved automata generation for linear temporal logic[END_REF]. In order to explain the principle of such translations, it is essential to be able to show how to build simple automata for simple formulae. For instance, the temporal formula X n p stating that the propositional variable p holds at the n-th next step, may lead to an exponential-size automaton in n when maximally consistent sets of formulae are states of the automata even though X n p has a linear-size automaton. This gain in simplification is of course crucial for practical purposes but it is also important to have simple constructions that can be easily taught. That is why we share the pedagogical motivations from [START_REF] Couvreur | On-the-fly verification of linear temporal logic[END_REF] and we believe that it is essential to be able to present automata constructions that produce simple automata from simple formulae.

Our contribution. This chapter presents two aspects of automata theory for LTL model-checking and it can be viewed as a follow-up to [START_REF] Vardi | Reasoning about infinite computations[END_REF][START_REF] Wolper | The tableau method for temporal logic: An overview[END_REF][START_REF] Wolper | Constructing automata from temporal logic formulas: A tutorial[END_REF]. First, we present a translation from LTL formulae to generalized Büchi automata such that simple formulae produce simple automata. We believe this translation can be easily taught and used by hand on real examples. So, Section 1.2 recalls standard definitions about the temporal logics LTL and CTL * whereas Section 1.3 provides the core of the translation in a self-contained manner. A nice feature of the construction is the use of target transition-based Büchi automata (BA) which allows us to obtain concise automata: the acceptance condition is a conjunction of constraints stating that some transitions are repeated infinitely often. This type of acceptance condition has already been advocated in [START_REF] Gerth | Simple on-the-fly automatic verification of linear temporal logic[END_REF][START_REF] Couvreur | On-the-fly verification of linear temporal logic[END_REF][START_REF] Gastin | Fast LTL to Büchi automata translation[END_REF][START_REF] Giannakopoulou | From states to transitions: improving translation of LTL formulae to Büchi automata[END_REF][START_REF] Couvreur | On-the-fly emptiness checks for generalized Büchi automata[END_REF][START_REF] Tauriainen | Automata and Linear Temporal Logic: Translations with Transitionbased Acceptance[END_REF]. Secondly, we consider richer temporal logics by adding either path quantifiers (Section 1.4.1) or language-based temporal operators (regular or context-free languages) following the approach introduced in [START_REF] Wolper | Temporal logic can be more expressive[END_REF]. We recall the main expressive power and complex-ity issues related to Extended Temporal Logic ETL [START_REF] Wolper | Temporal logic can be more expressive[END_REF] (Section 1.4.2). Finally, we show that model-checking for propositional calculus augmented with a simple context-free language recognized by a visibly pushdown automaton (VPA) [START_REF] Alur | Visibly pushdown languages[END_REF] is highly undecidable (Section 1.4). It is worth observing that Propositional Dynamic Logic with programs [START_REF] Harel | Dynamic Logic[END_REF] (PDL) augmented with visibly pushdown automata has been recently shown decidable [START_REF] Löding | Propositional dynamic logic with recursive programs[END_REF] and the class of VPA shares very nice features (closure under Boolean operations for instance [START_REF] Alur | Visibly pushdown languages[END_REF]).

Temporal logics 1.2.1. Modalities about executions

The languages of TL contain precisely modalities having a temporal interpretation. A modality is usually defined as a syntactic object (term) that modifies the relationships between a predicate and a subject. For example, in the sentence "Tomorrow, it will rain", the term "Tomorrow" is a temporal modality. TL makes use of different types of modalities and we recall below some of them interpreted over runs (a.k.a. executions or ω-sequences). The temporal modalities (a.k.a. temporal combinators) allow one to speak about the sequencing of states along an execution, rather than about the states taken individually. The simplest temporal combinators are X ("neXt"), F ("sometimes") and G ("always"). Below, we shall freely use the Boolean operators ¬ (negation), ∨ (disjunction), ∧ (conjunction) and → (material implication).

• Whereas ϕ states a property of the current state, X ϕ states that the next state (X for "neXt") satisfies ϕ. For example, ϕ ∨ X ϕ states that ϕ is satisfied now or in the next state.

X p p X p: next-time p

• F p announces that a future state (F for "Future") satisfies ϕ without specifying which state, and G ϕ that all the future states satisfy ϕ. These two combinators can be read informally as "ϕ will hold some day" and "ϕ will always be". Foundations of the modal approach to temporal logic can be found in [START_REF] Prior | Past, Present and Future[END_REF] in which are introduced the combinators F and G.

F p p F p: sometimes p

Duality The operator G is the dual of F: whatever the formula ϕ may be, if ϕ is always satisfied, then it is not true that ¬ϕ will some day be satisfied, and conversely. Hence G ϕ and ¬ F ¬ϕ are equivalent.

G p, p p p p p G p: always p By way of example, the expression alert → F halt means that if we (currently) are in a state of alert, then we will (later) be in a halt state.

Past-time operators Likewise, the past operators F -1 ("sometime in the past") and G -1 ("always in the past") are also introduced in [START_REF] Prior | Past, Present and Future[END_REF].

p F -1 p
F -1 p: sometime in the past p

• The U combinator (for "Until") is richer and more complicated than the combinator F. ϕ 1 Uϕ 2 states that ϕ 1 is true until ϕ 2 is true. More precisely: ϕ 2 will be true some day, and ϕ 1 will hold in the meantime.

p U q, p p p p q p U q: p until q

The example G(alert → F halt) can be refined with the statement that "starting from a state of alert, the alarm remains activated until the halt state is eventually reached":

G(alert → (alarm U halt)).

Sometime operator

The F combinator is a special case of U: F ϕ and true U ϕ are equivalent.

Weak until There exists also a "weak until", denoted W. The statement ϕ 1 W ϕ 2 still expresses "ϕ 1 U ϕ 2 ", but without the inevitable occurrence of ϕ 2 and if ϕ 2 never occurs, then ϕ 1 remains true forever. So,

ϕ 1 W ϕ 2 is equivalent to G ϕ 1 ∨ (ϕ 1 U ϕ 2 ).
Release operator In the sequel, we shall also use the so-called "release" operator R which is the dual of the until operator U. The formula ϕ 1 R ϕ 2 states that the truth of ϕ 1 releases the constraint on the satisfaction of ϕ 2 , more precisely, either ϕ 1 will be true some day and ϕ 2 must hold between the current state and that day, or ϕ 2 must be true in all future states.

We provide below other examples of properties that can be expressed thanks to these temporal modalities.

(safety) G(halt → F -1 alert), (liveness) G(p → F q), (total correctness) (init ∧ p) → F(end ∧ q), (strong fairness) G F enabled → G F executed.

Linear-time temporal logic LTL

As far as we know, linear-time temporal logic LTL in the form presented herein has been first considered in [START_REF] Gabbay | On the temporal analysis of fairness[END_REF] based on the early works [START_REF] Pnueli | The temporal logic of programs[END_REF][START_REF] Kamp | Tense Logic and the Theory of Linear Order[END_REF]. Indeed, the strict until operator in [START_REF] Kamp | Tense Logic and the Theory of Linear Order[END_REF] can express the temporal operators from LTL (without past-time operators) and in [START_REF] Pnueli | The temporal logic of programs[END_REF] temporal logics are advocated for the formal verification of programs. However, the version of LTL with explicitly the next-time and until operators first appeared in [START_REF] Gabbay | On the temporal analysis of fairness[END_REF]. Actually, the next-time operator has been introduced in [START_REF] Manna | The modal logic of programs[END_REF] in order to define LTL restricted to the next-time and sometime operators (see also a similar language in [START_REF] Pnueli | The temporal semantics of concurrent programs[END_REF]). Nowadays, LTL is one of the most used logical formalisms to specify the behaviours of computer systems in view of formal verification. It has been also the basis for numerous specification languages such as PSL [START_REF] Eisner | A Practical Introduction to PSL[END_REF]. Moreover, it is used as a specification language in tools such as SPIN [START_REF] Holzmann | The model checker SPIN[END_REF] and SMV [START_REF] Mcmillan | Symbolic Model Checking[END_REF]. LTL formulae are built from the following abstract grammar:

ϕ ::= propositional calculus ⊥ | ⊤ | p | ¬ϕ | ϕ ∧ ψ | ϕ ∨ ψ | temporal extension X ϕ | F ϕ | G ϕ | ϕ U ψ | ϕ R ψ
where p ranges over a countably infinite set AP of propositional variables. Elements of AP are obtained by abstracting properties, for instance p may mean "x = 0". Given a set of temporal operators O ⊆ {X, F, G, U, R}, we write LTL(O) to denote the restriction of LTL to formulae with temporal connectives from O. We write sub(ϕ) to denote the set of subformulae of the formula ϕ and |ϕ| to denote the size of the formula ϕ viewed as a string of characters. LTL models are program runs, i.e., executions viewed as ω-sequences. The reason why the models are infinite objects (instead of finite sequences to encode finite runs) is mainly due to the possibility to specify limit behaviours such as fair behaviours. So, a structure (or model) for LTL is an infinite sequence u : N → 2 AP , i.e., an infinite word of (2 AP ) ω . Here are the five first states of an LTL model:

{p} {q} {} {p, q, r} {q}
Given a structure u, a position i ∈ N and a formula ϕ, we define inductively the satisfaction relation |= as follows:

• always u, i |= ⊤ and never u, i |=⊥, • u, i |= p def ⇔ p ∈ u(i), for every p ∈ AP, • u, i |= ¬ϕ def ⇔ u, i |= ϕ, • u, i |= ϕ 1 ∧ ϕ 2 def ⇔ u, i |= ϕ 1 and u, i |= ϕ 2 , • u, i |= ϕ 1 ∨ ϕ 2 def ⇔ u, i |= ϕ 1 or u, i |= ϕ 2 , • u, i |= X ϕ def ⇔ u, i + 1 |= ϕ, • u, i |= F ϕ def ⇔ there is j ≥ i such that u, j |= ϕ, • u, i |= G ϕ def ⇔ for all j ≥ i, we have u, j |= ϕ, • u, i |= ϕ 1 U ϕ 2 def ⇔ there is j ≥ i such that u, j |= ϕ 2 and u, k |= ϕ 1 for all i ≤ k < j, • u, i |= ϕ 1 R ϕ 2 def ⇔ u, j |= ϕ 2 for all j ≥ i, or there is j ≥ i such that u, j |= ϕ 1 and u, k |= ϕ 2 for all i ≤ k ≤ j.
We say that two formulae ϕ and ψ are equivalent whenever for all models u and positions i, we have u, i |= ϕ if and only if u, i |= ψ. In that case, we write ϕ ≡ ψ. Roughly speaking, ϕ and ψ state equivalent properties over the class of ω-sequences indexed by propositional valuations. For instance, F ϕ is equivalent to ⊤ U ϕ and G ϕ is equivalent to ⊥ R ϕ. Consequently, it is clear that our set of connectives is not minimal in terms of expressive power but it provides handy notations. Moreover, we shall use the following abbreviations:

ϕ 1 → ϕ 2 for ¬ϕ 1 ∨ ϕ 2 and F ∞ ϕ for G F ϕ ("ϕ holds infinitely often"). Finally, one can check that G is the dual of F (since G p ≡ ¬ F ¬p) and R is the dual of U (since ϕ 1 R ϕ 2 ≡ ¬(¬ϕ 1 U ¬ϕ 2 )).
We write u |= ϕ instead of u, 0 |= ϕ. The standard automata-based approach for LTL, see e.g. [START_REF] Vardi | Reasoning about infinite computations[END_REF], considers the models for a formula ϕ as a language L(ϕ) over the alphabet 2 AP(ϕ) where AP(ϕ) denotes the set of propositional variables occurring in ϕ (these are the only relevant ones for the satisfaction of ϕ):

L(ϕ) = {u ∈ (2 AP(ϕ) ) ω | u |= ϕ}.
We say that ϕ is satisfiable if L(ϕ) is non-empty. Similarly, ϕ is valid if L(¬ϕ) is empty. The satisfiability problem for LTL, denoted by SAT(LTL), is defined as follows:

input: an LTL formula ϕ, output: 1 if u |= ϕ for some infinite word u ∈ (2 AP(ϕ) ) ω ; 0 otherwise. The validity problem VAL(LTL) is defined similarly. In order to be precise, it is worth observing that herein we consider initial satisfiability since the formula ϕ holds at the position 0. Since LTL (and the other temporal logics considered in this chapter) does not deal with past-time operators, initial satisfiability is equivalent to satisfiability (satisfaction at some position, not necessarily 0).

Let us now consider the model-checking problem. A Kripke structure M = W, R, λ is a triple such that

• W is a non-empty set of states, • R is a binary relation on W (accessibility relation, one-step relation), • λ is a labeling λ : W → 2 AP .
M is simply a directed graph for which each node is labeled by a propositional interpretation (labeled transition system). A path in M is a sequence σ = s 0 s 1 s 2 • • • (finite or infinite) such that (s i , s i+1 ) ∈ R for every i ≥ 0. We write Paths(M, s 0 ) to denote the set of infinite paths of M starting at state s 0 . We also write λPaths(M, s 0 ) to denote the set of labels of infinite paths starting at s 0 :

λPaths(M, s 0 ) = {λ(s 0 )λ(s 1 )λ(s 2 ) • • • | s 0 s 1 s 2 • • • ∈ Paths(M, s 0 )}.
The (universal ) model-checking problem for LTL, denoted by MC ∀ (LTL), is defined as follows:

input: an LTL formula ϕ, a finite and total † Kripke structure M and s 0 ∈ W , output: 1 if u |= ϕ for all u ∈ λPaths(M, s 0 ) (written M, s 0 |= ∀ ϕ); 0 otherwise. Without any loss of generality, in the above statement we can assume that the codomain of the labeling λ is restricted to AP(ϕ). The size of W, R, λ is defined by card(W ) + card(R) + Σ w∈W card(λ(w)). It is easy to check that M, s 0 |= ∀ ϕ if and only if λPaths(M, s 0 ) ∩ L(¬ϕ) = ∅.

There is a dual definition, called existential model checking and denoted by MC ∃ (LTL), where an existential quantification on paths is considered. We write

M, s 0 |= ∃ ϕ if u |= ϕ for some u ∈ λPaths(M, s 0 ). Similarly, M, s 0 |= ∃ ϕ if and only if λPaths(M, s 0 ) ∩ L(ϕ) = ∅.
We present below a Kripke structure in which ON and OFF are propositional variables and we identify them with states where they hold respectively.

ON OFF

We leave to the reader to check that the properties below hold:

• M, ON |= ∃ F ∞ ON ∧ F ∞ OFF, • M, ON |= ∃ ¬ F ∞ OFF, • M, ON |= ∃ G(ON → X X OFF).

Branching-time temporal logic CTL *

The language introduced so far can only state properties along one execution. It is also often desirable to express the branching aspect of the behavior: many futures are possible starting from a given state. For instance, consider the property ϕ which is informally defined as: "whenever we are in a state where p holds, it is possible to reach a state where q holds". This natural property cannot be expressed in LTL. Indeed, with the models M 1 and M 2 of Figure 1.1, we have λPaths(M 1 ) = λPaths(M 2 ). Hence M 1 and M 2 satisfy the same LTL formulae. But indeed, M 1 satisfies ϕ whereas M 2 does not. The logic CTL * introduces special purpose quantifiers, A (compare with ∀ in first-order logic) and E (compare with ∃ in first-order logic), which allow to quantify over the set of executions. These are called path quantifiers. The expression A ϕ M 1 : p, q p q M 2 : p, q p p q states that all executions out of the current state satisfy property ϕ. Dually, E ϕ states that from the current state, there exists an execution satisfying ϕ. Our "natural" property above can be written A G(p → E F q). It is worth observing that A and E quantify over paths whereas G and F quantify over positions along a path.

The expression E F ϕ states that it is possible (by following a suitable execution) to have ϕ some day, which is illustrated below.

p E F p

The expression A F ϕ states that we will necessarily have ϕ some day, regardless of the chosen execution (see below).

p p p p p

A F p

The expression A G ϕ states that ϕ holds in all future states including now (see below). The expression E G ϕ states that there is an execution on which ϕ always holds (see below). p p p E G p, p "Branching-time logics" refers to logics that have the ability to freely quantify over paths. Standard examples of branching-time temporal logics include Computation Tree Logic CTL [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching time temporal logic[END_REF], CTL * [START_REF] Emerson | Sometimes" and "Not Never" revisited: on branching versus linear time temporal logic[END_REF] and the modal µ-calculus. We define below the logic CTL * (that is more expressive than both LTL and CTL) for which the model-checking problem can be solved easily by using a subroutine solving the model-checking problem for LTL. Hence, even though the object of this chapter is not especially dedicated to branching-time logics, we explain how CTL * modelchecking can be dealt with. CTL * formulae are built from the following abstract grammar:

ϕ ::= p | ¬ϕ | ϕ 1 ∧ ϕ 2 | E ϕ | A ϕ | X ϕ | ϕ 1 U ϕ 2
where p ranges over AP. CTL * models are total Kripke models. Let σ = s 0 s 1 . . . be an infinite path in M, i ≥ 0 and ϕ be a formula. The satisfaction relation σ, i |= ϕ is defined inductively as follows (we omit the clauses for Boolean connectives):

• σ, i |= p def ⇔ p ∈ λ(s i ), • σ, i |= X ϕ def ⇔ σ, i + 1 |= ϕ, • σ, i |= ϕ 1 U ϕ 2 def ⇔ there is j ≥ i such that σ, j |= ϕ 2 and σ, k |= ϕ 1 for all i ≤ k < j, • σ, i |= E ϕ def ⇔ there is an infinite path σ ′ = s ′ 0 s ′ 1 . . . such that s ′ 0 = s i and σ ′ , 0 |= ϕ, • σ, i |= A ϕ def ⇔ for every infinite path σ ′ = s ′ 0 s ′ 1 . . . such that s ′ 0 = s i , we have σ ′ , 0 |= ϕ.
The model-checking problem for CTL * , denoted by MC ∀ (CTL * ), is defined as follows:

input: a CTL * formula, a finite and total Kripke model M = W, R, λ and s ∈ W ; output: 1 if σ, 0 |= ϕ for all infinite paths σ ∈ Paths(M, s) starting from s; 0 otherwise.

Complexity issues

Let us recall a few complexity results.

Theorem 1.1. [START_REF] Emerson | Sometimes" and "Not Never" revisited: on branching versus linear time temporal logic[END_REF][START_REF] Sistla | The complexity of propositional linear temporal logic[END_REF][START_REF] Demri | The complexity of propositional linear temporal logics in simple cases[END_REF][START_REF] Schnoebelen | The complexity of temporal logic model checking[END_REF] The following problems are PSpace-complete.

(i) SAT(LTL), VAL(LTL), MC ∃ (LTL) and MC ∀ (LTL).

(ii) SAT(LTL(X, F)), VAL(LTL(X, F)), MC ∃ (LTL(X, F)) and MC ∀ (LTL(X, F)).

(iii) SAT(LTL(U)), VAL(LTL(U)), MC ∃ (LTL(U)) and MC ∀ (LTL(U)).

(iv) The restriction of the above problems to a unique propositional variable.

(v) MC(CTL * ).

On the other hand, the problems SAT(LTL(F)), MC ∃ (LTL(F)) are NP-complete and VAL(LTL(F)), MC ∀ (LTL(F)) are coNP-complete.

The treatment in Section 1.3 will establish that SAT(LTL), VAL(LTL), MC ∀ (LTL) and MC ∃ (LTL) are in PSpace.

The Computation Tree Logic CTL [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching time temporal logic[END_REF] is a strict fragment of CTL * for which model-checking can be solved in polynomial-time. We briefly recall that CTL formulae are defined by the grammar below:

ϕ ::= p | ¬ϕ | ϕ 1 ∧ ϕ 2 | E ϕ 1 U ϕ 2 | A ϕ 1 U ϕ 2 | E X ϕ | A X ϕ
CTL model-checking is PTime-complete and the complexity function is bilinear in the size of the formula and in the size of the Kripke structure [START_REF] Clarke | Automatic verification of finitestate concurrent systems using temporal logic specifications[END_REF] (see also the survey paper [START_REF] Schnoebelen | The complexity of temporal logic model checking[END_REF]) whereas CTL satisfiability is ExpTime-complete [START_REF] Clarke | Design and synthesis of synchronization skeletons using branching time temporal logic[END_REF]. By contrast, the satisfiability problem for CTL * is much more complex: 2ExpTime-complete (upper bound from [START_REF] Emerson | The complexity of tree automata and logics of programs[END_REF] and lower bound from [START_REF] Vardi | Improved upper and lower bounds for modal logics of programs[END_REF]).

From LTL formulae to Büchi automata

In this section, we explain how to translate an LTL formula ϕ into an automaton A ϕ such that the language recognized by A ϕ is precisely L(ϕ). However, in order to be of practical use, the translation process can be divided in four stages (at least):

(1) preprocessing the LTL formula using simple logical equivalences, (2) translation of ϕ into a generalized Büchi automaton A ϕ (the core of the construction), (3) simplification and optimization of A ϕ , (4) translation of A ϕ into a Büchi automaton. Indeed, it is legitimate to aim at building Büchi automata as simple as possible, even though we know that in the worst case the translation has an exponential blow-up. This section is mainly dedicated to step (2) with the construction of simple automata. Considerations about steps ( 1) and ( 3) can be found in Sections 1.3.3 and 1.3.6, respectively.

Automata-based approach

The construction of A ϕ from the formula ϕ remains the core for the decision procedures of the satisfiability problem and the model checking problem for LTL specifications. Indeed, the (initial) satisfiability problem amounts to checking the Büchi automaton A ϕ for emptiness. To solve the model-checking problem, one constructs first the product B = M × A ¬ϕ of the model M with the automaton A ¬ϕ so that successful runs of B correspond to infinite runs of M satisfying the formula ¬ϕ. Therefore, L(B) = ∅ if and only if M |= ∀ ϕ and the model-checking problem is again reduced to the emptiness problem for a Büchi automaton.

Note that checking nonemptiness of a Büchi automaton can be done efficiently (NLogSpace or linear time, see e.g. [START_REF] Vardi | Nontraditional applications of automata theory[END_REF]Theorem 12]) since it reduces to several reachability questions in the underlying graph of the automaton: we have to find a reachable accepting state with a loop around it. Since both the satisfiability problem and the model-checking problem for LTL specifications are PSpace-complete, we cannot avoid an exponential blow-up in the worst case when constructing a Büchi automaton A ϕ associated with an LTL formula ϕ. Fortunately, in most practical cases, we can construct a small Büchi automaton A ϕ .

It is therefore very important to have good constructions for the Büchi automaton A ϕ even though there are several interpretations of good. It is indeed important to obtain a small automaton and several techniques have been developed to reduce the size of the resulting automaton [START_REF] Etessami | Fair simulation relations, parity games, and state space reduction for Büchi automata[END_REF]. On the other hand, it is also important to have a quick construction. Some constructions, such as the tableau construction [START_REF] Wolper | The tableau method for temporal logic: An overview[END_REF], may take an exponential time even if the resulting reduced automaton is small. The problem with the most efficient constructions [START_REF] Gastin | Fast LTL to Büchi automata translation[END_REF] is that they are involved, technical and based on more elaborate structures such as alternating automata. Herein we are interested in a good translation from a pedagogical point of view. Our construction is a middle term between tableau constructions and more elaborate constructions based on alternating automata. As a result, it will be efficient, it will produce small automata, and it will be possible to translate non trivial LTL formulae by hand. However, we admit that it is neither the most efficient nor the one that produces the smallest automata.

Büchi automata in a nutshell

We first recall the definition of Büchi automata (BA) and some useful generalizations; a self-contained introduction to the theory of finite-state automata for infinite words can be found in Chapter ??. A BA is a tuple A = (Q, Σ, I, T, F ) where Q is a finite set of states, Σ is the alphabet, I ⊆ Q is the set of initial states, T ⊆ Q×Σ×Q is the set of transitions, and

F ⊆ Q is the set of accepting (repeated, final) states. A run of A is a sequence ρ = s 0 , a 0 , s 1 , a 1 , s 2 , . . . such that (s i , a i , s i+1 ) ∈ T is a transition for all i ≥ 0. The run ρ is successful if s 0 ∈ I is initial and some state of F is repeated infinitely often in ρ: inf(ρ) ∩ F = ∅ where we let inf(ρ) = {s ∈ Q | ∀ i, ∃ j > i, s = s j }. The label of ρ is the word u = a 0 a 1 • • • ∈ Σ ω .
The automaton A accepts the language L(A) of words u ∈ Σ ω such that there exists a successful run of A on the word u, i.e., with label u. For instance, the automaton in Figure 1.2 accepts those words over {a, b} having infinitely many a's (the initial states are marked with an incoming arrow and the repeated states are doubly circled).

When dealing with models for an LTL formula ϕ, the words are over the alphabet

A = 1 2 a b b a Fig. 1.2. L(A) = {u ∈ {a, b} ω | |u|a = ω} Σ = 2 AP(ϕ)
where AP(ϕ) is the set of propositional variables occurring in ϕ. A letter a ∈ Σ is read as a propositional valuation for which exactly the propositional variables in a hold. We take advantage of this natural interpretation for defining sets of letters: given a propositional formula ψ, we let Σ ψ = {a ∈ Σ | a |= ψ} for which "|=" refers to the satisfaction relation from propositional calculus. For instance, we have

Σ p = {a ∈ Σ | p ∈ a}, Σ ¬p = Σ \ Σ p , Σ p∧q = Σ p ∩ Σ q , Σ p∨q = Σ p ∪ Σ q and Σ p∧¬q = Σ p \ Σ q .
In general, a transition between two states s, s ′ will be enabled for all letters satisfying some propositional formula ψ. We use s

Σ ψ --→ s ′ as a concise representation of the set of transitions {s a -→ s ′ | a ∈ Σ ψ }.
Several examples of Büchi automata corresponding to LTL formulae are given in Figure 1.3. In these automata, transitions are labeled with subsets of Σ meaning that all letters in the subset are allowed for the transition. In some cases, the automaton associated with a formula is deterministic, that is for all s ∈ Q and a ∈ Σ, {s ′ | s, a, s ′ ∈ T } has at most one state. Although, determinism is a very desirable property, it is not always possible. For instance, the automaton for G F p is deterministic whereas the automaton for its negation ¬ G F p ≡ F G ¬p must be nondeterministic. This is an easy example showing that deterministic BA are not closed under complement.

By contrast, Büchi automata are closed under union, intersection and complement, which corresponds to the Boolean operations on formulae. It is also easy to construct an automaton for X ϕ from an automaton for ϕ, see for instance the automaton for X X p in Figure 1.3. Finally, one can construct an automaton for ϕ U ψ from automata for ϕ and ψ. Hence, we have a modular construction of A ϕ for any LTL formula ϕ. But both negation and until yield an exponential blowup. Hence this modular construction is non-elementary and useless in practice, see also [START_REF] Meyer | Weak second order theory of successor is not elementary-recursive[END_REF][START_REF] Stockmeyer | The Complexity of Decision Problems in Automata Theory and Logic[END_REF]. Now we introduce a generalization of the acceptance condition of Büchi automata. First, it will fall on transitions instead of states, as considered also in [START_REF] Giannakopoulou | From states to transitions: improving translation of LTL formulae to Büchi automata[END_REF]. Second it will allow conjunctions of classical Büchi conditions. Formally, a generalized Büchi automaton (GBA) is a tuple A = (Q, Σ, I, T, T 1 , . . . , T n ) where Q, Σ, I, T are as above and the acceptance condition which deals with transitions is given by the sets T i ⊆ T for 1 ≤ i ≤ n. For a run ρ of A, we denote by inf T (ρ) the set of transitions that occur infinitely often in ρ and the run is successful if inf T (ρ)∩T i = ∅ for each 1 ≤ i ≤ n. Often, we simply write inf(ρ) instead of inf T (ρ). For instance, a GBA is given in Figure 1.4 where we require both that transitions with short dashes and transitions with long dashes are repeated infinitely often.

F p : 1 2 Σ Σ Σ p or 1 2 Σ ¬p Σ Σ p X X p : 1 2 3 4 Σ Σ Σ p Σ G p : 1 Σ p F G p : 1 2 Σ Σ p Σ p G F p : 1 2 Σ ¬p Σ p Σ p Σ ¬p G(p → F q) : 1 2 Σ ¬p∨q Σ ¬q Σ p∧¬q Σ q p U q : 1 2 Σ p Σ q Σ or 1 2 Σ p∧¬q Σ q Σ p W q : 1 2 Σ p Σ q Σ or 1 2 Σ p∧¬q Σ q Σ p R q : 1 2 Σ q Σ p∧q Σ or 1 2 Σ q∧¬p Σ p∧q Σ Fig. 1.3.

Büchi automata for some LTL formulae

Each GBA A can be easily translated into a classical BA (preserving the language of accepted ω-words). Indeed, it is sufficient to perform a synchronized product A ⊗ B with the automaton B in Figure 1.5 where the accepting Büchi states in the product are those containing the state n in the second component. Synchro-

G F p ∧ G F q: 0 Σ Σ p Σ q Fig. 1.4. Generalized Büchi automaton 0 T 1 T 1 T 2 T 2 T • • • T n T n T Fig. 1.5. Transforming a GBA into a classical BA
nization is performed thanks to the rule below:

t = s 1 a -→ s ′ 1 ∈ A s 2 t -→ s ′ 2 ∈ B s 1 , s 2 a -→ s ′ 1 , s ′ 2 ∈ A ⊗ B
Note that the intended construction can be performed in logarithmic space since typically in order to build the automaton in Figure 1.5 one needs a counter of size O(log(n)) and in order to address some part of the GBA A (in order to build the product) one needs a register of size O(log(|A|)).

Preprocessing the LTL formula

We have now all the background on Büchi automata that are useful for our construction of a GBA associated with an LTL formula. The first step is to put the formula in negative normal form, i.e., to propagate the negation connectives inwards. This can be done while preserving logical equivalence since all the connectives have a dual connective in LTL (X is self-dual). The equivalences below can be read as rewriting rules from left to right:

¬(ϕ ∨ ψ) ≡ (¬ϕ) ∧ (¬ψ) ¬(ϕ ∧ ψ) ≡ (¬ϕ) ∨ (¬ψ) ¬(ϕ U ψ) ≡ (¬ϕ) R (¬ψ) ¬(ϕ R ψ) ≡ (¬ϕ) U (¬ψ) ¬ X ϕ ≡ X ¬ϕ ¬¬ϕ ≡ ϕ
Formally, an LTL formula is in negative normal form (NNF) if it follows the syntax given by

ϕ ::= ⊤ | ⊥ | p | ¬p | ϕ ∨ ϕ | ϕ ∧ ϕ | X ϕ | ϕ U ϕ | ϕ R ϕ
where p ranges over atomic propositions in AP.

In the following, a temporal formula is defined as either a literal (i.e., a propositional variable or its negation) or a formula in NNF with outermost connective among {X, U, R}. Therefore, any LTL formula in NNF is a positive Boolean combination of temporal formulae. Note that, translating an arbitrary LTL formula in NNF does not increase the number of temporal subformulae. This is important since the size of the GBA A ϕ that we will construct depends on the number of temporal subformulae of ϕ. Therefore, before starting the construction, it is useful to rewrite the formula in order to reduce the number of temporal subformulae. Several rewriting rules are presented in [START_REF] Etessami | Optimizing Büchi automata[END_REF][START_REF] Somenzi | Efficient Büchi automata from LTL formulae[END_REF] and we only give below some examples which again should be applied from left to right.

(X ϕ) ∧ (X ψ) ≡ X(ϕ ∧ ψ) (X ϕ) U (X ψ) ≡ X(ϕ U ψ) (ϕ R ψ 1 ) ∧ (ϕ R ψ 2 ) ≡ ϕ R (ψ 1 ∧ ψ 2 ) (ϕ 1 R ψ) ∨ (ϕ 2 R ψ) ≡ (ϕ 1 ∨ ϕ 2 ) R ψ (G ϕ) ∧ (G ψ) ≡ G(ϕ ∧ ψ) G F ϕ ∨ G F ψ ≡ G F(ϕ ∨ ψ)
It is worth noting that the above simplification rules are useful in practice. By contrast, writing a formula in NNF remains a step that mainly eases the presentation of the forthcoming construction. Indeed, propagating the negation connectives inwards can be performed symbolically by storing subformulae of the initial formula augmented with polarities in {0, 1}.

Building simple automata

We start now the description of the core of our construction. A state Z of an automaton A ϕ will be a subset of sub(ϕ), the set of subformulae of ϕ. We say that a set Z of formulae is consistent if it does not contain ⊥ or a pair {ψ, ¬ψ} for some formula ψ (since our formulae are in NNF, ψ could only be a propositional variable). We often need the conjunction of formulae in Z which will be written Z = ψ∈Z ψ. Note that ∅ = ⊤. The formulae in Z are viewed as obligations, i.e., if a run ρ on a word u starts from Z and satisfies the acceptance condition then u |= Z, i.e., u |= ψ for all ψ ∈ Z. More precisely, if we denote by A Z ϕ the automaton A ϕ where Z is the unique initial state, then our construction will guarantee that

L(A Z ϕ ) = {u ∈ Σ ω | u |= Z}
Therefore, the unique initial state of A ϕ will be the singleton set {ϕ}. We say that a set Z of LTL formulae in NNF is reduced if all formulae in Z are either literals or formulae with outermost connective X. Given a consistent and reduced set Z, we write next(Z) to denote the set {ψ | X ψ ∈ Z} and Σ Z to denote the set of letters which satisfy all literals in Z:

Σ Z = p∈Z Σ p ∩ ¬p∈Z Σ ¬p
Equivalently, Σ Z is the set of letters a ∈ Σ such that for every p ∈ AP(ϕ), p ∈ Z implies p ∈ a and ¬p ∈ Z implies p / ∈ a. From a consistent and reduced set Z, the automaton is ready to perform any transition of the form Z a -→ next(Z) with a ∈ Σ Z .

If ψ = ψ 1 ∧ ψ 2 : Y ε -→ Y \ {ψ} ∪ {ψ 1 , ψ 2 } If ψ = ψ 1 ∨ ψ 2 : Y ε -→ Y \ {ψ} ∪ {ψ 1 } Y ε -→ Y \ {ψ} ∪ {ψ 2 } If ψ = ψ 1 R ψ 2 : Y ε -→ Y \ {ψ} ∪ {ψ 1 , ψ 2 } Y ε -→ Y \ {ψ} ∪ {ψ 2 , X ψ} If ψ = G ψ 2 : Y ε -→ Y \ {ψ} ∪ {ψ 2 , X ψ} If ψ = ψ 1 U ψ 2 : Y ε -→ Y \ {ψ} ∪ {ψ 2 } Y ε -→ !ψ Y \ {ψ} ∪ {ψ 1 , X ψ} If ψ = F ψ 2 : Y ε -→ Y \ {ψ} ∪ {ψ 2 } Y ε -→ !ψ Y \ {ψ} ∪ {X ψ}
For instance, for every a ∈ Σ, ∅ a -→ ∅ is a transition which can be interpreted as: when no obligations have to be satisfied, any letter can be read and there are still no obligations. Note that Σ Z = ∅ since Z is consistent, but next(Z) is not reduced in general. We will use ε-transitions to reduce arbitrary sets of formulae in reduced sets so that the semantics of the automaton is preserved. These transitions are handy but they will not belong to the final GBA A ϕ . So let Y be a set of formulae which is not reduced and choose some ψ ∈ Y maximal among the non-reduced formulae in Y (here maximal is for the subformula ordering). Depending on the form of ψ, the ε-transitions allowing to reduce ψ are presented in Table 1.1. The rules for G and F can indeed be derived from those for R and U, they are included for convenience. Indeed, we only introduce transitions between consistent sets. While

ε -→ Y 1 and Y ε -→ Y 2 and Y ≡ Y 1 ∨ Y 2 .
We introduce these ε-transitions iteratively until all states have been reduced. The construction terminates since each step removes a maximal non-reduced formula and introduces only strictly smaller non-reduced formulae (note that X α is not smaller than α but is reduced).

Finally, note the mark !ψ on the second transitions for U and F. It denotes the fact that the eventuality ψ 2 has been postponed. The marked transitions will be used to define the acceptance condition of the GBA in such a way that all eventualities are satisfied along an accepting run.

In Figure 1.6 we show the ε-transitions that are introduced when we start with a singleton set {ϕ} with ϕ = G(p → F q) ≡ ⊥ R (¬p ∨ (⊤ U q)). Note again the mark !F q on the last transition.

ϕ = G(¬p ∨ F q) ¬p ∨ F q, X ϕ ε ¬p, X ϕ ε F q, X ϕ ε q, X ϕ ε X F q, X ϕ ε !F q
({ϕ}) = {{¬p, X ϕ}, {q, X ϕ}, {X F q, X ϕ}} Red F q ({ϕ}) = {{¬p, X ϕ}, {q, X ϕ}}
Observe that in Red F q ({ϕ}), the subscript F q refers to an absence of ε-transitions marked by !F q along the reduction path. This is the case when we do not have the obligation F q or if the eventuality F q is satisfied now by imposing the obligation q. By contrast, an ε-transition {F q, X ϕ} ε -→ !F q {X F q, X ϕ} with mark !F q indicates that the eventuality F q is not satisfied now. We hope this is not too confusing.

We give now the formal definition of A ϕ = (Q, Σ, I, T, (T α ) α∈U(ϕ) ). The set of states is Q = 2 sub(ϕ) and the initial state is the singleton I = {ϕ}. The set of transitions is defined as follows:

T = {Y a -→ next(Z) | Y ∈ Q, a ∈ Σ Z and Z ∈ Red(Y )}
For each α ∈ U(ϕ), we define the acceptance set T α :

T α = {Y a -→ next(Z) | Y ∈ Q, a ∈ Σ Z and Z ∈ Red α (Y )}
Since ∅ ∈ Q and Σ ∅ = Σ, the transition ∅ Σ -→ ∅ belongs to T and to T α for each α ∈ U(ϕ). Note that, if ϕ does not have until subformulae then there are no acceptance conditions, which means that all infinite paths are successful.

In practice, we only compute and include in A ϕ the states and transitions that are reachable from the initial state {ϕ} so that Q is only a subset of 2 sub(ϕ) . The first automaton in Figure 1.7 shows the complete construction, including the ε-transitions and the intermediary dashed states, for the response formula ϕ = G(p → F q). After removing the intermediary dashed states and the εtransitions, we obtain the second automaton in Figure 1.7 where the transitions from the unique acceptance condition T F q are labelled with F q. As Σ ¬p ⊆ Σ, the loop labeled Σ ¬p on the second state is redundant ‡ . Similarly, the transitions labeled Σ ¬p∧q is redundant. We obtain the third GBA A ϕ in Figure 1.7. It is then easy to check that L(A ϕ ) = {u ∈ Σ ω | u |= ϕ}.

Correctness

More examples will conclude this section. Let us first show the correctness of the construction. The main result is stated in Theorem 1.2.

Theorem 1.2. The automaton A ϕ accepts precisely the models of ϕ, i.e.,

L(A ϕ ) = L(ϕ) = {u ∈ Σ ω | u |= ϕ}
In order to be precise, ϕ satisfies much more models by considering the larger set of propositional variables that do not appear in ϕ. Indeed such propositional variables are simply irrelevant for the satisfaction of ϕ. The proof of this theorem requires several lemmas and propositions. The first lemma is trivial.

α = α 1 U α 2 ∈ U(ϕ), if u |= α 2 , then Z ∈ Red α (Y ).

Proof. Consider again the reduction rules presented in

-→ Y 1 and Y ≡ Y 1 or we have two ε- transitions Y ε -→ Y 1 and Y ε -→ Y 2 and Y ≡ Y 1 ∨ Y 2 .
So there is a reduction path from Y to some Z ∈ Red(Y ) such that u |= Z and whenever we reduce an until formula α = α 1 U α 2 with u |= α 2 we take the first reduction Y ′ ε -→ Y ′ \ {α} ∪ {α 2 }. ‡ Actually this corresponds to a set of transitions which is contained in the set of transitions described by the loop labeled Σ.

ϕ = G(¬p ∨ F q) ¬p ∨ F q, X ϕ ε ¬p, X ϕ ε F q, X ϕ ε q, X ϕ ε X F q, X ϕ ε !F q Σ ¬p Σ q F q, ϕ Σ F q, ¬p ∨ F q, X ϕ ε F q, ¬p, X ϕ ε ε X F q, ¬p, X ϕ q, ¬p, X ϕ ε !F q ε Σ ¬p Σ ¬p∧q ϕ = G(¬p ∨ F q) F q, ϕ Σ Σ q F q Σ ¬p∧q F q Σ q F q Σ ¬p F q Σ Σ ¬p ϕ = G(¬p ∨ F q) F q, ϕ Σ Σ q F q Σ ¬p∨q F q Σ Fig. 1.7. GBA for the response formula Now, let α = α 1 U α 2 ∈ U(ϕ) be such that u |= α 2 .
Either α is never reduced along this path and indeed Z ∈ Red α (Y ) or α is reduced and by the hypothesis above we took the unmarked ε-transition. Hence Z ∈ Red α (Y ).

Proposition 1.5. L(ϕ) ⊆ L(A ϕ ).

Proof. Let u = a 0 a 1 a 2 • • • ∈ Σ ω be such that u |= ϕ. By induction, we build ρ = Y 0 a0 -→ Y 1 a1 -→ Y 2 • • •
of A ϕ such that for all n ≥ 0 we have u, n |= Y n and there is some

Z n ∈ Red(Y n ) with a n ∈ Σ Zn and Y n+1 = next(Z n ).
We start with Y 0 = {ϕ}. Assume now that u, n |= Y n for some n ≥ 0. By Lemma 1.4, there is

Z n ∈ Red(Y n ) such that u, n |= Z n and for all until subformulae α = α 1 U α 2 ∈ U(ϕ), if u, n |= α 2 then Z n ∈ Red α (Y n ). Then we define Y n+1 = next(Z n ). Since u, n |= Z n , Lemma 1.3 implies a n ∈ Σ Zn and u, n + 1 |= Y n+1 . Therefore, ρ is a run for u in A ϕ .
It remains to show that ρ is successful. By definition, it starts from the initial state {ϕ}. Now let α = α 1 U α 2 ∈ U(ϕ). Assume there exists N ≥ 0 such that Y n an --→ Y n+1 / ∈ T α for all n ≥ N . Then Z n / ∈ Red α (Y n ) for all n ≥ N and we deduce that u, n |= α 2 for all n ≥ N . But, since Z N / ∈ Red α (Y N ), the formula α has been reduced using an ε-transition marked !α along the path from Y N to Z N . Therefore, X α ∈ Z N and α ∈ Y N +1 . By construction of the run we have u, N + 1 |= Y N +1 . Hence, u, N + 1 |= α, a contradiction with u, n |= α 2 for all n ≥ N . Consequently, the run ρ is successful and u is accepted by A ϕ .

We prove now the converse inclusion.

Proposition 1.6. L(A ϕ ) ⊆ L(ϕ). Proof. Let u = a 0 a 1 a 2 • • • ∈ Σ ω and let ρ = Y 0 a0 -→ Y 1 a1 -→ Y 2 • • •
be an accepting run of A ϕ for the word u. We show by induction that for all ψ ∈ sub(ϕ) and n ≥ 0, for all reduction path Yn

ε -→ * Y ε -→ * Z with an ∈ ΣZ and Yn+1 = next(Z), if ψ ∈ Y then u, n |= ψ.
The induction is on the formula ψ with the subformula ordering.

If ψ = ⊤ then the result is trivial. Assume next that ψ = p ∈ AP(ϕ). Since p is reduced, we have p ∈ Z and it follows Σ Z ⊆ Σ p . Therefore, p ∈ a n and u, n |= p. The proof is similar if ψ = ¬p for some p ∈ AP(ϕ).

If ψ = X ψ 1 then ψ ∈ Z and ψ 1 ∈ Y n+1 . By induction we obtain u, n + 1 |= ψ 1 and we deduce u, n |= X ψ 1 = ψ.

Assume now that ψ = ψ 1 ∧ ψ 2 . Along the path Y ε -→ * Z the formula ψ must be reduced so

Y ε -→ * Y ′ ε -→ * Z with ψ 1 , ψ 2 ∈ Y ′ .
By induction, we obtain u, n |= ψ 1 and u, n |= ψ 2 . Hence, u, n |= ψ. The proof is similar for

ψ = ψ 1 ∨ ψ 2 . Assume next that ψ = ψ 1 U ψ 2 . Along the path Y ε -→ * Z the formula ψ must be reduced so Y ε -→ * Y ′ ε -→ Y ′′ ε -→ * Z with either Y ′′ = Y ′ \ {ψ} ∪ {ψ 2 } or Y ′′ = Y ′ \ {ψ} ∪ {ψ 1 , X ψ}.
In the first case, we obtain by induction u, n |= ψ 2 and therefore u, n |= ψ. In the second case, we obtain by induction u

, n |= ψ 1 . Since X ψ is reduced we get X ψ ∈ Z and ψ ∈ next(Z) = Y n+1 . Let k > n be minimal such that Y k a k -→ Y k+1 ∈ T ψ (such a value k exists since ρ is accepting). We first show by induction that u, i |= ψ 1 and ψ ∈ Y i+1 for all n < i < k. Recall that ψ ∈ Y n+1 . So let n < i < k be such that ψ ∈ Y i . Let Z ′ ∈ Red(Y i ) be such that a i ∈ Σ Z ′ and Y i+1 = next(Z ′ ). Since k is minimal we know that Z ′ / ∈ Red ψ (Y i ). Hence, along any reduction path from Y i to Z ′ we must use a step Y ′ ε -→ !ψ Y ′ \ {ψ} ∪ {ψ 1 , X ψ}.
By induction on the formula we obtain u, i |= ψ 1 . Also, since X ψ is reduced, we have The last case is when

X ψ ∈ Z ′ and ψ ∈ next(Z ′ ) = Y i+1 . Second, we show that u, k |= ψ 2 . Since Y k a k -→ Y k+1 ∈ T ψ , we find some Z ′ ∈ Red ψ (Y k ) such that a k ∈ Σ Z ′ and Y k+1 = next(Z ′ ). Since ψ ∈ Y k along some reduction path from Y k to Z ′ we use a step Y ′ ε -→ Y ′ \ {ψ} ∪ {ψ 2 }. By induction we obtain u, k |= ψ 2 . Finally, we have shown u, n |= ψ 1 U ψ 2 = ψ. ϕ = p U (q U r) ψ = q U r ∅ Σ p ψ Σ q ϕ Σ ϕ, ψ Σ q ϕ Σ r ϕ, ψ Σ r ϕ, ψ
ψ = ψ 1 R ψ 2 . Along the path Y ε -→ * Z the formula ψ must be reduced so Y ε -→ * Y ′ ε -→ Y ′′ ε -→ * Z with either Y ′′ = Y ′ \ {ψ} ∪ {ψ 1 , ψ 2 } or Y ′′ = Y ′ \ {ψ} ∪ {ψ 2 , X ψ}.
In the first case, we obtain by induction u, n |= ψ 1 and u, n |= ψ 2 . Hence, u, n |= ψ and we are done. In the second case, we obtain by induction u, n |= ψ 2 and we get also ψ ∈ Y n+1 . Continuing with the same reasoning, we deduce easily that either u, n

|= G ψ 2 or u, n |= ψ 2 U (ψ 1 ∧ ψ 2 ).
We have proved the correctness of our construction. We give now more examples and discuss simplifications that may be applied during the construction. First, consider ϕ = p U (q U r). Here we have two until formulae, ϕ itself and ψ = q U r, hence the GBA will have two acceptance sets T ϕ and T ψ . We can easily check that Red({ϕ}) = {{p, X ϕ}, {q, X ψ}, {r}} Red ϕ ({ϕ}) = {{q, X ψ}, {r}} Red ψ ({ϕ}) = {{p, X ϕ}, {r}} Hence, starting from the initial state {ϕ}, the construction introduces two new states {ψ} and ∅. We compute Red({ψ}) = {{q, X ψ}, {r}} Red ϕ ({ψ}) = {{q, X ψ}, {r}}

Red ψ ({ψ}) = {{r}}

There are no new states, so the construction terminates and we obtain the GBA of Figure 1.8 where the transitions from T ϕ and T ψ are marked ϕ and ψ respectively.

The polynomial space upper bound for LTL model-checking can be then stated as follows. • A ¬ϕ is the Büchi automaton recognizing the models for ¬ϕ obtained with the previous constructions. Its size is 2 O(|ϕ|) . • "⊗" denotes the product operation used for intersection.

Nonemptiness of A M,s ⊗ A ¬ϕ can be then checked on the fly in nondeterministic polynomial space since A M,s ⊗ A ¬ϕ is of size |M| × 2 O(|ϕ|) . By Savitch's theorem (see e.g. [START_REF] Papadimitriou | Computational Complexity[END_REF]), we then obtain Proposition 1.7. A similar reasoning can be done for existential model checking since M, s |= ∃ ϕ holds if and only if L(A M,s ⊗ A ϕ ) = ∅. Furthermore, the properties about the construction of A ϕ allow also to get the polynomial space upper bound for satisfiability and validity.

Proposition 1.8. [START_REF] Sistla | The complexity of propositional linear temporal logic[END_REF] Checking whether an LTL formula ϕ is satisfiable (or valid) can be done in space polynomial in |ϕ|.

1.3.6. On the fly simplifications of the GBA One optimization was already included in the contruction: when reducing a set Y of formulae, we start with maximal formulae. This strategy produces fewer εtransitions and fewer states in the set Red(Y ). For instance, assume that Y = {ϕ, G ϕ}. If we reduce first the maximal formula G ϕ we obtain Y ′ = {ϕ, X G ϕ} and it remains to reduce ϕ. We obtain the sets Z ∪ {X G ϕ} for Z ∈ Red({ϕ}). If instead we start by reducing ϕ we obtain the sets Z ∪ {G ϕ} for Z ∈ Red({ϕ}. But then G ϕ has to be reduced so that we obtain the sets Z ∪ {ϕ, X G ϕ} and ϕ has to be reduced again. We obtain finally sets

Z 1 ∪ Z 2 ∪ {X G ϕ} for Z 1 , Z 2 ∈ Red({ϕ}).
Next, during the reduction, we may replace a set Y by Y ′ provided they are equivalent, i.e., Y ≡ Y ′ . Checking equivalence is as hard as constructing the automaton, so we only use easy syntactic equivalences. For instance, we may use the following rules:

If ψ = ψ 1 ∨ ψ 2 and ψ 1 ∈ Y or ψ 2 ∈ Y : Y ε -→ Y \ {ψ} If ψ = ψ 1 U ψ 2 and ψ 2 ∈ Y : Y ε -→ Y \ {ψ} If ψ = ψ 1 R ψ 2 and ψ 1 ∈ Y : Y ε -→ Y \ {ψ} ∪ {ψ 2 }
We explain now an easy and useful simplification of the constructed GBA: when two states have the same outgoing transitions, then they can be merged. More precisely, two states s 1 and s 2 of a GBA A = (Q, Σ, I, T, T 1 , . . . , T n ) have the same outgoing transitions if for all a ∈ Σ and s ∈ Q, we have

(s 1 , a, s) ∈ T ⇐⇒ (s 2 , a, s) ∈ T and (s 1 , a, s) ∈ T i ⇐⇒ (s 2 , a, s) ∈ T i for all 1 ≤ i ≤ n.
In this case, the two states s 1 and s 2 can be merged without changing the accepted language. When merging these states, we redirect all transitions to either s 1 or s 2 to the new merged state s 1,2 .

With our construction, we have an easy sufficient condition ensuring that two states Y and Y ′ have the same outgoing transitions:

Red(Y ) = Red(Y ′ ) and Red α (Y ) = Red α (Y ′ ) for all α ∈ U(ϕ) (1.1)
For instance, consider the formula ϕ = G F p. We have

Red({ϕ}) = {{p, X ϕ}, {X F p, X ϕ}} Red F p ({ϕ}) = {{p, X ϕ}}
Hence, from the initial state {ϕ}, we reach a new state {F p, ϕ}. We can easily check that the two states satisfy (1.1) hence they can be merged and the resulting GBA has only one state and two transitions:

Σ p F p Σ ¬p Similarly, if we consider ϕ = G F p ∧ G F q. We have Red({ϕ}) = {{p, q, X G F p, X G F q}, {p, X F q, X G F p, X G F q}, {q, X F p, X G F p, X G F q}, {X F p, X F q, X G F p, X G F q}} Red F p ({ϕ}) = {{p, q, X G F p, X G F q}, {p, X F q, X G F p, X G F q}} Red F q ({ϕ}) = {{p, q, X G F p, X G F q}, {q, X F p, X G F p, X G F q}}
Hence, a direct application of the construction produces an automaton with 4 new states. However, we can easily check with (1.1) that all states have the same outgoing transitions. Hence, again, the resulting GBA has only one state and 4 transitions which are marked F p or F q if they belong to T F p or T F q :

Σ p F p Σ q F q Σ p∧q F p, F q Σ
More examples are given in Figure 1.9. Other optimizations can be found in [START_REF] Couvreur | On-the-fly verification of linear temporal logic[END_REF][START_REF] Wolper | Constructing automata from temporal logic formulas: A tutorial[END_REF], as well as simplifications of Büchi automata generated from LTL formulae in [START_REF] Gastin | Fast LTL to Büchi automata translation[END_REF].

Related work

The construction presented in this section is in the same vein as those presented in [START_REF] Gerth | Simple on-the-fly automatic verification of linear temporal logic[END_REF][START_REF] Couvreur | On-the-fly verification of linear temporal logic[END_REF][START_REF] Wolper | Constructing automata from temporal logic formulas: A tutorial[END_REF][START_REF] Manna | Temporal Verification of Reative Systems: Safety[END_REF], see also [START_REF] Tauriainen | Automata and Linear Temporal Logic: Translations with Transitionbased Acceptance[END_REF]. For instance, the states of the automata in [START_REF] Wolper | Constructing automata from temporal logic formulas: A tutorial[END_REF]

ϕ = F G p : ϕ G p Σ Σ p F G p Σ p F G p ϕ = G(p → X(q U r) : ϕ ϕ, q U r Σ ¬p q U r Σ q U r Σ ¬p∧r q U r Σ r q U r Σ q∧¬r ϕ = F(p → X(q U r) : ϕ q U r ∅ Σ q U r Σ ¬p ϕ, q U r Σ ϕ, q U r Σ q ϕ Σ r ϕ, q U r Σ ϕ, q U r Fig. 1.9. More examples ¬p, X ϕ q, X ϕ X F q, X ϕ X F q, ¬p, X ϕ q, ¬p, X ϕ Σ ¬p Σ ¬p Σ ¬p Σ q Σ q Σ q Σ Σ Σ Σ Σ ¬p Σ ¬p Σ ¬p Σ ¬p Σ ¬p∧q Σ ¬p∧q Σ ¬p∧q
Fig. 1.10. Another GBA for the response formula correspond to our reduced sets and the transitions are constructed by applying first the next step and then the reduction phase. For the response formula G(p → F q) there are 5 reduced sets (see Figure 1.7) and we would get the automaton of Figure 1.10. Note that, except possibly for the initial state, each of our states is the next state of some reduced set. But we usually have several reduced sets having the same next set. Hence, our construction cannot yield more states (still apart demri-gastin-SI-bangalore-final possibly for the initial state) and usually yield fewer states than the construction of [START_REF] Wolper | Constructing automata from temporal logic formulas: A tutorial[END_REF] as in the example above. Another difference is that [START_REF] Wolper | Constructing automata from temporal logic formulas: A tutorial[END_REF] uses acceptance conditions based on states whereas we use transition-based acceptance. Moreover, tableau methods for LTL, see e.g. [START_REF] Wolper | The tableau method for temporal logic: An overview[END_REF], contain decomposition rules similar to the reduction rules and contain an additional step to check global conditions about eventuality formulae (in U(ϕ)). Our construction is therefore similar to such methods since the expansion of a state (or branch in the tableau terminology) is done on demand and the verification of eventualities is simply performed by transition-based acceptance conditions. Hence, the two phases of the method in [START_REF] Wolper | The tableau method for temporal logic: An overview[END_REF] apply also herein and in the worst-case we also obtain exponential-size automata. It is worth recalling that a one-pass tableaux calculus for LTL is presented in [START_REF] Schwendimann | A new one-pass tableau calculus for PLTL[END_REF] by using additional control structures (no step to check global conditions). Finally, there is another solution to encode the second phase of the method in [START_REF] Wolper | The tableau method for temporal logic: An overview[END_REF], which is to translate LTL model-checking into CTL model-checking with fairness conditions [START_REF] Clarke | Another look at LTL model checking[END_REF].

Helpful bibliographical remarks can also be found at the end of [48, Chapter 5] as well as in [START_REF] Tauriainen | Automata and Linear Temporal Logic: Translations with Transitionbased Acceptance[END_REF].

Extensions

In this section, we consider three extensions for developments made in Section 1.3. Firstly, we show how a procedure solving LTL model-checking can be used to solve CTL * model-checking. Secondly, we present an extension of LTL with temporal operators defined from finite-state automata. Thirdly, we show that adding a single temporal operator defined by a context-free language leads to undecidability.

Model-checking for branching-time CTL *

Even though CTL * is a branching-time logic, MC ∀ (CTL * ) can be solved by using as subroutine the algorithm for LTL model-checking with a simple renaming technique. Proposition 1.9. [34] MC ∀ (CTL * ) is PSpace-complete.

Proof. Since MC ∀ (LTL) is a subproblem of MC ∀ (CTL * ), the PSpace-hardness is immediate. In order to show that MC ∀ (CTL * ) is in PSpace, we use known techniques for LTL plus renaming.

For each quantifier Q ∈ {∃, ∀}, we write MC Q LTL (M, s, ϕ) to denote the function that returns true if and only if M, s |= Q ϕ. We have seen that these functions can be computed in polynomial space in |ϕ| + log(|M|) (Proposition 1.7). In order to establish the PSpace upper bound, here is an algorithm based on formulae renaming using only polynomial space:

MC ∀ CTL * (M = W, R, λ , s ∈ W, ϕ)
• If E, A do not occur in ϕ, then return MC ∀ LTL (M, s, ϕ). • Otherwise ϕ contains a subformula Qψ where E, A do not occur in ψ and Q ∈ {E, A}. This means that the formula ψ belongs to LTL. Let Q ′ be "∀" if Q = A, "∃" otherwise. Let p Qψ be a new propositional variable. We define λ ′ an extension of λ for every s ′ ∈ W by:

λ ′ (s ′ ) = λ(s ′ ) ∪ {p Qψ } if MC Q ′ LTL (M, s ′ , ψ) λ(s ′ ) otherwise. Return MC ∀ CTL * ( W, R, λ ′ , s, ϕ[Qψ ← p Qψ ])
where ϕ[Qψ ← p Qψ ] is obtained from ϕ by replacing every occurrence of Qψ by p Qψ .

Since in MC ∀

CTL * (M, s, ϕ), the recursion depth is at most |ϕ|, we can show that MC ∀ CTL * uses only polynomial space since MC ∃ LTL and MC ∀ LTL require only polynomial space. The soundness of the algorithm is not very difficult to show.

Automata-based temporal operators

We have seen how to build a GBA A ϕ such that L(A ϕ ) is equal to the set of models for ϕ (in LTL). However, it is known that LTL is strictly less expressive than Büchi automata [START_REF] Wolper | Temporal logic can be more expressive[END_REF]. It is not always easy to figure out whether a given Büchi automaton on the alphabet 2 AP(ϕ) corresponds to an LTL formula where AP(ϕ) denotes the set of propositional variables occurring in ϕ. For instance, is there an LTL formula, counterpart of the automaton presented below?

q 0 q 1 {p} {p}, {}
We invite the reader to analyze why none of the formulae below is adequate:

(

1) p ∧ X ¬p ∧ G(p ↔ X X p), ( 2
) p ∧ G(p → X X p), (3) q ∧ X ¬q ∧ G(q ↔ X X q) ∧ G(q → p).
For instance, formula (1) defines a unique model over the two-letters alphabet 2 {p} . Note that formula (3) requires that p holds at all even positions but uses an extra propositional variable which is not allowed by the alphabet of the automaton. Actually, there exist quite simple properties that cannot be expressed with LTL.

To check whether an ω-regular language L can be expressed in LTL, one may compute the syntactic monoid of L from the automaton which recognizes L and check that this monoid is aperiodic, see e.g. the survey chapter [START_REF] Diekert | First-order definable languages[END_REF]. This procedure can be applied to prove the following result (even though the proof in [START_REF] Wolper | Temporal logic can be more expressive[END_REF] is different).

Proposition 1.10. [START_REF] Wolper | Temporal logic can be more expressive[END_REF] There is no LTL formula ϕ built over the unique propositional variable p such that L(ϕ) is exactly the set of LTL models such that p holds on every even position (on odd positions, p may be true or not).

That is why, in [START_REF] Wolper | Temporal logic can be more expressive[END_REF], an extension of LTL has been introduced by adding temporal operators defined with finite-state automata. Alternatively, right-linear grammars can also be used to define regular languages. Let A = Σ, S, S 0 , ρ, F be a finite-state automaton with letters from a linearly ordered alphabet Σ, say with the ordering a 1 < . . . < a k . Assume that we already have defined the formulae ϕ 1 , . . . , ϕ k . Then, A(ϕ 1 , . . . , ϕ k ) is a new formula in the Extended Temporal Logic (ETL). The relation u, i |= A(ϕ 1 , . . . , ϕ k ) holds when a finite pattern induced from L(A) exists from position i. There is a correspondence between the letters a 1 , . . . , a k and the arguments ϕ 1 , . . . , ϕ k . More precisely u, i |= A(ϕ 1 , . . . , ϕ k ) if there is a finite word a i1 a i2 . . . a in ∈ L(A) such that for every 1 ≤ j ≤ n, we have u, i + (j -1) |= ϕ ij .

Note that, if S 0 ∩ F = ∅, then ε ∈ L(A) and A(ϕ 1 , . . . , ϕ k ) is equivalent to ⊤. Observe also that in the condition above, the index of the k-th letter (with k ∈ {1, . . . , n}) determines which argument must hold at the (k-1)-th next position. We present below a model for the ETL formula A(p, q) with L(A) = {ab i a | i ≥ 0} and a < b.

p q q q q p a b b b b a ∈ L(A)
A(p, q)

By way of example, the formula ϕ U ψ is equivalent to B(ϕ, ψ) with L(B) = a * b and a < b. Similarly, the weakness of LTL described in Proposition 1.10 can be fixed within ETL: the formula ¬A(⊤, ¬p) with L(A) = (a 2 ) * b holds exactly in models such that the propositional variable p holds on every even position.

Formally, the syntax of ETL allows the propositional variables, the boolean connectives and temporal modalities of the form A(ϕ 1 , . . . , ϕ k ). Note that it does not include the temporal operators from LTL since they can be expressed with automata.

In order to illustrate the expressive power of ETL, it is sufficient to consider the fragment ETL -defined by the syntax below:

ϕ ::= ⊤ | ¬ϕ | ϕ ∨ ϕ | K • ϕ
where K ⊆ Σ * is a regular language of finite words over some finite alphabet Σ ⊆ 2 AP such that each letter a ∈ Σ is a finite set. The semantics is that w |= K • ϕ if we can write w = uv with u ∈ K and v |= ϕ. To show that K • ϕ can be expressed in ETL, consider an automaton A for K • # where # is a new letter (larger than all letters from Σ). For each a ∈ Σ, let ϕ a = p∈a p ∧ p / ∈a ¬p. Then, K • ϕ is expressed by A((ϕ a ) a∈Σ , ϕ) where ϕ a is substituted for a ∈ Σ and ϕ is substituted for the trailing #.

Lemma 1.11. For any ω-regular language L over a finite alphabet Σ ⊆ 2 AP made of finite letters, there is a formula ϕ in ETL -such that L = L(ϕ).

Proof. First, observe that any ω-regular language L over Σ can be written as a finite union of languages of the form K • L where K ⊆ Σ * is regular and L ⊆ Σ ω is deterministic, i.e., recognized by a deterministic Büchi automaton. This can be easily derived from a deterministic Muller automaton recognizing L.

So consider a deterministic and complete Büchi automaton A = (Q, Σ, {i}, δ, F ). For each s ∈ Q, we define

M s = {u ∈ Σ * | δ(i, u) = s} N s = {v ∈ Σ * | δ(s, v) ∈ F }.
Then, we can show

L(A) = s∈Q M s • N s • Σ ω
We deduce immediately that L(A) can be expressed with the formula

¬ s∈Q M s • ¬(N s • ⊤)
Consequently, given an ω-regular language defined by a finite union of the form K i • L i where each K i ⊆ Σ * is regular, each L i ⊆ Σ ω is deterministic, the corresponding ETL -formula is of the form below:

i K i • ¬ s∈Qi M s i • ¬(N s i • ⊤)
As a corollary, any ω-regular language can be defined by an expression obtained from the grammar L ::= Σ ω | L ∪ L | L | K • L, where K ranges over the regular languages in Σ * .

Even though ETL formulae are seldom used in specification languages, its main theoretical assets rest on its high expressive power and on the relatively low complexity of satisfiability/model-checking problems as stated below.

Proposition 1.12. [START_REF] Vardi | Reasoning about infinite computations[END_REF] (I) MC ∀ (ETL), MC ∃ (ETL) and SAT(ETL) are PSpace-complete. (II) ETL has the same expressive power as Büchi automata.

An automata-based construction for ETL formulae can be found in [START_REF] Wolper | Temporal logic can be more expressive[END_REF], leading to Proposition 1.12(I). Proposition 1.12(II) is a corollary of Lemma 1.11.

Proposition 1.12(I) entails that ETL model-checking is not more difficult than LTL model-checking in the worst case, modulo logarithmic space many-one reductions. This is quite surprising in view of the expressive power of ETL -Proposition 1.12(II). Hence, the class of languages defined by ETL formulae is equal to the class of languages defined by • Büchi automata (Proposition 1.12(II)),

• formulae from monadic second-order theory for ω, < (S1S) and ω-regular expressions (finite unions of sets U V ω with regular U, V ⊆ Σ * ), see e.g. [52, Chapter III],

• formulae from LTL with second-order quantification. In such an extension of LTL, we allow formulae of the form ∀p . ϕ with u, i |= ∀p . ϕ if for every u ′ such that u and u ′ agree on all propositional variables different from p, we have u ′ , i |= ϕ, see e.g. [START_REF] Wolper | Reasoning about infinite computation paths[END_REF]. • formulae from LTL with fixed-point operators [START_REF] Vardi | A temporal fixpoint calculus[END_REF].

So, ETL is a powerful extension of LTL but the above equivalences do not mean that all the above formalisms have the same conciseness. Actually, we know the following complexity results:

• the nonemptiness problem for Büchi automata is NLogSpace-complete, • MC ∀ (ETL), MC ∃ (ETL) and SAT(ETL) are PSpace-complete,

• satisfiability for LTL with fixed-point operators is PSpace-complete [START_REF] Vardi | A temporal fixpoint calculus[END_REF],

• satisfiability for S1S is non-elementary (time complexity is not bounded by any tower of exponential of fixed height) [START_REF] Meyer | Weak second order theory of successor is not elementary-recursive[END_REF].

So, S1S is the most concise language for describing ω-regular languages.

Context-free extensions

It is possible to extend the definition of ETL by replacing formulae of the form A(ϕ 1 , . . . , ϕ n ) by formulae of the form L(ϕ 1 , . . . , ϕ n ) where L is a language of finite words specified within a fixed formalism. The language L is again viewed as a set of patterns, not necessarily regular. For a class C of languages, we write PC[C] to denote the extension the propositional calculus with formulae of the form L(ϕ 1 , . . . , ϕ n ) for some L ∈ C. Obviously, ETL is precisely equivalent to PC [REG] where REG is the class of regular languages represented by finite-state automata.

We have seen that ETL is decidable and it is natural to wonder whether PC[CF] is also decidable where CF is the class of context-free languages (represented by context-free grammars).

Undecidability of PC[CF]

Since numerous problems for context-free languages are undecidable, it is not very surprising to get the following result.

Proposition 1.13. SAT(PC[CF]) is undecidable.

Before presenting the proof, let us recall that the next operator X and the until operator U (and the derived operators F and G) can be defined as operators obtained from finite-state automata. Hence, in the proof below, we use them freely.

Proof. We reduce the recurring domino problem DOMREC [START_REF] Harel | Recurring dominoes: making the highly undecidable highly understandable[END_REF] to satisfiability for PC[L 1 ]. Let Sides = {left , right , up, down} and recall that a domino game is a structure Dom = C, D, γ where C is a finite set of colours, D is a finite set of dominoes, and γ : D × Sides → C is a map that assigns a color to each side of the dominoes. Dom can tile N × N if and only if there is a map f : N × N → D that satisfies the color constraints. This means that only domino sides with identical colors can be adjacent (no rotation of dominoes is allowed). The problem DOMREC, known to be Σ 1 1 -complete [START_REF] Harel | Recurring dominoes: making the highly undecidable highly understandable[END_REF], takes as input a domino game Dom with a distinguished color c and asks whether Dom can pave N × N where the color c occurs infinitely often in the first column.

Let Dom = C, D, γ be a domino game with C = {1, . . . , n}, D = {1, . . . , m}, and c = 1. So we have an instance of DOMREC. Let us explain the syntactic ressources we shall need. We use the following propositional variables:

• in is a propositional variable that holds when the state encodes a position in N 2 . Indeed, there are states in the model that do not correspond to positions in N 2 . In order to facilitate the presentation, we also introduce out that is equivalent to the negation of in. • For every j ∈ D, we introduce the variable d j with intended meaning that "the position in N 2 associated with the current state is occupied by a domino of type j". • For every i ∈ C, we use the variables up i , down i , left i , right i . For instance, up 1 holds whenever the domino on the position associated with the current state has color 1 on its top.

Every state encoding a position in N 2 is occupied by a unique domino:

G   in → 1≤j≤m   d j ∧ 1≤k≤m,k =j ¬d k    
Propositional variables for colours are compatible with the definition of domino types:

1≤j≤m s∈Sides G   in ∧ d j → s γ(j,s) ∧ 1≤k≤n,k =γ(j,s) ¬s k  
We write PAVE to denote the conjunction of the above formulae. Now, we shall define the states of the model that correspond to positions in N 2 . We write SNAKE to denote the conjunction of the following formulae: The only structure (built over {in, out }) satisfying SNAKE is:

• G(in ↔ ¬out ), • in ∧ X out ∧ X X in ∧ X X X in ∧ X X X X out, • G(out → X L 1 (in, out , in ∧ X out )). out, ⇑ out , ⇑ out, ⇑ out, ⇓ out, ⇓ in, ⇓ in, ⇑ in, ⇓ in, ⇑ in, ⇓ in, ⇑ in, ⇓ in, ⇑ in, ⇓ in, ⇓ in, ⇑ in, ⇓ in, ⇑ in, ⇓ in, ⇓
{in} • {out} • {in} 2 • {out} • {in} 3 • {out} • {in} 4 . . .
This sequence makes reference to the path presented in Figure 1.11, where the set of grey nodes encodes N 2 . The difficulty of the proof is not to design a path through N 2 but rather to define a path on which it is easy to access to neighbours (right or up). Moreover, we need to identify the positions encoding the first column of N 2 . Consequently, a bit more work is required. For every state in, we need to remember if it occurs in a sequence of in that is upward or downward (alternately, this encodes the parity of i for each block {out} • {in} i •{out}). Indeed, this criterion is relevant to access to (right or up) neighbours. We introduce the variables ⇑ and ⇓. The former one ⇑ is only introduced to facilitate the presentation. We write DIRECTION to denote the conjunction of the following formulae: This structure encodes the path through N 2 described in Figure 1.11. The path allows to access to adjacent states as follows:

• G(⇑ ↔ ¬⇓), • ⇓ ∧ X ⇑, • G(in ∧ X in ∧ ⇑ → X ⇑) ("we stay on upward sequence"), • G(in ∧ X in ∧ ⇓ → X ⇓) ("we stay on downward sequence"), • G(in ∧ X out ∧ ⇑ → (X ⇓ ∧ X X ⇓)) ("we pass from upward to downward sequence"), • G(in ∧ X out ∧ ⇓ → (X ⇑ ∧ X X ⇑)) ("
• in a state {in, ⇑}, we access to the up and right neighbours with the help of L 0 and L 1 , respectively, • in a state {in, ⇓}, we access to the up and right neighbours with the help of L 1 and L 0 , respectively,

We write CONSTRAINTS to denote the conjunction of following formulae that express color constraints for adjacent dominoes:

• G(in ∧ ⇑ → 1≤i≤n right i → L 1 (in, out , left i ))),

• G(in ∧ ⇑ → ( 1≤i≤n up i → L 0 (in, out, down i ))),

• G(in ∧ ⇓ → ( 1≤i≤n right i → L 0 (in, out , left i ))),

• G(in ∧ ⇓ → ( 1≤i≤n up i → L 1 (in, out, down i ))).

We write REC to denote the formula that states that colour 1 occurs infinitely often in the first column:

G F X(out ∧ ⇓) ∧ s∈Sides s 1 ∨ G F out ∧ ⇓ ∧ X s∈Sides s 1
The domino game Dom can pave N 2 with colour 1 occurring infinitely often on the first column if and only if PAVE∧SNAKE∧DIRECTION∧CONSTRAINTS ∧REC is satisfiable in PC[L 1 ].

Satisfiability for PC[L 1 ] is therefore Σ 1 1 -hard and is not recursively enumerable. The proof of Proposition 1.14 is inspired from the undecidability of propositional dynamic logic (PDL) augmented with the context-free language {a k 1 a 2 a k 1 | k ≥ 0} (see for example [23, chapter 9] for more details). For formal verification, the following result is more meaningful since it illustrates the strength of adding a single context-free language.

Corollary 1.15. The model-checking problem for PC[L 1 ] is undecidable.

Proof. It is indeed simple to reduce satisfiability for PC[L 1 ] to model-checking for PC[L 1 ]. Let ϕ be a formula built over the propositional variables p 1 , . . . , p n . We write M n = W, R, λ to denote the complete Kripke structure such that W = 2 {p1,...,pn} , R = W × W and λ is the identity. Then ϕ is valid if and only if for all s ∈ W , we have M n , s |= ∀ ϕ. Since PC[L 1 ] is closed under negations, by Proposition 1.14, the validity problem for PC[L 1 ] is also undecidable. Hence, the model-checking problem for PC[L 1 ] is undecidable. Surprisingly, a similar undecidability result holds for a specific context-free language that can be recognized by a visibly pushdown automaton (VPA) [START_REF] Alur | Visibly pushdown languages[END_REF] as shown below. For instance, L 1 cannot be recognized by a VPA. Let L 2 be the context-free language {a k 1 a 2 a k 3 a 4 | k ≥ 0} built over the alphabet Σ = {a 1 , . . . , a 4 }. This language can be easily defined by a VPA. A very nice feature of the class of VPA is that it defines context-free languages that are closed under Boolean operations. Moreover, PDL generalized to programs defined by VPA is still decidable [START_REF] Löding | Propositional dynamic logic with recursive programs[END_REF] (generalizing for instance [START_REF] Harel | More on nonregular PDL: Finite models and Fibonaccilike programs[END_REF]). Unlike this extension of PDL, we have the following undecidability results. Indeed, the temporal operator defined with the language L 2 can easily express the temporal operator defined with L 1 since L 1 (ϕ 1 , ϕ 2 , ϕ 3 ) ≡ L 2 (ϕ 1 , ϕ 2 , ϕ 1 , ϕ 3 ). By contrast, the characterization of decidable positive fragments of PC[CF] (without negation) is still open (the above undecidability proofs use negation in an essential way).

Concluding remarks

In this chapter, we have presented two distinct aspects of the use of automata theory for the verification of computer systems. A translation from LTL formulae into Büchi automata has been defined with the main advantage to produce simple automata for simple formulae. This follows the automata-based approach advocated in [START_REF] Vardi | Reasoning about infinite computations[END_REF] with simplicity and pedagogical requirements from [START_REF] Gerth | Simple on-the-fly automatic verification of linear temporal logic[END_REF][START_REF] Couvreur | On-the-fly verification of linear temporal logic[END_REF]. We believe that this is an adequate translation to be taught to students. The second use of automata is related to automata-based temporal operators generalizing the more standard temporal connectives such as the next operator or the until operator. After recalling the standard results about the operators defined from regular languages, we have explained how a restricted addition of operators defined from context-free languages can easily lead to undecidability. For instance, we show why model-checking for propositional calculus augmented with a simple CF language recognized by a VPA [START_REF] Alur | Visibly pushdown languages[END_REF]

Fig. 1 . 1 .

 11 Fig. 1.1. Two models undistinguishable for LTL.

ε-→

  denotes the one-step reduction relation, as usual, we write ε -→ * to denote the reflexive and transitive closure of ε -→. When ψ is a conjunction or a G formula then we introduce only one ε-transition Y ε -→ Y 1 and Y ≡ Y 1 . In the other cases, we introduce two ε-transitions Y

Fig. 1 . 6 .

 16 Fig. 1.6. Reduction of a state to reduced states

Lemma 1 . 3 .

 13 Let Z be a consistent and reduced set of formulae in NNF. Let u = a 0 a 1 a 2 • • • ∈ Σ ω and n ≥ 0. Then u, n |= Z if and only if u, n + 1 |= next(Z) and a n ∈ Σ Z . Using the equivalence Y ≡ Z∈Red(Y ) Z we prove now: Lemma 1.4. Let Y be a subset of formulae in NNF and let u ∈ Σ ω be an infinite word. If u |= Y then there is Z ∈ Red(Y ) such that u |= Z and for every

Fig. 1 . 8 .

 18 Fig. 1.8. GBA for nested until

Proposition 1 . 7 .

 17 [START_REF] Vardi | Nontraditional applications of automata theory[END_REF] Given a finite and total Kripke structure M, a state s in M and an LTL formula ϕ, it is possible to check in space polynomial in |ϕ|+log|M| whether M, s |= ∀ ϕ and M, s |= ∃ ϕ. Indeed, M, s |= ∀ ϕ holds if and only if L(A M,s ⊗ A ¬ϕ ) = ∅ where • A M,s is the obvious Büchi automaton of size O(|M|) such that L(A M,s ) = λPaths(M, s) (all states are accepting),

Fig. 1 . 11 .

 111 Fig. 1.11. The path in N 2

Corollary 1 . 16 .

 116 Satisfiability and model-checking for PC[L 2 ] are undecidable.

Table 1 .

 1 1. Reduction rules.

Table 1 .

 1

	1. At each step,

  we pass from downward to upward sequence").The only structure (built over {in, out , ⇑, ⇓}) satisfying SNAKE ∧ DIRECTION is{in, ⇓} • {out, ⇑} • {in, ⇑} 2 • {out, ⇓} • {in, ⇓} 3 • {out, ⇑} • {in, ⇑} 4 • • •

  is highly undecidable.

		Index
	ω-regular language, 28	complexity, 9, 22, 28, 29
		problem, 7, 9, 10
	automaton	monadic second-order logic MSO, 29
	Büchi automaton, 11	MSO, see monadic second-order logic
	finite-state automaton, 27
	generalized Büchi automaton, 12	past-time operator, 6
	transition-based acceptance, 12	path quantifier, 7
	visibly pushdown automaton, 3, 34	PDL, see propositional dynamic logic
		problem
	Büchi automaton, 11	model-checking, 7, 9, 10
	BA, see Büchi automaton	recurring domino, 31 satisfiability, 6
	computation tree logic CTL, 9, 10 CTL, see computation tree logic CTL * , 7, 25	universality, 30 validity, 6, 30 propositional dynamic logic PDL, 3
	domino game, 31	recurring domino problem, 31 renaming, 25
	ETL, see extended temporal logic extended temporal logic ETL, 27	satisfiability problem, 6
	GBA, see generalized Büchi automaton generalized Büchi automaton, 12	temporal logic, 3 CTL * , 7, 25 computation tree logic CTL, 9, 10
	Kripke structure, 6	extended temporal logic ETL, 27 linear-time temporal logic LTL, 5
	language	transition-based acceptance, 12
	ω-regular, 28 context-free, 29	universality problem, 30
	regular, 27 linear-time temporal logic LTL, 5 logic, see temporal logic monadic second-order logic MSO, 29	validity problem, 6 visibly pushdown automaton, 3, 34 VPA, see visibly pushdown automaton
	propositional dynamic logic PDL, 3
	LTL, see linear-time temporal logic
	modality, 3
	model-checking
	algorithm, 25

July 12, 2010 16:55 World Scientific Review Volume -9.75in x 6.5in demri-gastin-SI-bangalore-final

† ∀x ∈ W, ∃y ∈ W, x, y ∈ R.

World Scientific Review Volume -9.75in x 6.5in demri-gastin-SI-bangalore-final

* This work has been partially supported by projects ARCUS Île de France-Inde, ANR-06-SETIN-003 DOTS, and P2R MODISTE-COVER/Timed-DISCOVERI.

Proof. We show that the validity problem for PC [CF] is undecidable, which entails the undecidability of SAT(PC[CF]) since PC [CF] is closed under negations. We reduce the universality problem for context-free grammars (see e.g. the textbook [START_REF] Kozen | Automata and Computability[END_REF]) into the validity problem. Let G be a context-free grammar over the terminal alphabet Σ = {a 1 , . . . , a n }. We write G + to denote the CF grammar over the terminal alphabet

The letter a n+1 is simply an end marker. G + can be effectively computed from G.

Let UNI be the formula

The structures satisfying UNI are precisely those for which exactly one variable from p 1 , . . . , p n+1 holds at each state and, p n+1 holds at a unique state of the model. Hence, we characterize structures that can be naturally viewed as finite words, possibly in L(G + ). We show that

) is valid since every structure satisfying the formula UNI corresponds to a word in Σ * . Proposition 1.13 is interesting, but after all, it rests on the fact that PC[CF] can easily encode universality for context-free grammars. It would be more interesting to establish that undecidability still holds for a very small fragment of CF, which is the subject of the next section.

When a single context-free language leads to high undecidability

The main result of this section is the (high) undecidability of the model-checking problem for PC[L 1 ] for the context-free language L

The next operator X, the eventuality operator F and the temporal operator defined from L 0 are definable in PC[L 1 ] thanks to the following equivalences:

In the sequel, we therefore freely use these operators in PC[L 1 ] as well as the dual operator G. Proposition 1.14. Satisfiability for PC[L 1 ] is undecidable.