Revision as of 12:45, 12 February 2014 edit Ashutosh y0078 (talk \| contribs) 2,179 edits →Gerth et al. algorithm ← Previous edit		Revision as of 15:48, 12 February 2014 edit undo Ashutosh y0078 (talk \| contribs) 2,179 edits No edit summary Next edit →
Line 2: finite state [[model checking]] needs to compute an equivalent [[Büchi automaton]] (BA) to a [[Linear temporal logic]] (LTL) formula, i.e., the LTL formula and the BA recognizes the same [[ω-language]]. There are algorithms that translate aan 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.

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