Tableau-based decision method for testing satisfiability of the linear temporal logic LTL

V Goranko

Tableau-based decision method for testing satisfiability of the linear temporal logic LTL

Valentin Goranko DTU Informatics

November 2010

Tableau for LTL: introduction

The tableau method forLTL searches systematically for alinear modelsatisfying the input formula.

We will considerLTLover a minimal language with one transition relation, containing>,¬, and∧as Boolean connectives, and X, G, and U as temporal operators.

The other Boolean constants and connectives>,⊥,∨,→, as well as the operators F and R will be assumed definable.

We will present an optimized version of the first construction of tableau for LTLdeveloped by Wolper in 1983-85.

It takes exponential time and space in the length of the formula, but can be optimized to work inPSpace.

V Goranko

Types of formulae

We distinguish 4 types of formulae:

1. α-formulae, of conjunctive type.

Everyα-formulaθ is associated with itsα-components, and is equivalent to their conjunction.

E.g., theα-components ofϕ∧ψ are θ₁ =ϕand θ₂ =ψ, and the only α-component of ¬¬ϕ isθ1 =ϕ.

2. β-formulae, of disjunctive type.

Everyβ-formulaθ is associated with itsβ-components, and is equivalent to their disjunction.

E.g., theβ-components ofϕ∨ψ areθ₁ =ϕandθ₂ =ψ.

3. Nexttime formulaein LTL are those of the type Xϕ.

The nexttime componentof Xϕis ϕ.

4. literals: >,¬>, atomic propositions and their negations.

The literals and the nexttime formulae areprimitive formulae.

α- and β-formulae in LTL

Theα- and β-formulae inLTL and their components:

α α1 α2

¬¬ϕ ϕ ϕ

¬Xϕ X¬ϕ X¬ϕ

ϕ∧ψ ϕ ψ

Gϕ ϕ XGϕ

¬(ϕUψ) ¬ψ ¬ϕ∨ ¬X(ϕUψ)

β β1 β2

¬(ϕ∧ψ) ¬ϕ ¬ψ

¬Gϕ ¬ϕ X¬Gϕ

ϕUψ ψ ϕ∧X(ϕUψ)

Lemma

I. For everyα-formulaϕ: ϕ≡α₁(ϕ)∧α₂(ϕ).

II. For everyβ-formula ϕ: ϕ≡β₁(ϕ)∨β₂(ϕ).

V Goranko

Closure of an LTL- formula

The closure cl(η) of an LTL-formulaη is the least set of formulae such that:

1. >, ϕ∈cl(η);

2. cl(η) is closed under taking all components of α-formulae, β-formulae, and nexttime-formulae.

NB:closure under subformulae and negation is not required.

For any set of formulae Φ we definecl(Φ) :=S

{cl(ϕ)| ϕ∈Φ}. A set of formulae Φ isclosedif Φ =cl(Φ).

The closure of a formula (and, of any finite set of formulae) is always a finite set, of cardinality linear in the length of the formula.

Closure of LTL formulae: example

Running example 1:

η=(pUq)∧Gr

cl(η) ={η,pUq,Gr,p∧X(pUq),q,r,XGr,p,X(pUq)} Running example 2:

η=(pUq)∧(p→ ¬Xq)

cl(η) ={η,pUq,p → ¬Xq,p∧X(pUq),q,p,X(pUq),¬p,¬Xq,X¬q} Exercise: Define explicitly closure of LTL-formulae.

Exercise: Show that cl(ϕ) is finite for everyϕ∈LTL.

V Goranko

Consistent and fully expanded subsets of a closure

A set of formulae ispatently inconsistent if it contains⊥, or ¬>, or a contradictory pair of formulae¬ϕandϕ.

Definition (Fully expanded set)

A set of formulae Φ isfully expandediff:

1. it is not patently inconsistent;

2. for every α-formula in Φ, all of its α-components are in Φ;

3. for every β-formula in Φ, at least one of itsβ-components is in Φ.

Exercise: Give explicitly the closure conditions for fully expanded sets of LTL-formulae.

