Linear-Time Temporal Logic and Büchi Automata^{∗}

Madhavan Mukund SPIC Mathematical Institute 92 G N Chetty Road Madras 600 017, India E-mail: madhavan@ssf.ernet.in

Abstract

Over the past two decades, temporal logic has become a very basic tool for specifying properties of reactive systems. For finite-state systems, it is possible to use techniques based on Büchi automata to verify if a system meets its specifications. This is done by synthesizing an automaton which generates all possible models of the given specification and then verifying if the given system refines this most general automaton. In these notes, we present a self-contained introduction to the basic techniques used for this automated verification. We also describe some recent spaceefficient techniques which work on-the-fly.

∗Tutorial talk, Winter School on Logic and Computer Science, Indian Statistical Institute, Calcutta, January 1997.

Introduction

Program verification is a fundamental area of study in computer science. The broad goal is to verify whether a program is “correct”—i.e., whether the implementation of a program meets its specification. This is, in general, too ambitious a goal and several assumptions have to be made in order to render the problem tractable. In these lectures, we will focus on the verification of finite-state reactive programs. For specifying properties of programs, we use linear time temporal logic.

What is a reactive program? The general pattern along which a conventional program executes is the following: it accepts an input, performs some computation, and yields an output. Thus, such a program can be viewed as an abstract function from an input domain to an output domain whose behaviour consists of a transformation from initial states to final states.

In contrast, a reactive program is not expected to terminate. As the name suggests, such systems “react” to their environment on a continuous basis, responding appropriately to each input. Examples of such systems include operating systems, schedulers, discrete-event controllers etc. (Often, reactive systems are complex distributed programs, so concurrency also has to be taken into account. We will not stress on this aspect in these lectures—we take the view that a run of a distributed system can be represented as a sequence, by arbitrarily interleaving concurrent actions.)

To specify the behaviour of a reactive system, we need a mechanism for talking about the way the system evolves along potentially infinite computations. Temporal logic [Pnu77] has become a well-established formalism for this purpose. Many varieties of temporal logic have been defined in the past twenty years—we focus on propositional linear time temporal logic (LTL).

There is an intimate connection between models of LTL formulas and languages of infinite words—the models of an LTL formula constitute an ω-regular language over an appropriate alphabet. As a result, the satisfiability problem for LTL reduces to checking for emptiness of ω-regular languages. This connection was first explicitly pointed out in [SVW87].

Later, in [VW86], the connection between LTL and ω-regular languages has been extended to model checking. Unlike the satisfiability problem, which asks if a given formula α has a model, the model-checking problem is one of verification: the task is to verify whether a given finite-state program P satisfies a specification α. This consists of checking that all runs of P constitute models for α. Since finite-state reactive programs can be represented quite naturally as Büchi automata, model-checking also reduces to a problem in automata theory. It suffices to show that no run of P is a model for ¬α, which is the same as checking that the intersection of the language accepted by P and the language defined by ¬α is empty.

In recent years, the techniques proposed in [VW86] have moved from the realm of theory to practice. In this context, there has been renewed emphasis on reducing the complexity of the automata-theoretic method. One fruitful approach is to build up the automaton associated with a formula “on-the-fly” so that only as much of the automaton is constructed as is needed to settle the model-checking problem. A first step in this regard is the algorithm proposed in [GPVW95].

This write-up is organized as follows. We begin with a description of the logical language LTL. We then provide a quick introduction to Büchi automata in Section 2. In Section 3 we describe the basic automata-theoretic approach of [VW86]. Next, in Section 4, we present a formal basis for the on-the-fly method of [GPVW95]. We conclude with some pointers to ways in which these approaches can be extended in more general settings.

1 Linear-time temporal logic

Linear time temporal logic is a logic for talking about infinite sequences, where each element in the sequence corresponds to a propositional world.

Syntax

We fix a countable set of atomic propositions P = {p_{0}, p_{1}, …}. Then Φ, the set of formulas of LTL, is defined inductively as follows:

• Every member of P belongs to Φ.

• If α and β are formulas in Φ, then so are ¬α, α ∨ β, Oα and α Uβ.

The connectives ¬ and ∨ correspond to the usual Boolean connectives “not” and “or” respectively. The modality O to be read as “next” while the binary modality U is to be read as “until”. Thus Oα is “next α” while α Uβ is “α until β”.

Semantics

A model is a function M : ℕ_{0} → 2^{P}. In other words, a model is an infinite sequence P_{0}P_{1} … of subsets of P. The function M describes how the truth of atomic propositions changes as time progresses.

We write M, i ⊧ α to denote that “α is true at time instant i in the model M”. This notion is defined inductively, according to the structure of α.

• M, i ⊧ p, where p ∈ P, iff p ∈ M(i).

• M, i ⊧ ¬α iff M, i |̸= α.

• M, i ⊧ α ∨ β iff M, i ⊧ α or M, i ⊧ β.

• M, i ⊧ Oα iff M, i+1 ⊧ α.

• M, i ⊧ α Uβ iff there exists k ≥ i such that M, k ⊧ β and for all j such that i ≤ j < k, M, j ⊧ α.

A formula α is said to be satisfiable if there exists a model M and an instant i such that M, i ⊧ α. Since the modalities we have defined only talk about future time-points within a model, it is not difficult to argue that a formula is satisfiable iff in some model it is satisfied at the initial point.

Proposition 1.1 Let α be a formula in Φ. Then α is satisfiable iff there exists a model M such that M, 0 ⊧ α.

Another simple observation is that in order to satisfy a formula α, a model needs to assign truth values only to those propositions which occur in α. Let Voc(α), the “vocabulary” of α, denote the subset of P which is mentioned in α. Voc(α) can be defined inductively quite easily:

• Voc(p) = {p}

• Voc(¬α) = Voc(α)

• Voc(α ∨ β) = Voc(α) ∪ Voc(β)

• Voc(Oα) = Voc(α)
• Voc(α Uβ) = Voc(α) ∪ Voc(β)

If M is a model and α is a formula, let M_{Voc(α)} be a new model where for all i ∈ ℕ_{0}, M_{Voc(α)}(i) = M(i) ∩ Voc(α). We then have the following simple fact.

Proposition 1.2 Let M be a model and α be a formula. Then, for all i ∈ ℕ_{0}, M, i ⊧ α iff M_{Voc(α)}, i ⊧ α.

Derived connectives

As usual, we introduce constants ⊤ and ⊥ representing “true” and “false”. We can write ⊤ as, for instance, p_{0} ∨ ¬p_{0} (recall that P = {p_{0}, p_{1}, …}) and ⊥ as ¬⊤.

We can also generate normal Boolean connectives like ∧ (“and”), ⇒ (“implies”) and ⇔ (“iff”) from the connectives ¬ and ∨ in the usual way—for instance, α ⇒ β = ¬α ∨ β.

We also introduce two derived modalities based on α Uβ. We write ◇α for ⊤ Uα and □α for ¬◇¬α. The modality ◇ is read as “eventually” while the modality □ is read as “henceforth”. Let M be a model. It is not difficult to verify the following facts:

