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

Revision as of 11:23, 4 November 2021

Revision as of 15:03, 10 March 2022

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.

Line 32:

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 iff 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 strictly super set M' such that M and M' are equiv-satisfiable.

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

{|

|

Line 100:

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