Full expansions of a set of LTL formulae

Just like inML, a fully expanded set ∆ of LTL formulae is a full expansion of a set of LTL formulae Γ, if ∆ can be obtained from Γ by repeated application of the following rules:

1. for every α-formula in the current set, add all of its α-components.

2. for every β-formula in the current set, at one of its β-components.

Computing the full expansions of Γ corresponds to saturating a local tableau for LTLwith input set Γ and collecting the sets of formulae on every open branch.

Thus, a set Γ may have several, possibly none, full expansions.

Like inML, not every fully expanded set is satisfiable.

The purpose of the tableau for LTL is to determine whether at

V Goranko

Local tableau for LTL

The local tableau for LTL is defined by extending the the unlabeled tableau for classical propositional logic with the following rules:

Non-branching rules (α-rules) Branching rules (β-rules)

(¬X)

¬Xϕ

↓ X¬ϕ

(G)

Gϕ

↓ ϕ,XGϕ

(¬G)

¬Gϕ . &

¬ϕ X¬Gϕ

(¬U)

¬(ϕUψ)

↓

¬ψ,¬ϕ∨ ¬X(ϕUψ)

(U)

ϕUψ . &

ψ ϕ∧X(ϕUψ)

The rest is just like the local tableau for ML.

Computing full expansions of sets of LTL-formulae by encapsulating the local tableau

The procedureFullExpansionfor computing the family FE(Γ) of full expansions of a given set of formulae Γ uses the following set replacement operationsapplied to a set of formulae Φ in a family of sets of formulaeF:

(α): Ifϕ∈Φ for some α-formula ϕwith α-components ϕ1 andϕ2, replace Φ by Φ∪ {ϕ1, ϕ2}.

(β): Ifϕ∈Φ for some β-formulaϕwith β-components ϕ1 andϕ2, replace Φ by Φ∪ {ϕ1} and Φ∪ {ϕ2}. Anexpansion step:

1. choose a set Φ from the current family of sets F; 2. choose an α- or β- formula ϕ∈Φ;

3. apply the respective set replacement operation for ϕto Φ.

Proviso: if a patently inconsistent set is added to F as a result of

V Goranko

Exercise: Give explicitly the set-replacement operations of the procedureFullExpansionfor theLTL-formulae ¬Xϕ,ϕUψ,

¬(ϕUψ), and Gϕ.

Given a finite set of formulae Γ, the procedureFullExpansion starts with the singleton family{Γ} and checks if it is patently inconsistent.

If so, it returnsFE(Γ) =∅.

Otherwise, it applies repeatedly expansion steps to the current familyF until saturation, i.e. until no application of a set replacement operation can changeF.

The stage of saturation is guaranteed to occur.

At that stage, the familyFE(Γ) of sets of formulae is produced and returned.

Full expansions: Example 1

Letη:= (pUq)∧Gr. The full expansions of{η}: Φ1 ={η,pUq,Gr,q,r,XGr}

Φ2 ={η,pUq,Gr,p∧X(pUq),p,X(pUq),r,XGr}

V Goranko

Full expansions: Example 2

Letη:= (pUq)∧(p→ ¬Xq).

The full expansions of{(pUq)∧(p → ¬Xq)}: Φ₁ ={η,pUq,q,p→ ¬Xq,¬p}

Φ₂ ={η,pUq,q,p→ ¬Xq,¬Xq,X¬q}

Φ3 ={η,pUq,p∧X(pUq),p,X(pUq),(p → ¬Xq),¬p}This set is patently inconsistent and is eliminated immediately.

Φ₄ ={η,pUq,p∧X(pUq),p,X(pUq),(p → ¬Xq),¬Xq,X¬q}

Eventualities in LTL

Eventualitiesare formulae stating that something will happen eventually in the future, but without specifying exactly when.

In particular, the eventualities inLTL are the formulae of the type ϕUψ and¬Gϕ.

V Goranko

Hintikka structures for LTL: Hintikka traces

Hintikka trace is the linear version of Hintikka structure.