• M, i ⊧ ◇α iff there exists k ≥ i such that M, k ⊧ α.

• M, i ⊧ □α iff for all k ≥ i, M, k ⊧ α.

Examples

Here are some examples of the kinds of assertions we can make in temporal logic.

• The formula ◇□α says that α is eventually a “stable property” of the system— M, i ⊧ ◇□α iff for some j ≥ i, for all k ≥ j, M, k ⊧ α.

• On the other hand, □◇β asserts that β holds infinitely often.

• If we use the full power of U, we can make some fairly complex statements about a program’s behaviour. For instance, consider a system which schedules access to a shared resource among k competing processes which are named, for convenience, 1, 2, …, k. For each process i, we could have two atomic propositions r_{i} and g_{i} to denote the state of i vis-a-vis the shared resource—proposition r_{i} is true if process i has requested the resource but has not yet got access to it, while g_{i} is true when i is granted access to the resource.

The formula r_{i} Ug_{i} asserts that process i continues to be in a requesting state until access to the resource is granted. A desirable property that the system should satisfy is that for all i, the formula □(r_{i} ⇒ (r_{i} Ug_{i})) is true at the initial state—i.e., the scheduler eventually grants every request.

For a detailed exposition of how to specify properties of reactive systems in temporal logic, the reader is referred to the book [MP91].

2 Büchi automata

Automata on infinite inputs were introduced by Büchi in [Bü60]. A Büchi automaton is a non-deterministic finite-state automaton which takes infinite words as input. A word is accepted if the automaton goes through some designated “good” states infinitely often while reading it.

We begin with some notation for infinite words. Let Σ be a finite alphabet. An infinite word α ∈ Σ^{ω} is an infinite sequence of symbols from Σ. We shall represent α as a function α : ℕ_{0} → Σ, where ℕ_{0} is the set {0, 1, 2, …} of natural numbers. Thus, α(i) denotes the letter occurring at the i^{th} position.

In general, if S is a set and σ an infinite sequence of symbols over S—in other words, σ : ℕ_{0} → S—then inf(σ) denotes the set of symbols from S which occur infinitely often in σ. Formally, inf(σ) = {s ∈ S | ∃^{ω}n ∈ ℕ_{0} : σ(n) = s}, where ∃^{ω} denotes the quantifier “there exist infinitely many”.

Automata An automaton is a triple A = (S, →, S_{in}) where S is a set of states, S_{in} ⊆ S is a set of initial states and → ⊆ S × Σ × S is a transition relation. Normally, we write s ⟶^{a} s′ to denote that (s, a, s′) ∈ →.

The automaton is said to be deterministic if S_{in} is a singleton and → is a function from S ×Σ to S. The automata we encounter in this paper will, in general, be non-deterministic.

Runs Let A = (S, →, S_{in}) be an automaton and α : ℕ_{0} → Σ an input word. A run of A on α is a infinite sequence ρ : ℕ_{0} → S such that ρ(0) ∈ S_{in} and for all i ∈ ℕ_{0},

ρ(i) ⟶^{α(i)} ρ(i+1).

Figure 1: A typical accepting run of a Büchi automaton, with s ∈ S_{in} and g ∈ G.

So, a run is just a “legal” sequence of states that an automaton can pass through while reading the input. In general, an input may admit many runs because of nondeterminism. Since a non-deterministic automaton may have states where there are no outgoing transitions corresponding to certain input letters, it is also possible that an input admits no runs—in this case, every potential run leads to a state from where there is no outgoing transition enabled for the next input letter. If the automaton is deterministic, each input admits precisely one run.

Büchi automata A Büchi automaton is a pair (A, G) where A = (S, →, S_{in}) and G ⊆ S. G denotes a set of good states. The automaton (A, G) accepts an input α : ℕ_{0} → Σ if there is a run ρ of A on α such that inf(ρ) ∩ G ≠ ∅. The language recognized by (A, G), L(A, G), is the set of all infinite words accepted by (A, G). A set L ⊆ Σ^{ω} is said to be Büchi-recognizable if there is a Büchi automaton (A, G) such that L = L(A, G).

According to the definition, a Büchi automaton accepts an input if there is a run along which some subset of G occurs infinitely often. Since G is a finite set, it is easy to see that there must actually be a state g ∈ G which occurs infinitely often along σ. In other words, if we regard the state space of a Büchi automaton as a graph, an accepting run traces an infinite path which starts at some state s in S_{in}, reaches a good state g ∈ G and, thereafter, keeps looping back to g infinitely often (see Figure 1).

Example 2.1 Consider the alphabet Σ = {a, b}. Let L ⊆ Σ^{ω} consist of all infinite words α such that there are infinitely many occurrences of a in α. Figure 2 shows a Büchi automaton recognizing L. The initial state is marked by an unlabelled incoming arrow. There is only one good state, which is indicated with a double circle. In this automaton, all transitions labelled a lead into the good state and, conversely, all transitions coming into the good state are labelled a. From this, it follows that the automaton accepts an infinite word iff it has infinitely many occurrences of a.

The complement of L, which we denote \overline{L}, is the set of all infinite words α such that α has only finitely many occurrences of a. An automaton recognizing \overline{L} is shown in Figure 3. The automaton guesses a point in the input beyond which it will see no more a’s—such a point must exist in any input with only a finite number of a’s. Once it has made this guess, it can process only b’s—there is no transition labelled a from the second state—so if it reads any more a’s it gets stuck.

□

Figure 2: A Büchi automaton for L (Example 2.1)

Figure 3: A Büchi automaton for \overline{L} (Example 2.1)

In the example, notice that the automaton recognizing L is deterministic while the automaton for \overline{L} is non-deterministic. It can be shown that the non-determinism in the second case is unavoidable—that is, there is no deterministic automaton recognizing \overline{L}. This means that Büchi automata are fundamentally different from their counterparts on finite inputs: we know that over finite words, deterministic automata are as powerful as non-deterministic automata.

2.1 Constructions on Büchi automata

It turns out that the class of Büchi-recognizable languages is closed under boolean operations.

Union To show closure under finite union, let (A_{1}, G_{1}) and (A_{2}, G_{2}) be two Büchi automata. To construct an automaton (A, G) such that L(A, G) = L(A_{1}, G_{1}) ∪ L(A_{2}, G_{2}), we take A to be the disjoint union of A_{1} and A_{2}. Since we are permitted to have a set of initial states in A, we retain the initial states from both copies. If a run of A starts in an initial state contributed by A_{1}, it will never cross over into the state space contributed by A_{2} and vice versa. Thus, we can set the good states of A to be the union of the good states contributed by both components.

