Content deleted Content added
m WP:CHECKWIKI error fix for #61. Punctuation goes before References. Do general fixes if a problem exists. - using AWB (8855) |
Added two spaces |
||
Line 1:
In [[formal verification]],
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 a 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>
| |||