We are pleased to announce the release of Spot 0.9.1. Spot is a model-checking library developed collaboratively by LRDE and LIP6. It provides algorithms and data structures to implement the automata-theoretic approach to LTL model checking. This maintenance release fixes a couple of bugs, and improves the speed of the translation slightly. You can find the new release here: http://spot.lip6.fr/dl/spot-0.9.1.tar.gz An updated version of the translation benchmark has been put here: http://spot.lip6.fr/dl/bench-0.9.1.pdf New in spot 0.9.1 (2012-05-23): * The version of LBTT we distribute includes a patch from Tomáš Babiak to count the number of non-deterministic states, and the number of deterministic automata produced. See lbtt/NEWS for the list of other differences with the original version of LBTT 1.2.1. * The Couvreur/FM translator has learned two new tricks. These only help to speedup the translation by not issuing states or acceptance conditions that would be latter suppresed by other optimizations. - The translation rules used to translate subformulae of the G operator have been adjusted not to produce useless loops already implied by G. This generalizes the "GF" trick presented in Couvreur's original FM'99 paper. - Promises generated for formula of the form P(a U (b U c)) are reduced into P(c), avoiding the introduction of many promises that imply each other. * The tgba_parse() function is now available via the Python bindings. * Bug fixes: - The random SERE generator was using the wrong operators for "and" and "or", mistaking And/Or with AndRat/OrRat. - The translation of !{r} was incorrect when this subformula was recurring (e.g. in G!{r}) and r had loops. - Correctly recognize ltl2tgba's option -rL. - Using LTL simplification rules based on syntactic implication, or based on language containment checks, caused BDD variables to be allocated in an "unnatural" order, resulting in a slower translation and a less optimal degeneralization. - When ltl2tgba reads a neverclaim, it now considers the resulting TGBA as a Büchi automaton, and will display double circles in the dotty output.