Complementation Showing that Büchi-recognizable languages are closed under complementation is highly non-trivial. One problem is that we cannot determinize Büchi automata. Even if we could work with deterministic automata, the formulation of Büchi acceptance is not symmetric with respect to complementation in the following sense. Suppose (A, G) is a deterministic Büchi automaton and α is an infinite word which does not belong to L(A, G). Then, the (unique) run ρ_{α} of A on α is such that inf(ρ_{α}) ∩ G = ∅. Let \overline{G} denote the complement of G. It follows that inf(ρ_{α}) ∩ \overline{G} ≠ ∅, since some state must occur infinitely often in ρ_{α}. It would be tempting to believe that the automaton (A, \overline{G}) recognizes Σ^{ω} − L(A, G). However, there may be words which admit runs which visit both G and \overline{G} infinitely often. These words will be including both in L(A, \overline{G}) as well as in L(A, G). So, there is no convenient way to express the complement of a Büchi condition again as a Büchi condition. Fortunately, we shall not need to complement Büchi automata for any of the constructions which we describe here.

Intersection Turning to intersection, the natural way to intersect automata A_{1} and A_{2} is to construct an automaton whose state space is the cross product of the state spaces of A_{1} and A_{2} and let both copies process the input simultaneously. For finite words, the input is accepted if each copy can generate a run which reaches a final state at the end of the word.

For infinite inputs, we have to do a more sophisticated product construction. An infinite input α should be accepted by the product system provided both copies generate runs which visit good states infinitely often. Unfortunately, there is no guarantee that these runs will ever visit good states simultaneously—for instance, it could be that the first run goes through a good state after α(0), α(2), … while the second run enters good states after α(1), α(3), … So, the main question is one of identifying the good states of the product system.

The key observation is that to detect that both components of the product visit good states infinitely often, one need not record every point where the copies visit good states; in each copy, it suffices to observe an infinite subsequence of the overall sequence of good states. So, we begin by focusing on the first copy and waiting for its run to enter a good state. When this happens, we switch attention to the other copy and wait for a good state there. Once the second copy reaches a good state, we switch back to the first copy and so on. Clearly, we will switch back and forth infinitely often iff both copies visit their respective good states infinitely often. Thus, we can characterize the good states of the product in terms of the states where one switches back and forth.

Formally, the construction is as follows. Let (A_{1}, G_{1}) and (A_{2}, G_{2}) be two Büchi automata such that A_{i} = (S_{i}, →_{i}, S_{in}^{i}) for i = 1, 2. Define (A, G), where A = (S, →, S_{in}), as follows:

• S = S_{1} × S_{2} × {1, 2}

• The transition relation → is defined as follows:

(s_{1}, s_{2}, 1) ⟶^{a} (s′_{1}, s′_{2}, 1) if s_{1} ⟶^{a}_{1} s′_{1}, s_{2} ⟶^{a}_{2} s′_{2} and s_{1} ∉ G_{1}.

(s_{1}, s_{2}, 1) ⟶^{a} (s′_{1}, s′_{2}, 2) if s_{1} ⟶^{a}_{1} s′_{1}, s_{2} ⟶^{a}_{2} s′_{2} and s_{1} ∈ G_{1}.

(s_{1}, s_{2}, 2) ⟶^{a} (s′_{1}, s′_{2}, 2) if s_{1} ⟶^{a}_{1} s′_{1}, s_{2} ⟶^{a}_{2} s′_{2} and s_{2} ∉ G_{2}.

(s_{1}, s_{2}, 2) ⟶^{a} (s′_{1}, s′_{2}, 1) if s_{1} ⟶^{a}_{1} s′_{1}, s_{2} ⟶^{a}_{2} s′_{2} and s_{2} ∈ G_{2}.

• S_{in} = {(s_{1}, s_{2}, 1) | s_{1} ∈ S_{in}^{1} and s_{2} ∈ S_{in}^{2}}

• G = S_{1} × G_{2} × {2}.

In the automaton A, each product state carries an extra tag indicating whether the automaton is checking for a good state on the first or the second component. The automaton accepts if it switches focus from the second component to the first infinitely often. (Notice that we could equivalently have defined G to be the set G_{1} × S_{2} × {1}.) It is not difficult to verify that L(A, G) = L(A_{1}, G_{1}) ∩ L(A_{2}, G_{2}).

Emptiness In applications, we will need to be able to check whether the language accepted by a Büchi automaton is empty. To do this, we recall our observation that any accepting run of a Büchi automaton must begin in an initial state, reach a final state g and then cycle back to g infinitely often.

If we ignore the labels on the transitions, we can regard the state space of a Büchi automaton (A, G) as a directed graph G_{A} = (V_{A}, E_{A}) where V_{A} = S and (s, s′) ∈ E_{A} iff for some a ∈ Σ, s ⟶^{a} s′. Recall that a set of vertices X in a directed graph is a strongly connected component iff for every pair of vertices v, v′ ∈ X, there is a path from v to v′. Clearly, L(A, G) is non-empty iff there is a strongly connected component X in G_{A} such that X contains a vertex g from G and X is reachable from one of the initial states. We thus have the following theorem.

Theorem 2.2 The emptiness problem for Büchi automata is decidable.

Notice that it is sufficient to analyze maximal strongly connected components in G_{A} in order to check that L(A, G) ≠ ∅. Computing the maximal strongly connected components of a directed graph can be done in time linear in the size of the graph [AHU74], where the size of a graph G = (V, E) is, as usual, given by |V | + |E|. Checking reachability can also be done in linear time. So, if A has n states, checking that L(A, G) ≠ ∅ can be done in time O(n^{2}).

2.2 Generalized Büchi automata

When expressing the connection between temporal logic and Büchi automata, it is often convenient to work with a slightly more elaborate acceptance condition. A generalized Büchi automaton is a structure (A, G_{1}, G_{2}, …, G_{k}), where A = (S, →, S_{in}) and for all i ∈ {1, 2, …, k}, G_{i} ⊆ S.

An input α is accepted by the automaton (A, G_{1}, G_{2}, …, G_{k}) if there is a run ρ of A on α such that inf(ρ) ∩ G_{i} ≠ ∅ for all i ∈ {1, 2, …, k}. As usual, L(A, G_{1}, G_{2}, …, G_{k}) denotes the language of all infinite words accepted by the automaton (A, G_{1}, G_{2}, …, G_{k}). The following observation is immediate.

Proposition 2.3 Let (A, G_{1}, G_{2}, …, G_{k}) be a generalized Büchi automaton. Then

L(A, G_{1}, G_{2}, …, G_{k}) = ⋂_{i∈{1,2,...,k}} L(A, G_{i}).

In other words, every language which is recognized by a generalized Büchi automaton is also Büchi recognizable. It is not difficult to argue that checking whether the language accepted by a generalized Büchi automaton is empty is no harder, in terms of computational complexity, than the corresponding check for a normal Büchi automaton.

Further reading

The languages recognized by Büchi automata correspond to ω-regular languges. These languages have a syntactic characterization in terms of regular languages of finite strings. They can also be characterized logically using the monadic second order theory of one successor (S1S). For a more detailed introduction to the theory of automata on infinite words, the reader is encouraged to consult the excellent surveys by Thomas [Th90, Th96].

3 Automata-theoretic methods