Definition (Hintikka trace)

Given a set of formulae Φ, aHintikka trace(HT) for Φ is a mappingH:N→ P(Φ) satisfying the following conditions for everyn∈N:

H1 H(n) is fully expanded;

H2 If Xϕ∈ H(n), then ϕ∈ H(n+ 1)

H3 IfϕUψ∈ H(n), then there exists i ≥0 such that ψ∈ H(n+i) andϕ∈ H(n+j) for every j such that 0≤j <i.

Definition

A formulaθ∈LTLis satisfiable in a Hintikka trace H ifθ∈ H(n) for somen ∈N.

Proposition

In every Hintikka traceH:

1. If¬(ϕUψ)∈ H(n), then for every i ∈Nif ¬ψ∈ H(n+i) then ϕ∈ H(n+j) for some j such that 0≤j <i .

2. IfGϕ∈ H(n), then ϕ∈ H(n+i) for every i ∈N. Lemma

For any set of formulaeΦ, every linear ITS M= (N,L) generates a Hintikka traceH:N→ P(Φ)for Φ, where

H(n) ={ϕ∈LTL | M,n|=ϕ}for every n∈N. Proof: Straightforward verification of H1-H3. Exercise.

Usually, we will be interested in Hintikka traces for setscl(η), whereη is a formula for which we want to find a model.

V Goranko

Satisfiability and Hintikka traces

Theorem

A formulaη∈LTLis satisfiable iff it is satisfiable in a Hintikka trace for cl(η).

Proof: One direction follows by the Lemma above for Φ =cl(η).

For the converse, supposeη ∈ H(m) for some Hintikka trace H:N→ P(cl(η)) and m∈N. We can assume that m= 0.

We define the following state descriptionLin N: L(n) :=PROP∩ H(n).

LetM= (N,succ,L), where succ is the successor relation in N. We show by induction onθ∈LTLthat for everyn ∈N:

(i) if θ∈ H(n) thenM,n|=θ;

(ii) if ¬θ∈ H(n) thenM,n|=¬θ.

Exercise: Complete the details of the proof above.

Tableaux construction for testing satisfiability in LTL

The tableau procedure for a given input formulaη attempts to construct a non-empty graphT^η, called atableau, representing in a way sufficiently many possible Hintikka traces forη.

The procedure consists of three major phases:

1. Pretableau construction phase 2. Prestate elimination phase 3. State elimination phase

Since no different prestates or states with the same labels will be created, we will identify prestates or states with their labels.

V Goranko

Pretableau construction phase

That phase produces a finite digraph with labeled verticesP^η – thepretableauforη – following prescribedconstruction rules.

The set of nodes of the pretableau properly contains the set of nodes of the tableauT^η that is to be ultimately built.

The pretableau has two types of nodes: states andprestates.

The states are labeled with fully expanded subsets ofcl(η) and represent states of a Hintikka structure, while the prestates can be labeled with any subsets ofcl(η) and play only a temporary role.

State construction rule PrExp

The rulePrExp^LTL produces all offspring statesof a prestate.

RulePrExp^LTL: Given a prestate Γ to which the rule has not yet been applied, do the following:

1. Compute the familyFE(Γ) ={∆₁, . . .∆_n}of all full

expansions of Γ and add these as (labels of) new states in the pretableau, called the offspring states of Γ.

2. For each newly introduced state ∆, create an edge Γ =⇒∆.

3. If, however, the pretableau already contains a state with label

∆ then do not create a new state with that label, but create an edge Γ =⇒∆ to that state.

We denote the set{∆| Γ =⇒∆}of offspring states of Γ by states(Γ).

V Goranko

Prestate construction rule Next

The ruleNext^LTL produces thesuccessor prestate of a state (recall that we are looking for a linear model).

RuleNext^LTL: Given a state with label ∆, to which the rule has not yet been applied, do the following:

1. Add a successor prestate Γ of ∆ with label {ψ| Xψ∈∆}. 2. If the label of ∆ does not contain any formula of the type Xψ

