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

Revision as of 13:32, 20 October 2020

Latest revision as of 21:36, 9 August 2025

(7 intermediate revisions by 7 users not shown)

Line 1:

In [[formal verification]],

finite state [[model checking]] needs to find a [[Büchi automaton]] (BA) equivalent to a given [[Linearlinear 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.

</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.

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.

==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 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 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 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 100 ⟶ 98:

===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 Bu¨chiBü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.

Line 234 ⟶ 232:

==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==