As we saw in the last section, a model for an LTL formula α is a function M : ℕ_{0} → 2^{P}. We also saw that to check whether α is satisfiable, it suffices to look at models defined over Voc(α). In other words, we can restrict our attention to models of the form P_{0}P_{1} … where each P_{i} is a subset of Voc(α). Since Voc(α) is finite, we can treat each model as an infinite word over the finite alphabet 2^{Voc(α)}.

The result we shall establish is that the set of all infinite words over 2^{Voc(α)} which are models for α—i.e., the set

Mod(α) = {M = P_{0}P_{1} … | M, 0 ⊧ α}

actually constitutes a Büchi recognizable language. We shall also demonstrate how to explicit construct a generalized Büchi automaton (A_{α}, G_{1}, G_{2}, …, G_{k}) over the alphabet 2^{Voc(α)} such that L(A_{α}, G_{1}, G_{2}, …, G_{k}) = Mod(α).

3.1 Satisfiability

We begin by defining the (Fischer-Ladner) closure of a formula.

Closure Let α be an LTL formula. Then CL′(α) is the smallest set of formulas such that:

• α ∈ CL′(α).

• If ¬β ∈ CL′(α), then β ∈ CL′(α).

M Mukund: LTL and Büchi Automata  10

• If β ∨ γ ∈ CL′(α), then β, γ ∈ CL′(α).

• If Oβ ∈ CL′(α), then β ∈ CL′(α).

• If β Uγ ∈ CL′(α), then β, γ, O(β Uγ) ∈ CL′(α). Finally, CL(α) = CL′(α) ∪ {¬β | β ∈ CL′(α)}, where we identify ¬¬β with β.

Notice that CL(α) is always finite, even though the clause for β Uγ throws in a larger formula into the set. In fact, if α contains n symbols, then |CL(α)| is O(n).

The automaton A_{α} that we associate with a formula α will have as its states subsets of CL(α) which are both propositionally and temporally “consistent”. These subsets are called atoms. Atoms Let α be a formula. Then A ⊆ CL(α) is an atom if:

• ∀β ∈ CL(α), β ∈ A iff ¬β ∉ A.

• ∀β ∨ γ ∈ CL(α), β ∨ γ ∈ A iff β ∈ A or γ ∈ A.

• ∀β Uγ ∈ CL(α), β Uγ ∈ A iff γ ∈ A or β, O(β Uγ) ∈ A. Let AT be the set of all atoms of α. Constructing a Büchi automaton for α We first construct an automaton A_{α} = (S, →, S_{in}) over the alphabet 2^{Voc(α)}, where:

• S = AT

• Let A, B ∈ AT and P ⊆ Voc(α). Then A ⟶^{P} B iff the following hold.

– P = A ∩ Voc(α).

– For all Oβ ∈ CL(α), Oβ ∈ A iff β ∈ B.

• S_{in} = {A ∈ AT | α ∈ A}. Let {β_{1} Uγ_{1}, β_{2} Uγ_{2}, …, β_{k} Uγ_{k}} be the set of until formulas which appear in CL(α). We add a generalized Büchi acceptance condition (G_{1}, G_{2}, …, G_{k}) where for each i,

G_{i} = {A ∈ AT | β_{i} Uγ_{i} ∉ A or γ_{i} ∈ A}.

We then have the following theorem. Theorem 3.1 Let M be an infinite word over 2^{Voc(α)}. Then

M ∈ L(A_{α}, G_{1}, G_{2}, …, G_{k}) iff M, 0 ⊧ α

Winter School on Logic & Computer Science  ISI Calcutta, Dec 1996–Jan 1997

Proof (⇒) Let M = P_{0}P_{1} … be an infinite word over Voc(α) which is accepted by (A_{α}, G_{1}, G_{2}, …, G_{k}). Let A_{0}A_{1} … be an accepting run of A_{α} on M. For all β ∈ CL(α) and for all i ∈ ℕ_{0}, we show that M, i ⊧ β iff β ∈ A_{i}.

The proof is by induction on the structure of β.

(β = p ∈ P)

Then M, i ⊧ p iff p ∈ P_{i} iff p ∈ A_{i}.

(β = ¬γ)

Then M, i ⊧ β iff M, i |̸= γ iff (by the induction hypothesis) γ ∉ A_{i} iff β ∈ A_{i} (by the definition of an atom).

(β = γ ∨ δ)

Then M, i ⊧ β iff (M, i ⊧ γ or M, i ⊧ δ) iff—by the induction hypothesis—(γ ∈ A_{i} or δ ∈ A_{i}) iff—by the definition of an atom—γ ∨ δ ∈ A_{i}.

(β = Oγ)

Then M, i ⊧ β iff M, i+1 ⊧ γ iff (by the induction hypothesis) γ ∈ A_{i+1} iff (by the

definition of A_{i} ⟶^{P_{i}} A_{i+1}) Oγ = β ∈ A_{i}.

(β = γ Uδ)

Suppose that M, i ⊧ β. We must show that β ∈ A_{i}. By the semantics of the modality U, there exists k ≥ i such that M, k ⊧ δ and for all j, i ≤ j < k, M, j ⊧ γ. We show that β ∈ A_{i} by a second induction on k − i.

Base case: (k − i = 0)

Then k = i and M, i ⊧ δ. By the main induction hypothesis, δ ∈ A_{i}, whence, from the definition of atoms, γ Uδ = β ∈ A_{i}.

Induction step: (k − i = ℓ > 0)

By the semantics of the modality U, M, i ⊧ γ and M, i+1 ⊧ γ Uδ. Then, by the secondary induction hypothesis, γ Uδ ∈ A_{i+1}. From the definition of A_{i} ⟶^{P_{i}} A_{i+1}, we then have O(γ Uδ) ∈ A_{i} (recall that if γ Uδ ∈ CL(α) then O(γ Uδ) ∈ CL(α) as well). By the main induction hypothesis, we also have γ ∈ A_{i}. Combining these facts, from the definition of an atom, γ Uδ = β ∈ A_{i}.

Conversely, suppose β ∈ A_{i}. We must show that M, i ⊧ β. Recall that we have indexed the until formulas in CL(α) by 1, 2, …, k. Let m be the index of β.

Since A_{0}A_{1} … is an accepting run of (A_{α}, G_{1}, G_{2}, …, G_{k}), there must exist a k ≥ i such that A_{k} ∈ G_{m}. Choose the least such k. Once again, we do a second induction on k − i to show that M, i ⊧ β.

Base case: (k − i = 0)

If k = i, then A_{i} ∈ G_{m}. Since γ Uδ ∈ A_{i}, the only way for A_{i} to be in G_{m} is for δ to also belong to A_{i}. Then, by the main induction hypothesis, M, i ⊧ δ, whereby M, i ⊧ γ Uδ as well.

Induction step: (k − i = ℓ > 0)

