Feature #720

ltl2ba update

Added by Jaco van de Pol about 7 years ago. Updated over 6 years ago.

Status:NewStart date:09 Jul 2013
Priority:NormalDue date:
Assignee:-% Done:

0%

Category:toolsSpent time:-
Target version:-

Description

We should add the best tools to translate LTL to Buchi automata, ltl3ba and ltl2tgba.
This should result in faster LTL model checken, since they produce better Buchi automata
(smaller, more deterministic).

This should be added as flag to the LTL layer (--ltl), in the form of: --ltl2ba={ltl2ba,ltl3ba,ltl2tgba}
ltl3ba is from Jan Strejcek. ltl2tgba is from Alexander Duret-Lutz. I will add his information
on this ticket separately.

History

#1 Updated by Jaco van de Pol about 7 years ago

Information from Alexander Duret-Lutz:

Some pointers to follow up on tonight's diner (SPIN 2013 - Stony Brook)

ltl3ba is a better replacement for ltl2ba (faster processings, smaller automata)
- source code: http://sourceforge.net/projects/ltl3ba/files/ltl3ba/
- paper: http://arxiv.org/abs/1201.0682 (Full version from their
TACAS'12 paper)

Spot is a model checking library that includes a command-line tool
called ltl2tgba,
that can produce output compatible with ltl2ba/ltl3ba when given the
--spin option.
It implements more simplifications than ltl3ba, but in general it
takes more time.
It can also translate PSL formulae.
- source code: http://spot.lip6.fr/wiki/GetSpot
- doc: http://spot.lip6.fr/userdoc/ltl2tgba.html
- paper: http://www.lrde.epita.fr/~adl/dl/adl/duret.11.vecos.pdf (VECOS'11)

#2 Updated by Alfons Laarman over 6 years ago

note that the goal of the current implementation was to obtain similar state counts to competitive model checkers such as spin and divine, in order to do experimental comparisons. Therefore, an optional interface to different buchi translators would be useful.

#3 Updated by Alfons Laarman over 6 years ago

Esparza and K?etínský have a new method which results in completely deterministic (and small) "Buchi" automata:
http://arxiv.org/abs/1402.3388
(deterministic results tend to reduce the size of the cross product)

http://www.model.in.tum.de/~kretinsk/LTLdeterminization.html

Also available in: Atom PDF