then add a successor prestate Γ of ∆ with label {>}. 3. Create an edge ∆−→Γ.

4. If, however, the pretableau already contains a prestate with label Γ then do not create a new prestate with that label, but extend an arrow ∆−→Γ to that prestate.

Pretableau construction phase completion

The pretableau construction phase for an input formulaη begins with creating a single prestate{η}, followed by alternating applications of the rules PrExp and Next, respectively to the prestates and the states created earlier in the construction.

The construction phase ends when none of these rules can add any new states or prestates to the current graph.

The resulting graph is the pretableauP^η.

V Goranko

Pretableau examples: notation

In what follows:

The mark * means that an expansion step has been applied to the formula.

Superscript ‘s’ means that the set is a state.

Superscript ‘p’ means that the set is a prestate.

Pretableau: example 1

(pUq)∧Gr

1.

(pUq)∧Gr ^P

@@@R

2.

 S





(pUq)∧Gr^∗ pUq^∗,Gr^∗

q, r,XGr





4. ? ^P

Gr

?

5.

S

Gr^∗ r,XGr

3.

 S





(pUq)∧Gr^∗ pUq^∗, p,X(pUq)

Gr^∗, r,XGr





6. ? ^P

pUq,Gr

@@R

7.

S

pUq^∗, q Gr^∗, r,XGr

@

@@

@ I

8.

S

pUq^∗, p,X(pUq) Gr^∗, r,XGr

V Goranko

Pretableau: example 2

(pUq)∧(p→ ¬Xq) 1.

(pUq)∧ (p→ ¬Xq)

P

? @

@@R ?

2.

 S













(pUq)∧ (p→ ¬Xq)^∗,

pUq^∗, q, p→ ¬Xq^∗,

¬p













?

3.

 S













(pUq)∧ (p→ ¬Xq)^∗,

pUq^∗, q, p→ ¬Xq^∗,

¬Xq^∗,X¬q













?

4.

 S

















(pUq)∧

(p→ ¬Xq)^∗ pUq^∗,p, X(pUq), (p→ ¬Xq)^∗,

¬p















 removed

5.

 S

















(pUq)∧

(p→ ¬Xq)^∗ pUq^∗, p, X(pUq), (p→ ¬Xq)^∗,

¬Xq^∗,X¬q

















6.

P

>

? I 7.

S

>

8.

P

¬q

?

9. ^S

¬q

10.

P

pUq,¬q

@@@R 11.

S

pUq^∗,¬q p,X(pUq)

?

12. ^S

pUq^∗,¬q, q removed

13. ^P

pUq

@@R

14. ^S

pUq^∗, q I

15.

S

pUq^∗, p, X(pUq)

Pretableau: example 2

(pUq)∧(p→ ¬Xq) 1.

(pUq)∧ (p→ ¬Xq)

P

? ?

2.

 S













(pUq)∧ (p→ ¬Xq)^∗,

pUq^∗, q, p→ ¬Xq^∗,

¬p













?

3.

 S













(pUq)∧ (p→ ¬Xq)^∗,

pUq^∗, q, p→ ¬Xq^∗,

¬Xq^∗,X¬q













?

5.

 S

















(pUq)∧

(p→ ¬Xq)^∗ pUq^∗, p, X(pUq), (p→ ¬Xq)^∗,

¬Xq^∗,X¬q

















6.

P

>

? I 7.

S

>

8.

P

¬q

?

9. ^S

¬q

10.

P

pUq,¬q

11.

S

pUq^∗,¬q p,X(pUq)

?

13. ^P

pUq

@@R

I

S

pUq^∗, p,

V Goranko

Pretableau: example 3

(pUq)∧G¬q 1.

(pUq)∧G¬q ^P

@@@R

2.

 S





(pUq)∧G¬q^∗ pUq∗,G¬q∗ q,¬q,XG¬q



 removed

3.

 S





(pUq)∧G¬q^∗ pUq^∗, p,X(pUq), G¬q^∗,¬q,XG¬q





4. ? ^P