Since A_{i} ∉ G_{m}, δ ∉ A_{i}. From the definition of atoms, both γ and O(γ Uδ) must be in A_{i}. Since A_{i} ⟶^{P_{i}} A_{i+1}, it must be the case that and γ Uδ ∈ A_{i+1}. By the secondary induction hypothesis, M, i+1 ⊧ γ Uδ while by the main induction hypothesis M, i ⊧ γ. From the semantics of the modality U, it then follows that M, i ⊧ γ Uδ as well.

(⇐) Suppose that M = P_{0}P_{1} … such that M, 0 ⊧ α. We have to show that M ∈ L(A_{α}, G_{1}, G_{2}, …, G_{k}). In other words, we have to exhibit an accepting run of the automaton on M.

For i ∈ ℕ_{0}, define A_{i} to be the set {β ∈ CL(α) | M, i ⊧ α}. It is easy to verify that each A_{i} is an atom. We can also verify that each adjacent pair of atoms A_{i} and A_{i+1} satisfy the conditions specified for the existence of an arrow A_{i} ⟶^{P_{i}} A_{i+1}. Finally, since M, 0 ⊧ α, we have α ∈ A_{0}, so A_{0} is an initial state in A_{α}. From all this, it follows that A_{0}A_{1} … is a run of the automaton on M.

To check that it is an accepting run, we have to verify that each good set G_{m} is met infinitely often. Suppose this is not the case—i.e., for some G_{m} and some index k ∈ ℕ_{0}, for all j ≥ k, A_{j} ∉ G_{m}. In other words, for all j ≥ k, the m^{th} until formula in CL(α), γ_{m} Uδ_{m}, belongs to A_{j} and δ_{m} ∉ A_{j}. Since A_{k} = {β ∈ CL(α) | M, k ⊧ β}, it follows that M, k ⊧ γ_{m} Uδ_{m}. But, since δ_{m} ∉ A_{j} for all j ≥ k, it follows that M, j ⊧ ¬δ_{m} for all j ≥ k, which contradicts the fact that M, k ⊧ γ_{m} Uδ_{m}. □

It follows from the preceding theorem that α is satisfiable iff the language recognized by (A_{α}, G_{1}, G_{2}, …, G_{k}) is non-empty. Let the length of α be n. Since the size of CL(α) is linear in n, it follows that the number of states in A_{α} is bounded by 2^{O(n)}. Since checking for non-emptiness can be done in time (2^{O(n)})^{2} = 2^{O(n)}, the satisifiability problem for a formula of length n is solvable in time 2^{O(n)}.

3.2 Model checking

Let us model finite-state reactive programs as (generalized) Büchi automata—a program is a structure P = ((S, →, S_{in}), G_{1}, G_{2}, …, G_{k}). The acceptance condition may trivial—i.e., we could have k = 1 and G_{1} = S.

We use atomic propositions to characterize properties satisified by the states of the program. In other words, a program P comes with a function V : S → P which describes the properties of each state.

Each run of P generates a model in the obvious way. Let ρ = s_{0}s_{1} … be a run of P —in other words, s_{0} ∈ S_{in} and for all i ∈ ℕ_{0}, s_{i} ⟶^{a} s_{i+1}. This induces a model M_{ρ} : ℕ_{0} → P given by M_{ρ}(i) = V (ρ(i)) for all i ∈ ℕ_{0}.

The model-checking problem is the following: given a program P and a valuation V together with a specification α, does every run of P satisfy α? In other words, we want to check that the set Mod(P) = {M_{ρ} | ρ is a run of P } is a subset of Mod(α), the set of models of α. This is equivalent to saying that Mod(P) does not contain any model of ¬α.

To check this, we first construct an automaton (A_{P} , G_{1}, G_{2}, …, G_{k}) from (P, V) over the alphabet 2^{Voc(α)} as follows. Let P = ((S, →, S_{in}), G_{1}, G_{2}, …, G_{k}). Then A_{P} = (S_{P} , →_{P} , S_{in}^{P}), where

• S_{P} = S

• →_{P} = {(s, Q, s′) | ∃a. s ⟶^{a} s′ and Q = V (s) ∩ Voc(α)}.

• S_{in}^{P} = S_{in}.

The following is then obvious:

Theorem 3.2 Let (P, V) be a program and α be a formula. Then all models generated by P satisfy α iff L(A_{P}) ∩ L(A_{¬α}) = ∅.

Recall that intersecting two Büchi automata is just a simple extension of the product construction. From this it follows that the complexity of settling the model checking problem is O(m 2^{O(n)}), where m is the the number of states in A_{P} and n is the length of α.

4 On-the-fly methods

The construction described in the previous section requires us to construct the entire automaton A_{¬α} in order to solve the model-checking problem. In particular, the emptiness check at the end of the procedure assumes that the entire automaton is available in memory in order to search for an accepting run.

A simple way to get around this memory requirement is to explore the state space in an incremental fashion. For instance, in [CVWY92], a depth-first-search (DFS) based strategy is used to detect cycles and hence check for emptiness, rather than looking for strongly connected components directly in the full automaton graph.

Such a strategy can be implemented along with an “on-the-fly” construction of the automaton—when constructing the product of the program automaton and the formula automaton, we generate the states of the product incrementally, as and when they are explored by the DFS-based cycle-detection strategy. In the process, if we find an accepting cycle, we can abort the search without generating the entire state space. Of course, in the worst case (which occurs when the program does meet the specification given the formula!), we end up having to explore the entire state space.

To generate the product state space on the fly, we have to first have a method for constructing both the program automaton and formula automaton on-the-fly, individually.

In many applications, the program to be verified is a concurrent system specified in terms of its components. In order to apply the technique discussed in the previous section, we have to generate the global state space of the concurrent program. The obvious on-the-fly approach is to generate these global states as and when the need arises.

More tricky is to find an on-the-fly approach for generating the formula automaton. A procedure for achieving this is described in [GPVW95]. However, the construction presented in [GPVW95] is fairly opaque thanks to the fact that it blurs the distinction between the basic strategy used for on-the-fly generation and some specific optimizations which improve the overall performance.

Here, we present the basis a technically cleaner version of the [GPVW95] algorithm (which is admittedly less efficient overall). However, by separately applying optimizations to our construction, we can improve the complexity bounds. The construction described here is from [DSz96].

Now and next-state requirements

Though LTL formulas are intepreted on infinite runs, the definition of the satisfaction relation for LTL gives rise to what may be called a “two-state” semantics. Every LTL formula α can be thought of as specifying two sets of requirements: one set to be satisfied “now” and the rest to be satisfied in the “next state”. For instance, the formula α Uβ says that either β is true now, or α is true now and α Uβ is true in the next state.

By repeatedly breaking down a formula, we can put it in a sort of disjunctive normal form, which specifies all possible ways of making the formula true. For instance, the formula p ∧ (q Ur) breaks down into two sets of requirements, {p, q, O(q Ur)} and {p, r}. If either of these sets is true, the original formula is true. Notice that each of these sets internally breaks up into current requirements (e.g., p, q in the first set) and next-state requirements (O(q Ur) in the first set).

