Aalta tool

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.

Aalta input

Since Aalta uses the LTL parser from SPOT [1], 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.

Aalta output

The output of Aalta follows the promela format that is used in SPIN[2] model checker.

Bug report

If you find any bugs in Aalta, please contact us.

Contact us

Email: lijwen2748@gmail.com

MSN: lijwen2748@gmail.com

Department: Software Engineering Institute, East China Normal University

Address: NO.3663, North Zhongshan Road, Shanghai, China


[1].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.

[2].Gerard J. Holzmann. The model checker SPIN. In IEEE Transactions on Software Engineering, pages 279-295, 1997.

Leave a Reply

Your email address will not be published. Required fields are marked *

You may use these HTML tags and attributes:

<a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <s> <strike> <strong>