LTL2ABA is an Ocaml program that converts an LTL formula into an alternating Buchi automaton.
This is work in progress. Ultimately, I want to have a translator from LTL to Buchi automata via alternating automata. My second goal of this exercise was to study the Ocaml literate programming facility as well as some features of the Ocaml language, such as lexing and parsing.
The program is usable right now, but far from mature. So download and test it if you like, but do not expect production code. It is my toy, but may be useful to you.
Formulas need to be given using prefix notaton. The following constructs are available:
ltl_formula ::= True | False | s | ( ltl_formula ) | G ltl_formula | F ltl_formula | X ltl_formula | ltl_formula & ltl_formula | ltl_formula | ltl_formula | - ltl_formula | ltl_formula U ltl_formula | ltl_formula <-> ltl_formula | ltl_formula -> ltl_formula
where s is an alphanumeric string. For example, you can use the program like this:
$ ./ltl2aba "G (-a | F b)"
which results in
[(Glob (Or (Neg (Var "a"), Ev (Var "b")))), [], (Glob (Or (Neg (Var "a"), Ev (Var "b"))))] [(Glob (Or (Neg (Var "a"), Ev (Var "b")))), [Var "b"], (Glob (Or (Neg (Var "a"), Ev (Var "b"))))] [(Glob (Or (Neg (Var "a"), Ev (Var "b")))), [Var "a"], (And (Ev (Var "b"), Glob (Or (Neg (Var "a"), Ev (Var "b")))))] [(Glob (Or (Neg (Var "a"), Ev (Var "b")))), [Var "a"; Var "b"], (Glob (Or (Neg (Var "a"), Ev (Var "b"))))] [(Ev (Var "b")), [], (Ev (Var "b"))] [(Ev (Var "b")), [Var "b"], (True)] [(Ev (Var "b")), [Var "a"], (Ev (Var "b"))] [(Ev (Var "b")), [Var "a"; Var "b"], (True)]
This is the transition table of an alternating automaton corresponding to the above formula in prefix notation.
The Ocaml source code is available here (5 KBytes).
The generated documentation is available here (PDF, 77 KBytes). (Also contains the source.)
Copyright © 2008 by Andreas Bauer
LTL2ABA is released under the terms of the GNU General Public License.
Andreas Bauer, <baueran@rsise.anu.edu.au> Last modified: Wed May 7 22:19:03 2008 |