LTL2ABA

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.


How it works

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.

Download

The Ocaml source code is available here (5 KBytes).

The generated documentation is available here (PDF, 77 KBytes). (Also contains the source.)

Copyright

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
Valid HTML 4.0