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

Revision as of 15:38, 3 September 2016

Latest revision as of 21:36, 9 August 2025

(21 intermediate revisions by 17 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 an 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/>;

aA verified construction mechanism of this by Schimpf, Merz and Smaus is also available.<ref name=TPHOLS2009/>A. isSchimpf, alsoS. availableMerz, 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.

</ref>

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

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

Line 159 ⟶ 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''' ''create_graph''('''LTL''' f) {

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

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

}

}}

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

1: '''if''' curr = ∅ '''then'''

Line 243 ⟶ 229:

* For each sub-formula g = g₁ '''U''' g₂, let F_g = { q ∈ Nodes | g₂ ∈ ''Now''(q) or g ∉ ''Now''(q) }, then '''F''' = { F_g | 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==