pUq,G¬q

@@R

5.

S

pUq^∗,q G¬q^∗,¬q,XG¬q

removed

6.

S

pUq^∗, p,X(pUq) G¬q^∗,¬q,XG¬q

Pretableau: example 3

(pUq)∧G¬q 1.

(pUq)∧G¬q ^P

@@@R

3.

 S





(pUq)∧G¬q^∗ pUq^∗, p,X(pUq), G¬q^∗,¬q,XG¬q





4. ? ^P

pUq,G¬q

@@R

6.

S

pUq^∗, p,X(pUq) G¬q^∗,¬q,XG¬q

V Goranko

Prestate elimination phase for LTL

In this phase, all prestates are removed fromP^η, together with their incoming and outgoing arrows, by applying the following prestate elimination rule:

RulePrElim^LTL: For every prestate Γ inP^η, do the following:

1. Remove Γ from P^η;

2. If there is a state ∆ in P^η with ∆−→Γ, then for every state

∆⁰ ∈states(Γ), create an edge ∆−→∆⁰.

The resulting graphT0^η is called the initial tableau forη.

The offspring states of the input prestate{η} are called input statesof T0^η.

Prestate elimination and initial tableau: example 1

(pUq)∧Gr

2.

 ?









(pUq)∧Gr^∗ pUq∗,Gr∗

q,r,XGr









 3.

 ?









(pUq)∧Gr^∗ pUq^∗,p,X(pUq),

Gr^∗,r,XGr











@@R 5.

( Gr∗,>

r,XGr R )

7.

( pUq^∗,>,q, Gr∗,r,XGr

) 8.

( pUq^∗,p,X(pUq)

>,Gr∗,r,XGr )

The initial states of the tableau are marked with?.

V Goranko

Prestate elimination and initial tableau: example 2

(pUq)∧(p→ ¬Xq)

2.

 ?













(pUq)∧ (p→ ¬Xq)^∗,

pUq^∗, q, p→ ¬Xq^∗,

¬p













?

3.

 ?













(pUq)∧ (p→ ¬Xq)^∗,

pUq^∗, q, p→ ¬Xq^∗,

¬Xq^∗,X¬q













?

5.

 ?

















(pUq)∧

(p→ ¬Xq)^∗ pUq^∗, p, X(pUq), (p→ ¬Xq)^∗,

¬Xq^∗,X¬q

















7.

> 6 9.

¬q,>

11.

pUq^∗,¬q,>

p,X(pUq)

@@R 14.

pUq^∗, q,>

I

15.

pUq^∗,>, p, X(pUq)

Prestate elimination and initial tableau: example 3

(pUq)∧G¬q

3.

 ?





(pUq)∧G¬q^∗ pUq^∗, p,X(pUq), G¬q^∗,¬q,XG¬q





@@R

6.

>, pUq^∗, p,X(pUq) G¬q∗,¬q,XG¬q

V Goranko

State elimination phase for LTL

The purpose of the state elimination phase is to remove from the tableau all ‘bad’ states, the labels of which are not satisfiable in any Hintikka trace, and hence in any linear model for LTL.

That will be done using thestate elimination rules StElim1^LTL andStElim2^LTL.

State elimination rule StElim1

One possible reason for existence of a ‘bad state’ in a current tableau is that it may lack a successor state.

Such states can arise because some prestates may have no full expansions, and hence may yield no offspring states.

Once such bad states are removed, some of their predecessor states may be left without successors, so they must be removed, too, etc., until stabilization.

Formally, the elimination of states with no successors is done by applying the following rule.

RuleStElim1^LTL: If a state∆has no successor states in the current tableau, then remove∆from the tableau.

V Goranko

Realization of eventualities in LTL

A state is ‘bad’ if it contains an eventuality that is not ‘realized’ in any reachable state. Such states are removed by another state elimination rule, using the notion ofeventuality realization.

Path inTn^η: path of successor states ∆₀−→∆₁ −→. . . in Tn^η. Definition (Realization of eventualities in LTL)

