Aalta is a tool that can translates the LTL formulas to the equivalent Buchi automata. The implementation is achieved by using C++ under the Ubuntu 12.10 operating system. Currently only the binary code is supported here.
Since Aalta uses the LTL parser from SPOT , so it has the same input format with SPOT. However, Aalta now only support the U (until), R (Release), X (Next), G (Global) and F (Future) temporal operators. For more input information, please refer to SPOT wiki.
The output of Aalta follows the promela format that is used in SPIN model checker.
If you find any bugs in Aalta, please contact us.
Department: Software Engineering Institute, East China Normal University
Address: NO.3663, North Zhongshan Road, Shanghai, China
.Alexandre Duret-Lutz and Denis Poitrenaud. Spot: an extensible model checking library using transition-based generalized Buchi automata. In MASCOTS’04, pages 76-83, 2004.
.Gerard J. Holzmann. The model checker SPIN. In IEEE Transactions on Software Engineering, pages 279-295, 1997.