Linear temporal logic to Büchi automaton: Difference between revisions

Revision as of 08:54, 3 September 2013

Latest revision as of 21:36, 9 August 2025

(37 intermediate revisions by 20 users not shown)

Line 1:

In [[formal verification]],

finite state [[model checking]] needs to find a [[Büchi automaton]] (BA) equivalent to a given [[linear temporal logic]] (LTL) formula, i.e., such that the LTL formula and the BA recognize the same [[ω-language]]. There are algorithms that translate an LTL formula to a BA.<ref name=VW94>M.Y. Vardi and P. Wolper, Reasoning about infinite computations, [[Information and Computation]], 115(1994), 1–37.</ref><ref name=KMMP93>Y. Kesten, Z. Manna, H. McGuire, [[Amir Pnueli|A. Pnueli]], A decision algorithm for full propositional temporal logic, CAV’93, Elounda, Greece, LNCS 697, Springer–Verlag, 97-109.</ref><ref name=GPVW93>R. Gerth, D. Peled, M.Y. Vardi and P. Wolper, "Simple On-The-Fly Automatic Verification of Linear Temporal Logic," Proc. IFIP/WG6.1 Symp. Protocol Specification, Testing, and Verification (PSTV95), pp. 3-18, Warsaw, Poland, Chapman & Hall, June 1995.

finite state [[model checking]] needs to compute an equivalent [[Büchi automaton]] (BA) to a [[Linear temporal logic]] (LTL) formula,

</ref><ref name=GOCAV01>

i.e., the LTL formula and the BA recognizes the same [[ω-language]].

There are algorithms that translate a LTL formula to an equivalent BA.<ref name=VW94>M.Y. Vardi and P. Wolper, Reasoning about infinite computations, Information and Computation, 115(1994), 1–37.</ref>

<ref name=KMMP93>Y.Kesten,Z.Manna,H.McGuire,A.Pnueli,A decision algorithm for full propositional temporal logic, CAV’93, Elounda, Greece, LNCS 697, Springer–Verlag, 97-109.</ref>

<ref name=GPVW93>R. Gerth, D. Peled, M.Y. Vardi and P. Wolper, "Simple On-The-Fly Automatic Verification of Linear Temporal Logic," Proc. IFIP/WG6.1 Symp. Protocol Specification, Testing, and Verification (PSTV95), pp. 3-18,Warsaw, Poland, Chapman & Hall, June 1995.

</ref>

<ref name=GOCAV01>

P. Gastin and D. Oddoux, Fast LTL to Büchi automata translation, Thirteenth Conference on Computer Aided Verification (CAV ′01), number 2102 in LNCS, Springer-Verlag (2001), pp. 53–65.