An eventualityξ =ϕUψ isrealized at the state ∆ in Tn^η if there exists a finite path ∆ = ∆0,∆1, . . . ,∆minT^nη, such that

ξ, ψ∈∆_m andξ, ϕ∈∆_i for everyi = 0, . . . ,m−1. We say thatξ is realized on the path ∆0,∆1, . . . ,∆m. The shortest length of such a path is therank of the statewith respect to the eventuality ξ. If ψ∈∆, then ξ is immediately realizedat the state ∆.

Realization of eventualities¬Gϕis defined likewise.

Efficient algorithms for testing the realization of the eventualities in tableau states useglobal approach, where that testing is done for all eventualities at all states simultaneously.

State elimination rule StElim2

RuleStElim2^LTL: If an eventuality ξ∈∆is not realized on any path starting from a state∆, then remove∆ from the current tableau.

V Goranko

The state elimination phase in LTL

The state elimination phase is carried out in a sequence of stages:

• starting at stage 0 with the initial tableau T0^η,

• eliminating at every stagen at most one state for the current tableauTn^η, by applying one of the state elimination rules,

• thus producing the new current tableau Tn+1^η .

The rulesStElim1^LTL and StElim2^LTL are applied alternatively, in any order, which may be determined by a specific strategy.

This procedure continues until reaching a stage when no further elimination of states by an application of any of the rules is possible.

The final tableau for LTL

When the state elimination phase reaches a stabilization stage the current tableau at that stage is thefinal tableau for η, denoted by T^η, with a set of states denoted byS^η.

Definition

The final tableauT^η isopenif η∈∆ for some ∆∈S^η; otherwise, T^η isclosed.

The procedure returnsnot satisfiable if the final tableau is closed.

Otherwise, it returnssatisfiable.

Moreover, an open tableau provides sufficient information for producing a finite Hintikka trace satisfyingη.

V Goranko

State elimination and final tableau: example 1

(pUq)∧Gr

2.

?

0





(pUq)∧Gr^∗ pUq∗,Gr∗

q, r,XGr



 3.

?

1





(pUq)∧Gr^∗ pUq^∗, p,X(pUq),

Gr^∗, r,XGr





@@R

5.

Gr∗,>

r,XGr

∞ R

7.

>, pUq^∗, q, Gr∗, r,XGr

0

8.

pUq^∗, p,X(pUq)

>,Gr∗, r,XGr

∞

No state gets eliminated due to patent inconsistency.

There is only one eventuality, pUq. The ranks are shown as subscripts.

State 8 gets eliminated due to RuleStElim2^LTL.

The final tableau is open; it gives two possible Hintikka traces for the formula.

State elimination and final tableau: example 2

(pUq)∧(p→ ¬Xq)

2.

?

0













(pUq)∧ (p→ ¬Xq)^∗,

pUq^∗, q, p→ ¬Xq^∗,

¬p













?

3.

?

0













(pUq)∧ (p→ ¬Xq)^∗,

pUq^∗, q, p→ ¬Xq^∗,

¬Xq^∗,X¬q













?

5.

?

2

















(pUq)∧ (p→ ¬Xq)^∗

pUq^∗, p, X(pUq), (p→ ¬Xq)^∗,

¬Xq^∗,X¬q

















7.

> _∞

6 9.

¬q,>

∞ 11.

pUq^∗,¬q,>

p,X(pUq)

1

@@R 14.

pUq^∗, q,>

I

015.

pUq^∗,>, p, X(pUq)

∞

There is only one eventuality,pUq.

The rank of each state is shown next to its bottom-right corner.

State 15 is eliminated due to RuleStElim2^LTL.

The final tableau contains three initial states: 2, 3, and 5. Hence, it is open.

V Goranko

State elimination and final tableau: example 3

(pUq)∧G¬q

3.

?

∞





(pUq)∧G¬q^∗ pUq^∗, p,X(pUq), G¬q^∗,¬q,XG¬q





@@R

6.

>, pUq^∗, p,X(pUq) G¬q∗,¬q,XG¬q