We would like to formalize this notion: a formula will generate an automaton whose states are sets like the ones above. Each set represents one way of making some requirement true. A state t is a valid next state for a state s if it is one of the ways of satisfying the next-state formulas in s.

Positive formulas

We modify the syntax of LTL so that all negations appear only at the level of atomic propositions. Formally, we begin with a set of atomic propositions P, together with predefined constants ⊤ and ⊥. Let \overline{P} denote the set \{¬p | p ∈ P\}. Then Φ^{+}, the set of LTL formulas in positive form, is defined inductively as follows:

• ⊤ and ⊥ belong to Φ^{+}.

• Every member of P and \overline{P} belongs to Φ^{+}.

• If α and β are formulas in Φ^{+}, then so are α ∨ β, α ∧ β, Oα, α Uβ and αVβ.

The semantics is ∨, ∧, O and U is as before. The formula αVβ is an abbreviation for ¬(¬α U¬β). It is easy to check that

• M, i ⊧ αVβ iff either for all k ≥ i, M, k ⊧ β or there is a j ≥ i such that M, j ⊧ α and for all ℓ, i ≤ ℓ ≤ j, M, ℓ ⊧ β.

Notice that any LTL formula can be converted into a positive formula by pushing all negations inwards to the level of atomic propositions. The resulting formula may be longer, but is still linear in the size of the original formula. Henceforth, we assume that all formulas we encounter are from Φ^{+}.

For a set of formulas X, let next(X) = {Oα | Oα ∈ X} and snext(X) = {α | Oα ∈ X}. In other words, snext(X) consists of all O-formulas in X stripped of the O modality. We use ⋀ X to denote the conjunction of formulas in X and ⋁ X to denote the disjunction of formulas in X. We adopt the convention that ⋀ ∅ = ⊤ and ⋁ ∅ = ⊥.

Disjunctive normal form To formalize the notion of breaking down a formula into all possible ways of satisfying it, we introduce a version of disjunctive normal form.

Let

dnf : Φ^{+} → Sets of subsets of P ∪ \overline{P} ∪ next(Φ^{+})

be given by:

dnf(⊤)  = {∅}
dnf(⊥)  = ∅
dnf(x)  = {{x}}, for x = p, ¬p, Oα
dnf(α ∨ β) = dnf(α) ∪ dnf(β)
dnf(α ∧ β) = {C ∪ D | C ∈ dnf(α), D ∈ dnf(β), C ∪ D is propositionally consistent}
dnf(α Uβ) = dnf(α ∧ O(α Uβ)) ∪ dnf(β)
dnf(αVβ) = dnf(α ∧ β) ∪ dnf(β ∧ O(αVβ))

Thus the function dnf breaks up a formula into a set of sets of formulas. Each lower level set represents a clause in an extended version of disjunctive normal form, where propositions, their negations and next formulas are treated as literals. The modalities U and V are interpreted as disjunctions over their “two-state semantics”.

We can prove the following by induction on the structure of formulas.

Lemma 4.1 For all formulas α ∈ Φ^{+},

α ⇔ ⋁_{X∈dnf(α)}(⋀ X)

Let us fix a formula α ∈ Φ^{+}. We extend the notion of CL(α) to cover the new modality V in the obvious way: if βVγ ∈ CL(α), then β, γ ∈ CL(α).

In our on-the-fly construction, we will not work with fully specified atoms. Instead, we normally work with “unsaturated” subsets X ⊆ CL(α). For such a subset X, we define consq(X), the logical consequences of X as follows.

Let X ⊆ CL(α). Then consq(X) is the smallest subset of CL(α) such that:

• X ⊆ consq(X)

• If ⊤ ∈ CL(α) then ⊤ ∈ consq(X).

• For all β ∨ γ ∈ CL(α), if β ∈ consq(X) or γ ∈ consq(X) then β ∨ γ ∈ consq(X).

• For all β ∧ γ ∈ CL(α), if β, γ ∈ consq(X) then β ∧ γ ∈ consq(X).

• For all β Uγ ∈ CL(α), if β, O(β Uγ) ∈ consq(X) or γ ∈ consq(X) then β Uγ ∈ consq(X).

• For all βVγ ∈ CL(α), if β, γ ∈ consq(X) or β, O(βVγ) ∈ consq(X) then βVγ ∈

consq(X). The following properties of consq are not difficult to prove. Lemma 4.2 Let β ∈ CL(α) and X, Y ⊆ CL(α). Then

(i) If X ⊆ Y then consq(X) ⊆ consq(Y). (ii) If X ∈ dnf(β) then β ∈ consq(X). (iii) If β ∈ X and Y ∈ dnf(⋀ X), then β ∈ consq(Y). (iv) Let M = P_{O}P_{1} … be a model. If M, 0 ⊧ ⋀ X then M, 0 ⊧ ⋀ consq(X). We can now define a generalized Büchi automaton corresponding to a formula α. The automaton A_{α} = (S, →, S_{in}) over 2^{Voc(α)} is given by:

• S = Subsets of P ∪ \overline{P} ∪ next(CL(α)).

• S_{in} = dnf(α).

• X ⟶^{P} Y iff the following are true:

– X ∩ P ⊆ P.

– {p | ¬p ∈ X} ∩ P = ∅.

– Y ∈ dnf(⋀ snext(X)). Notice that we could now have many different arrows X ⟶^{P} Y between a pair of states X and Y, since X and Y are no longer atoms. In general, a P labelled-arrow exists provided P does not contradict the propositional assertions in X.

As before let {β_{1} Uγ_{1}, β_{2} Uγ_{2}, …, β_{k} Uγ_{k}} be the set of until formulas which appear in CL(α). We add a generalized Büchi acceptance condition (G_{1}, G_{2}, …, G_{k}) where for each i, G_{i} = {X ∈ S | β_{i} Uγ_{i} ∉ consq(X) or γ_{i} ∈ consq(X)}.

We want to show that M = P_{0}P_{1} … is accepted by (A_{α}, G_{1}, G_{2}, …, G_{k}) iff M, 0 ⊧ α. We break the proof up into two parts.

Winter School on Logic & Computer Science  ISI Calcutta, Dec 1996–Jan 1997

Soundness

Let M = P_{0}P_{1} … be accepted by (A_{α}, G_{1}, G_{2}, …, G_{k}). We need to show that M, 0 ⊧ α. Let X_{0}X_{1} … be an accepting run for M. We show the following:

Lemma 4.3 ∀β ∈ CL(α), ∀i ∈ ℕ_{0}, if β ∈ consq(X_{i}) then M, i ⊧ β.

Proof By induction on the structure of β.

(β = p ∈ P)

If p ∈ consq(X_{i}) then p ∈ X_{i} which implies that p ∈ P_{i} which implies that M, i ⊧ p.

(β = ¬p, p ∈ P)

If ¬p ∈ consq(X_{i}) then ¬p ∈ X_{i} which implies that p ∉ P_{i} which implies that M, i ⊧ ¬p.

(β = γ ∨ δ)

