Dear all,
included in the SPOT distribution is the tool "ltl2tgba" that converts LTL
formulas to equivalent Büchi automata. For the research I am currently
working on, I need to convert LTL formulas to as-small-as-possible Büchi
automata (that are not transition-based, so I am using the tool with the
"-N" parameter to obtain SPIN never-claims). So far, for all my
benchmarks, I am calling the tool with the following parameter
combinations:
ltl2tgba -N -R3 -r4
ltl2tgba -N -R3 -r7
ltl2tgba -N -R3 -r4
ltl2tgba -N -R3 -r7
ltl2tgba -N -R3 -r4
ltl2tgba -N -R3 -r7
After that, I take the smallest automata obtained. So far, I am only
interested in the number of states.
Now my question is: Given that I have enough time, which other parameter
combinations might lead to automata that that are smaller than any
automaton obtained when using the parameter combinations given above? As
an example, can it be the case that "-R2q" is sometimes better than "-R3"?
Phrased in other words, I'd like to know some set of parameter
combinations "A" such that for all LTL formulas "f", I can simply run
"ltl2tgba" on "f" trying all parameters combinations in "A" and take the
minimal automaton found. For the resulting automaton, it should be assured
that there's no smaller automaton obtainable with "ltl2tgba" from "f" for
any possible parameter combination. At the same time, "A" should be as
small as possible.
I hope that someone finds some time to reply and apologies for using the
SPOT framework in such a restricted way.
Best regards,
Ruediger Ehlers
We're pleased to announce the release of Spot 0.5.
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 release includes more than two year of work, with contributions
from Damien Lefortier, Guillaume Sadegh, Félix Abecassis, and
Alexandre Duret-Lutz. We would also like to thank Akim Demaille,
Denis Poitrenaud, and Kristin Y. Rozier for their bug reports and
help.
You can find the new release here:
http://spot.lip6.fr/dl/spot-0.5.tar.gz
Before listing what is new in this release, let me mention that we
have setup two mailing lists so you can stay informed, or discuss spot:
- <spot-announce(a)lrde.epita.fr> is read-only and will be used to
announce new releases. You may subscribe at
https://www.lrde.epita.fr/mailman/listinfo/spot-announce
- <spot(a)lrde.epita.fr> can be used to discuss anything related to
Spot. You may subscribe at
https://www.lrde.epita.fr/mailman/listinfo/spot-announce
What is new in spot 0.5 (2010-02-01):
* Two new LTL translations have been implemented:
- eltl_to_tgba_lacim() is a symbolic translation for ELTL based on
Couvreur's LaCIM'00 paper. For this translation (available with
ltl2tgba's option -le), all operators are described as finite
automata. A default set of operators is provided for LTL
(option -lo) and user may add more automaton operators.
- ltl_to_taa() is a translation based on Tauriainen's PhD thesis.
LTL is translated to "self-loop" alternating automata
and then to Transition-based Generalized Automata. (ltl2tgba's
option -taa).
The "Couvreur/FM" translation remains the best LTL translation
available in Spot.
* The data structures used to represent LTL formulae have been
overhauled, and it resulted in a big performence improvement
(in time and memory consumption) for the LTL translation.
* Two complementation algorithms for state-based Büchi automata
have been implemented:
- tgba_kv_complement is an on-the-fly implementation of the
Kupferman-Vardi construction (TCS'05) for generalized acceptance
conditions.
- tgba_safra_complement is an implementation of Safra's
complementation. This algorithm takes a degeneralized Büchi
automaton as input, but our implementation for the Streett->Büchi
step will produce a generalized automaton in the end.
* ltl2tgba has gained several options and the help text has been
reorganized. Please run src/tgbatest/ltl2tgba without arguments
for details. Couvreur/FM is now the default translation.
* The ltl2tgba.py CGI script can now run standalone. It also offers
the Tauriainen/TAA translation, and some options for SCC-based
reductions.
* Automata using BDD-encoded transitions relation can now be pruned
for useless states symbolically using the delete_unaccepting_scc()
function. This is ltl2tgba's -R3b option.
* The SCC-based simplification (ltl2tgba's -R3 option) has been
rewritten and improved.
* The "*" symbol, previously parsed as a synonym for "&" is no
longer recognized. This makes room for an upcoming support of
rational operators.
* More benchmarks in the bench/ directory:
- gspn-ssp/ some benchmarks published at ACSD'07,
- ltlcounter/ translation of a class of LTL formulae used by
Rozier & Vardi at SPIN'07
- scc-stats/ SCC statistics after translation of LTL formulae
- split-product/ parallelizing gain after splitting LTL automata
* An experimental Kripke interface has been developed to simplify
the integration of third party tools that do not use acceptance
conditions and that have label on states instead of transitions.
This interface has not been used yet.
* Experimental interface with the Nips virtual machine.
It is not very useful as Spot isn't able to retrieve any property
information from the model. This will just check assertions.
* Distribution:
- The Boost C++ library is now required.
- Update to Autoconf 2.65, Automake 1.11.1, Libtool 2.2.6b,
Bison 2.4.1, and Swig 1.3.40.
- Thanks to the newest Automake, "make check" will now
run in parallel if you use "make -j2 check" or more.
* Bug fixes:
- Disable warnings from the garbage collection of BuDDy, it
could break the standard output of ltl2tgba.
- Fix several C++ constructs to ensure Spot will build with
GCC 4.3, 4.4, and older 3.x releases, as well as with Intel's
ICC compiler.
- A very old bug in the hash function for LTL formulae caused Spot
to sometimes (but very rarely) consider two different LTL formulae
as equal.
--
Alexandre Duret-Lutz