∞

There is only one eventuality,pUq.

States 3 and 6 get eliminated due to RuleStElim2^LTL.

The final tableau is empty, therefore closed. The attempt to build a Hintikka trace for the formula (pUq)∧G¬qhas failed, hence it is not satisfiable.

Soundness of the tableau for LTL

Soundness of the tableau procedure means that if the input formulaη is satisfiable, then the tableau T^η is open.

It suffices to prove that every state elimination rule is ‘sound’, meaning that it never eliminates a state with a satisfiable label.

Theorem (Soundness of the tableau for LTL) Ifη∈LTL is satisfiable thenT^η is open.

V Goranko

Completeness of the tableaux for LTL: the problem

Completenessof the tableau procedure means that if the input formulaη is not satisfiable, then the final tableauT^η is closed, so the tableau procedure is guaranteed to establish the unsatisfiability.

For completeness of the tableaux it suffices to show how from open final tableauT^η one can construct a Hintikka trace satisfying η.

One can try to extract such a Hintikka trace fromT^η, by starting with any state ∆ containingη and building up a path of successor states throughT^η, while ensuring that all eventualities appearing along that path eventually get realized on that path.

However, not every path inT^η satisfies that requirement, because different eventualities may be realized alongdifferent paths.

Building Hintikka traces from open tableaux

So, we have to guide the process of building a Hintikka trace.

The idea: build the Hintikka traceH(η) in a sequence of steps, each producing a finitepartial Hintikka trace appending to the previous one a finite path realizing onepending eventuality, while possibly adding more pending eventualities at the end.

Thus, an infinite path is produced in the limit, as a union of all partial Hintikka traces, in which there are no unrealized

eventualities – and that is the required Hintikka trace.

That construction is possible because the realization of any eventuality can be deferred indefinitely.

V Goranko

Completeness of the tableaux for LTL

Theorem (Completeness of the tableau for LTL)

For any formulaη ∈LTL, if the final tableauT^η is open, then the formula is satisfiable.

Corollary

The logicLTLhas the small model property.

Proof.

The construction ofH(η) above can be made finite by propagating the list of pending eventualities to every next state in the partial Hintikka traces produced as above and looping back whenever a state is to be created for which a state with the same label and same set of pending eventualities (even possibly listed in different order) appears earlier in the current trace.

That construction produces an ultimately periodic Hintikka trace with a number of states bounded exponentially by the size of the formula.

On the complexity and optimality of the tableau for LTL

The tableau procedure forLTL, as described above, shows that it takes exponential time in the size of the input formulaη.

On the other hand, it is known [Sistla&Clarke’85] that the problem of testing satisfiability of anLTL formula isPSpace-complete, so the tableau presented here uses more space resources than

necessary.

It can be optimized to work in (non-deterministic)PSpaceby first guessing a satisfying ‘Hintikka trace’ already in the pretableau, i.e., organizing a depth-first expansion of the pretableau, and then testing for its suitability with a more judicial memory use, namely only keeping in the memory the current position and the set of eventualities currently waiting to be satisfied.

V Goranko

Online implementation of the tableau for LTL

The tableau procedure forLTLdescribed above has been

implemented (in Python) by Angelo Kyrilov, and is available online:

http://msit.wits.ac.za/ltltableau

More optimized tableau procedure forLTL, implemented in Ocaml, can be downloaded and installed from

http://users.cecs.anu.edu.au/~rpg/PLTLProvers

Exercises on tableau for LTL

Using the tableau method check the followingLTL formulae for satisfiability:

1. Gp∧Fq→pUq 2. Gp∧Gq →G(p∧q) 3. Gp∨Gq →G(p∨q) 4. p∧G(p→Xp)→Gp 5. pU(q∧r)→(pUq∧pUr) 6. (pUq∧pUr)→pU(q∧r) 7. pU(q∨r)→(pUq∨pUr) 8. (pUq∨pUr)→pU(q∨r) 9. p∧G(p→Fp)→GFp 10. p∧G(p→XFp)→GFp