Since X_{i} consists of formulas from P ∪ \overline{P} ∪ next(Φ^{+}), it cannot be the case that γ ∨ δ ∈ X_{i}. Thus, we must have derived the fact that γ ∨ δ ∈ consq(X_{i}) using our inductive definition of consq(X_{i}). From this, it follows that either γ ∈ consq(X_{i}) or δ ∈ consq(X_{i}). By the induction hypothesis, either M, i ⊧ γ or M, i ⊧ δ, so M, i ⊧ γ ∨ δ.

(β = γ ∧ δ)

Once again, it cannot be the case that γ∧δ ∈ X_{i}. From the fact that γ∧δ ∈ consq(X_{i}), it follows that γ ∈ consq(X_{i}) and δ ∈ consq(X_{i}). By the induction hypothesis, M, i ⊧ γ and M, i ⊧ δ, so M, i ⊧ γ ∧ δ.

(β = Oγ)

If Oγ ∈ consq(X_{i}) then Oγ ∈ X_{i}. So γ ∈ snext(X_{i}). Since X_{i+1} ∈ dnf(snext(X_{i})), it follows from Lemma 4.2 (ii) that γ ∈ consq(X_{i+1}). By the induction hypothesis, M, i+1 ⊧ γ, so M, i ⊧ Oγ.

(β = γ Uδ)

In general if X ⟶^{P} Y and γ Uδ ∈ consq(X), then either δ ∈ consq(X) or γ ∈ consq(X) and γ Uδ ∈ consq(Y). So, if γ Uδ ∈ consq(X_{i}), it follows either that for all k ≥ i, γ Uδ ∈ consq(X_{k}) and δ ∉ consq(X_{k}) or that there exists k ≥ i such that δ ∈ consq(X_{k}) and for all j such that i ≤ j < k, γ ∈ consq(X_{j}).

The first case is ruled out by the fact that X_{0}X_{1} … is an accepting run. By the induction hypothesis, the second case yields M, k ⊧ δ and M, j ⊧ γ whereby M, i ⊧ γ Uδ.

(β = γVδ)

In general if X ⟶^{P} Y and γVδ ∈ consq(X), then either γ ∧ δ ∈ consq(X) or δ ∈ consq(X) and γVδ ∈ consq(Y). It follows that either for all k ≥ i, γVδ ∈ consq(X_{k}) and δ ∈ consq(X_{k}) or there exists k ≥ i such that γ ∧ δ ∈ consq(X_{k}) and for all j such that i ≤ j < k, γ ∈ consq(X_{j}).

If the first case holds, by the induction hypothesis, we have M, k ⊧ δ for all k ≥ i, so M, i ⊧ γVδ by the semantics of the modality V. If the second case holds, from the definition of consq, it follows that γ, δ ∈ consq(X_{k}). Hence, by the induction hypothesis, M, k ⊧ γ and M, k ⊧ δ, so M, k ⊧ γ ∧ δ. Also, by the induction hypothesis, for j such that i ≤ j < k, M, j ⊧ γ. From the semantics of the modality V, it then follows that M, i ⊧ γVδ.

□

Since X_{0} ∈ dnf(α), we have α ∈ consq(X_{0}) (Lemma 4.2 (ii)). It then follows that M, 0 ⊧ α.

Completeness

Let M = P_{0}P_{1} … be a model such that M, 0 ⊧ α. We have to show that M is accepted by (A_{α}, G_{1}, G_{2}, …, G_{k}). We begin with an auxiliary lemma.

Lemma 4.4 Let X be a state of A_{α} such that for some i, M, i ⊧ ⋀ X. Then there exists a state Y of A_{α} such that:

• X ⟶^{P_{i}} Y.

• M, i+1 ⊧ Y.

• For all γ Uδ ∈ CL(α), if γ Uδ ∈ consq(X) and δ ∉ consq(X) and M, i+1 ⊧ δ, then δ ∈ consq(Y).

Proof Let next_{1} = {γ Uδ ∈ consq(X) | δ ∉ consq(X) and M, i+1 ⊧ δ}. Note that next_{1} ⊆ snext(X) for, in general, if γ Uδ ∈ consq(X′) and δ ∉ consq(X′) then it must be the case that O(γ Uδ) ∈ consq(X′). Let next_{2} = snext(X) − next_{1}.

Since M, i ⊧ ⋀ X, it must be the case that M, i+1 ⊧ ⋀ snext(X). Hence M, i+1 ⊧ ⋀ next_{1} and M, i+1 ⊧ ⋀ next_{2}.

Let Δ = {δ | γ Uδ ∈ next_{1}}. From the definition of next_{1}, M, i+1 ⊧ δ for each δ ∈ Δ. For each δ ∈ Δ, since we know that δ ⇔ ⋁_{Z∈dnf(δ)} ⋀ Z, there must be some Z_{δ} ∈ dnf(δ) such that M, i+1 ⊧ Z_{δ}. Let Z_{1} = ⋃_{δ∈Δ} Z_{δ}.

Since M, i+1 ⊧ ⋀ Z_{1}, Z_{1} must be consistent. Further, from the way dnf is defined on U, it follows that Z_{1} ∈ dnf(⋀ next_{1}).

Similarly, since M, i+1 ⊧ ⋀ next_{2}, there must be a set Z_{2} ∈ dnf(⋀ next_{2}) such that M, i+1 ⊧ ⋀ Z_{2}. We choose Y to be Z_{1} ∪ Z_{2}.

To show that X ⟶^{P_{i}} Y, we note that dnf(⋀ snext(X)) = dnf((⋀ next_{1}) ∧ (⋀ next_{2})). We know that Z_{1} ∈ dnf(⋀ next_{1}) and Z_{2} ∈ dnf(⋀ next_{2}). Since M, i+1 ⊧ ⋀ Z_{1} and M, i+1 ⊧ ⋀ Z_{2}, Z_{1} ∪ Z_{2} is consistent. Thus, Y = Z_{1} ∪ Z_{2} ∈ dnf(snext(X)). To check that P_{i} is a valid label, we just use the fact that M, i ⊧ X. So, if p ∈ X, then p ∈ P_{i} and if ¬p ∈ X then p ∉ P_{i}.

Clearly, M, i+1 ⊧ ⋀(Z_{1} ∪ Z_{2}). Further, for all δ ∈ Δ, δ ∈ consq(Z_{1} ∪ Z_{2}), since δ ∈ consq(Z_{δ}) ⊆ consq(Z_{1}) ⊆ consq(Z_{1} ∪ Z_{2}).

□

We use this lemma to produce an accepting run as follows. First, note that α ⇔ ⋁_{X∈S_{in}} ⋀ X holds. Since M, 0 ⊧ α, we have M, 0 ⊧ ⋁_{X∈S_{in}} ⋀ X, so S_{in} is non-empty—there must exist X_{0} ∈ S_{in} such that M, 0 ⊧ ⋀ X_{0}.

