Content deleted Content added
→Tools: update Spot's and ltl2ba's URL; cite Owl. |
m →Tools: HTTP to HTTPS for SourceForge |
||
| (One intermediate revision by one other user not shown) | |||
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 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 234:
*[https://spot.lre.epita.fr Spot's LTL2TGBA] - LTL2TGBA translator included in C++ library SPOT. Online translator available.
*[http://www.lsv.fr/~gastin/ltl2ba/ LTL2BA] - Fast LTL to BA translator via alternating automata. Online translator available.
*[
*[https://owl.model.in.tum.de/ Owl's LTL2NBA] - LTL2NBA translator included in Java library Owl. Online translator available.
| |||