NewsLetter 38 - September 24, 2003:
LTL to Buchi Automata Converters
Stefano Tonetta and Roberto Sebastiani have announced the availability of their tool called Modella (short for More Deterministic LTL to Automata), which can be used for the conversion of LTL formula into Buchi Automata.
Documentation, test results, and source code for the new tool are available from: http://www.science.unitn.it/~stonetta/modella.html
Besides the algorithm that is builtin to SPIN itself, include the ltl2ba tool developed by Denis Oddoux and Paul Gastin, written in C: http://spinroot.com/spin/Src/ltl2ba.tar.gz and the ``Temporal Massage Parlor'' tool written by Kousha Etessami, written in ML: http://www.bell-labs.com/topic/swdist/.
The New Book
The new Spin book is now finally available at all online booksellers.
The Spin Model Checker Primer and Reference Manual. Gerard J. Holzmann Addison-Wesley, ISBN 0-32122-862-6, 608 pgs.You can order the book at, for instance:
End of Newsletter Nr. 38.
To subscribe/unsubscribe: [email protected]