From the previous lemma, given M, 0 ⊧ ⋀ X_{0}, we can find X_{1} such that X_{0} ⟶^{P_{0}} X_{1} and M, 1 ⊧ ⋀ X_{1}. Repeatedly applying the lemma, we extract a run X_{0}X_{1} … of A_{α}.

Suppose that this run is not an accepting run. Then there is some formula γ Uδ ∈ CL(α) and an index k ∈ ℕ_{0} such that for all i ≥ k, γ Uδ ∈ consq(X_{i}) and δ ∉ consq(X_{i}). But γ Uδ ∈ consq(X_{k+1}), so M, k+1 ⊧ γ Uδ by Lemma 4.2 (iv). So, there exists j ≥ k+1 such that M, j ⊧ δ and for all ℓ, k+1 ≤ ℓ < j, M, ℓ |̸= δ. Since γ Uδ ∈ consq(X_{j−1}) and δ ∉ consq(X_{j−1}) and M, j ⊧ δ, by the preceding lemma we must have δ ∈ consq(X_{j}) which is a contradiction.

On-the-fly traversal

We have shown that the automaton defined in terms of the function dnf contains all possible models of the formula α. This automaton can be constructed “on-the-fly”. We begin by constructing the states corresponding to dnf(α). After that, whenever we need to find the successors of a node X, we apply the function dnf to ⋀ snext(X). With some bookkeeping, we can avoid duplicating nodes. This is essentially what the algorithm in [GPVW95] computes, though they also combine some low-level optimization with the basic algorithm

A straightforward implementation of dnf yields an automaton which could potentially take time 2^{O(n^{2})} for an input formula of length n, even though the total number of states is bounded by 2^{O(n)}. In contrast, the algorithm of [GPVW95] runs in 2^{O(n)} time [DSz96].

On the other hand, it is possible to build in optimizations when implementing dnf which could bring down the bound. The main point is that the dnf construction clearly brings out the formal basis for the on-the-fly construction, which is somewhat obscured in the direct algorithmic reasoning of [GPVW95].

5 Extensions

The temporal logic we have considered ignores the labels on the transitions of a program— the model generated by a run is just the sequence of states it goes through. It is often useful to be able to talk about which transitions were used as well—for instance, in the setting of concurrent programs, the automaton is often specified as a synchronized product of sequential automata, where the synchronization mechanism is encoded via the actions performed. Normally, each sequential component comes equipped with a local set of actions. If an action is common to more than one component, those components must synchronize to perform the action. Actions which involve disjoint sets of processes can be performed concurrently.

It is not difficult to extend the syntax of LTL to include a modality which talks about actions—for each a ∈ Σ, we introduce the modality ⟨a⟩. A model is no longer just a sequence of propositional valuations P_{0}P_{1} …, but instead a sequence of transitions of the form P_{O} ⟶^{a_{0}} P_{1} ⟶^{a_{1}} ⋯, where each P_{i} is a subset of P, as before, and each a_{i} belongs to Σ. The semantics of the new modality is the obvious one. Let M = P_{O} ⟶^{a_{0}} P_{1} ⟶^{a_{1}} · · ·. Then

M, i ⊧ ⟨a⟩α iff a_{i} = a and M, i+1 ⊧ α.

Let us denote this extended version of LTL as LTL(Σ).

Both the global automata-theoretic construction of Section 3 as well as the on-the-fly approach of [GPVW95] can be extended smoothly to LTL(Σ) [Mad96].

Having extended LTL to talk about actions, the next challenge is to exploit the concurrency present in the program specification to further reduce the complexity of modelchecking. As we mentioned in the Introduction, here we have assumed that all program runs are represented as infinite sequences. However, when the program involves concurrent actions, this approach generates many equivalent interleavings of the same stretch of concurrent behaviour. It would be extremely useful if we can identify just one representative sequence to be verified for each such class of interleavings.

There is a considerable amount of work in progress on designing so-called “partial order methods” for verifying temporal properties of concurrent programs [GW94, Val90]. Another challenging task is to identify subclasses of formulas in LTL(Σ) which have the following property: if a formula is true in one representative interleaving of a concurrent run, then it is true in all interleavings. Though some subsets of LTL(Σ) which have this property have been identified, the search for a full characterization of this class is elusive [MT96].

Acknowledgments I thank Deepak D’Souza and P Madhusudan for shedding light on the subtleties of the on-the-fly method. In particular, the dnf based presentation of the [GPVW95] construction is due to Deepak.

References

[AHU74] A.V. Aho, J.E. Hopcroft and J.D. Ullman: The Design and Analysis of Algorithms, Addison-Wesley, Reading (1974).

[Bü60] J.R. Büchi: On a decision method in restricted second order arithmetic, Z. Math. Logik Grundlag. Math, 6 (1960) 66–92

[CVWY92] C. Courcoubetis, M. Vardi, P. Wolper and M. Yannakakis: Memory efficient algorithms for the verification of temporal logic properties, Formal Methods in System Design 1 (1992) 275–288.

[DSz96] Deepak D’Souza: On-the-fly techniques for linear time temporal logic, Manuscript (1996).

[GPVW95] R. Gerth, D. Peled, M. Vardi and P. Wolper: Simple on-the-fly automatic verification of linear temporal logic, Proc. IFIP/WG6.1 Symp. on Protocol Specification, Testing and Verification, Warsaw, Poland, June 1995.

[GW94] P. Godefroid and P. Wolper: A partial approach to model checking, Inform. and Comput., 110 (1994) 305–326.

[Mad96] P. Madhusudan: An on-the-fly algorithm for linear time temporal logic, M.Sc. Thesis, Anna University, Madras, India (1996).

[MP91] Z. Manna and A. Pnueli: The Temporal Logic of Reactive and Concurrent Systems (Specification), Springer-Verlag, Berlin (1991).

[MT96] M. Mukund and P.S. Thiagarajan: Linear time temporal logics over Mazurkiewicz traces, Proc MFCS ’96, LNCS 1113 (1996) 62–92.

[Pnu77] A. Pnueli: The temporal logic of programs, Proc. 18th IEEE FOCS (1977) 46–57.

[SVW87] A.P. Sistla, M. Vardi and P. Wolper: Reasoning about infinite computation paths, Proc. 24th IEEE FOCS (1983) 185–194.

[Th90] W. Thomas: Automata on infinite objects, in J. van Leeuwen (ed.), Handbook of Theoretical Computer Science, Volume B, North-Holland, Amsterdam (1990) 133–191.

[Th96] W. Thomas: Languages, automata and logic, Report 9607, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität, Kiel, Germany, May 1996. (Preliminary version of a chapter to appear in G. Rozenberg, A. Salomaa (eds.), Handbook of Formal Language Theory, Springer-Verlag.)

[Val90] A. Valmari: Stubborn sets for reduced state space generation, LNCS 483 (1990) 491–515.

[VW86] M. Vardi and P. Wolper: An automata theoretic approach to automatic program verification, Proc. 1st IEEE LICS, (1986) 332–345.

[VW94] M. Vardi and P. Wolper: Reasoning about infinite computations, Inform. Comput., 115(1) (1994) 1–37.