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

Revision as of 22:55, 16 March 2017

Revision as of 22:56, 16 March 2017

Line 3:

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>