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

Revision as of 19:37, 3 September 2017

Revision as of 19:39, 3 September 2017

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 an equivalenta 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.