</ref> This transformation is normally done in two steps. The first step produces a [[generalized Büchi automaton]] (GBA) from a LTL formula. The second step translates this GBA into a BA, which involves a relatively [[Büchi automaton#Transforming from other models of description to non-deterministic B.C3.BCchi automata|easy construction]]. Since LTL is strictly less expressive than BA, the reverse construction is not always possible.

</ref>

This transformation is normally done in two steps.

The first step produces a [[generalized Büchi automaton]](GBA) from a LTL formula.

The second step translates this GBA into a BA, which involves relatively

[[Büchi_automaton#Transforming_from_other_models_of_description_to_non-deterministic_B.C3.BCchi_automata|easy construction]].

Since LTL is strictly less expressive than BA, the reverse construction is not possible.

The algorithms for transforming LTL to GBA differ in their construction strategies but they all have a common underlying principle, i.e., each state in the constructed automaton represents a set of LTL formulas that are ''expected'' to be satisfied by the remaining input word after occurrence of the state during a run.

The algorithms for transforming LTL to GBA

differ in their construction strategies but they

all have common underlying principle, i.e.,

each state in the constructed automaton represents a set of LTL formulas

that are ''expected'' to be satisfied by the remaining input word after occurrence of the state during a run.

==Transformation from LTL to GBA==

Here, two algorithms are presented for the construction. The first one provides a declarative and easy -to -understand construction. The second one provides an algorithmic and efficient construction. Both the algorithms assume that the input formula f is constructed using the set of propositional variables ''AP'' and f is in [[Linear temporal logic#Negation normal form|negation normal form]].

For each LTL formula f' without ¬ as top symbol, let ''neg''(f') = ¬f', and ''neg''(¬f') = f'.

For a special case f'='''true''', let ''neg''('''true''') = '''false'''.

Line 29 ⟶ 15:

Before describing the construction, we need to present a few auxiliary definitions.

For aan LTL formula ''f'', Let ''cl''( f ) be athe smallest set of formulas that satisfies the following conditions:

{|

|

Line 43 ⟶ 29:

|}

''cl''( f ) is closure of sub-formulas of f under negation''neg''.

Note that ''cl''( f ) may contain formulas that are not in negation normal form.

The subsets of ''cl''( f ) are going to serve as states of the equivalent GBA.

We aim to construct the GBA such that if a state ''corresponds'' to a subset M ⊂⊆ ''cl''( f ) then the GBA has an accepting run starting from the state for a word iffif and only if the word satisfies every formula in M and violates every formula in ''cl''( f )/ \ M.

For this reason,

we will not consider each formula set M that is clearly inconsistent

or subsumed by a strictlystrict super setsuperset M' such that M and M' are equiv-satisfiable.

A set M ⊂⊆ ''cl''( f ) is ''maximally consistent'' if it satisfies the following conditions:

{|

|

Line 75 ⟶ 61:

if f₁ '''U''' f₂ is true in some state then eventually f₂ is true at some state later.

{{Hidden begin|titlestyle = background:lightblue;|contentstyle = background-color: lightgrey;

{{hidden begin

|title = Proof of correctness of the above construction

|titlestyle = background:lightblue;

|bg2 = lightgrey

}}

Let ω-word ''w''= a₁, a₂,... over alphabet 2^''AP''. Let ''w''ⁱ = a_i, a_i+1,... .

Line 113 ⟶ 97:

===Gerth et al. algorithm===

The following algorithm is due to Gerth, Peled, [[Moshe Y. Vardi|Vardi]], and [[Pierre Wolper|Wolper]].<ref name=GPVW93/>

A verified construction mechanism of this by Schimpf, Merz and Smaus is also available.<ref name=TPHOLS2009>A. Schimpf, S. Merz, and J.-G. Smaus, "Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL," Proc. International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2009), pp. 424-439, Munich, Germany, Springer, August 2009.

The above construction creates exponentially many states upfront and many of those states may be unreachable.

</ref>

The following algorithm has two steps.

The aboveprevious construction creates exponentially many states upfront and many of those states may be unreachable.

In step one, it incrementally constructs a directed graph stored in a tableaux. In step two, it builds an [[labeled generalized Büchi automaton]] (LGBA) by defining nodes of the graph as states and directed edges as transitions.

The following algorithm avoids this upfront construction and has two steps.

In the first step, it incrementally constructs a directed graph.

In stepthe one, it incrementally constructs a directed graph stored in a tableaux. Insecond step two, it builds ana [[labeled generalized Büchi automaton]] (LGBA) by defining nodes of the graph as states and directed edges as transitions.

This algorithm takes reachability into account and may produce a smaller automaton but the worst-case complexity remains the same.

The nodes of the graph are labeled by sets of formulas and are obtained by decomposing formulas according to their Boolean structure, and by expanding the temporal operators in order to separate what has to be true immediately from what has to be true from the next state ononwards. For example, let us assume that an LTL formula f₁ '''U''' f₂ appears in the label of a node.

f₁ '''U''' f₂ is equivalent to f₂ ∨ ( f₁ ∧ '''X'''(f₁ '''U''' f₂) ).

The equivalent expansion suggests that f₁ '''U''' f₂ is true in one of the following two conditions.

# f₁ holds inat the current time and (f₁ '''U''' f₂) holds inat the next time step, or

# f₂ holds inat the current time step

ThisThe logictwo cases can be encoded by creating two states (nodes) of the automaton and the automaton may non-deterministically jump to either of them.

In the first case, we have offloaded a part of burden of proof in the next time step

therefore we also create another state (node) that will carry the obligation for next time step in its label.

We also need to consider temporal operator '''R''' that may cause such case split.

f₁ '''R''' f₂ is equivalent to ( f₁ ∧ f₂) ∨ ( f₂ ∧ '''X'''(f₁ '''R''' f₂) )

and this equivalent expansion suggests that f₁ '''R''' f₂ is true in one of the following two conditions.

# f₂ holds inat the current time and (f₁ '''R''' f₂) holds inat the next time step, or

# ( f₁ ∧ f₂) holds inat the current time step.

To avoid many cases in the following algorithm, let us define functions ''new1curr1'', ''next1'' and ''new2curr2'' that encode the above equivalences in the following table.

{| class="wikitable"

|-

! f !! new1curr1(f) !! next1(f) !! new2curr2(f)

|-

| f₁ '''U''' f₂ || {f₁} || { f₁ '''U''' f₂ } || {f₂}

Line 157 ⟶ 144:

For a node q, ''Now''(q) denotes the set of formulas that must be satisfied by the rest of the input word if the automaton is currently at node(state) q.

''Next''(q) denotes the set of formulas that must be satisfied by the rest of the input word if the automaton is currently at the next node(state) after q.

{{pre|1=

'''typedefs'''

'''LTL''': LTL formulas

'''LTLSet''': Sets of LTL formulas

'''NodeSet''': Sets of graph nodes ∪ {init}

'''globals'''

''Nodes'' : set of graph nodes := ∅

''Incoming'': ''Nodes'' → '''NodeSet''' := ∅

''Now'' : ''Nodes'' → '''LTLSet''' := ∅

''Next'' : ''Nodes'' → '''LTLSet''' := ∅

'''function''' ''create_graph''('''LTL''' f) {

expand({f}, ∅, ∅, {init} )

'''return''' (''Nodes'', ''Now'', ''Incoming'')

}

}}

'''function''' expand('''LTLSet''' newcurr, '''LTLSet''' old, '''LTLSet''' next, '''NodeSet''' incoming){

1: '''if''' newcurr = ∅ '''then'''

2: '''if''' ∃q ∈ ''Nodes'': ''Next''(q)=next ∧ ''Now''(q)=old '''then'''

3: ''Incoming''(q) := ''Incoming''(q) ∪ incoming

Line 186 ⟶ 174:

10: expand(''Next''(q), ∅, ∅, {q})

11: '''else'''

12: f ∈ newcurr

13: newcurr := newcurr\{f}

14: old := old ∪ {f}

15: '''match''' f '''with'''

Line 194 ⟶ 182:

18: '''skip'''

19: '''else'''

20: expand(newcurr, old, next, incoming)

21: | f₁ ∧ f₂ →

22: expand(newcurr ∪ ({f₁,f₂}\old), old, next, incoming)

23: | '''X''' g →

24: expand(newcurr, old, next ∪ {g}, incoming)

25: | f₁ ∨ f₂, f₁ '''U''' f₂, or f₁ '''R''' f₂ →

26: expand(newcurr ∪ (''new1curr1''(f)/\old), old, next ∪ ''next1''(f), incoming)

27: expand(newcurr ∪ (''new2curr2''(f)/\old), old, next, incoming)

28: '''return'''

}

Line 208 ⟶ 196:

Each call to ''expand'' aims to add a node and its successors nodes in the graph.

The parameters of the call describes a potential new node.

* The first parameter ''newcurr'' contains the set of formulas that are yet to be expanded.
* The second parameter ''old'' contains the set of formulas that are already expanded.

* The third parameter ''next'' is the set of the formula using which successor node will be created.

* The fourth parameter ''incoming'' defines set of incoming edges when the node is added to the graph.

At line 1, the '''if''' condition checks if ''new'' contains any formula to be expanded.

If the ''new'' is empty then atAt line 21, the '''if''' condition checks if there''curr'' alreadycontains existsany aformula stateto q' with same set ofbe expanded formulas.

If the ''curr'' is empty then at line 2 the '''if''' condition checks if there already exists a state q' with same set of expanded formulas.

If that is the case, then we do not add a redundant node, but we add parameter ''incoming'' in ''Incoming''(q') at line 3.

Otherwise, we add a new node q using the parameters at lines 5–9 and we start expanding a successor node of q using ''next''(q) as its unexpanded set of formulas at line 10.

In the case ''newcurr'' is not empty, then we have more formulas to expand and control jumps from line 1 to 12.

At lines 12–14, a formula f from ''newcurr'' is selected and moved to ''old''.

Depending on structure of f, the rest of the function executes.

* If f is a literal, then expansion continues at line 20, but if ''old'' already contains ''neg''(f) or f='''false''', then ''old'' contains an inconsistent formula and we discard this node by not making any recursive all at line 18.

* If f = f₁ ∧ f₂, then f₁ and f₂ are added to ''curr'' and a recursive call is made for further expansion at line 22.

''neg''(f) or f='''false''', then ''old'' contains an inconsistent formula and we discard this node by not making any recursive all at line 18.

* If f = '''X''' f₁ ∧ f₂, then f₁ and f₂ areis added to ''newnext'' andfor athe recursivesuccessor callof isthe madecurrent fornode furtherunder expansionconsideration at line 2224.

* If f = f₁ ∨ f₂, f = f₁ '''XU''' f₁₂, thenor f = f₁ is added to ''next'R''' forf₂ then the successorcurrent ofnode theis currentdivided into two nodes and for each node undera considerationrecursive atcall lineis 24made.

If f = f₁ ∨ f₂, f = f₁ '''U''' f₂, or f = f₁ '''R''' f₂ then the current node is divided into two nodes and for each node a recursive call is made. For the recursive calls, ''newcurr'' and ''next'' are modified using functions ''new1curr1'', ''next1'', and ''new2curr2'' that were defined in the above table.

<!--

There are following four possible results of the call.

Line 233 ⟶ 224:

Let (''Nodes'', ''Now'', ''Incoming'') = create_graph(f).

An equivalent LGBA to f is ''A''=(''Nodes'', 2^''AP'', ''L'', Δ, ''Q''₀, '''F'''), where

* ''L'' = { (q,a) | q ∈ ''Nodes'' and (''Now''(q) ∩ ''AP'') ⊆ a ⊆ {p ∈ P''AP'' | ¬p ∉ ''Now''(q) } }

* Δ = {(q,q')| q,q' ∈ Nodes and q ∈ Incoming(q') }

* ''Q''₀ = { q ∈ Nodes | init ∈ ''NowIncoming''(q) }

* For each sub-formula g = g₁ '''FU''' =g₂, {let F_g = { q ∈ Nodes | fg₂ ∈ ''Now''(q) or (f₁ '''U''' f₂)g ∉ ''Now''(q) }, | f₁then '''UF''' f= { F_2g | g ∈ ''cl''( f ) }

Note that node labels in the algorithmic construction does notdo not contain negation of sub-formulas of f. In the declarative construction a node has the set of formulas that are expected to be true. The algorithmic construction ensures the correctness without the need of all the true formulas to be present in a node label.

==Tools==

*[httphttps://spot.lip6lre.epita.fr SPOTSpot's LTL2TGBA] - LTL2TGBA translator included in Object-oriented model checkingC++ library SPOT. Online translator available.

*[http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/ LTL2BA] - Fast LTL to BA translator via alternating automata. Online translator available.

*[httphttps://sourceforge.net/projects/ltl3ba/ LTL3BA] - An up-to-date improvement of LTL2BA.

*[https://owl.model.in.tum.de/ Owl's LTL2NBA] - LTL2NBA translator included in Java library Owl. Online translator available.

==References==

Line 250 ⟶ 242:

{{DEFAULTSORT:Linear temporal logic to Buchi automaton}}

[[Category:Automata theory(computation)]]

[[Category:Model checking]]

[[Category:Temporal logic]]