I am happy to announce that the following two papers have been
accepted at the 22nd International SPIN Symposium on Model Checking of
Software (SPIN 2015) to be held in Stellenbosch, South Africa on 24–26
August 2015.
---
On Refinement of Büchi Automata for Explicit Model Checking
František Blahoudek¹, Alexandre Duret-Lutz²,
Vojtěch Rujbr¹, and Jan Strejček¹
¹Faculty of Informatics, Masaryk University, Brno, Czech Republic
²LRDE, EPITA, Le Kremlin-Bicêtre, France
https://www.lrde.epita.fr/wiki/Publications/blahoudek.15.spin
Abstract:
In explicit model checking, systems are typically described in an
implicit and compact way. Some valid information about the system
can be easily derived directly from this description, for example
that some atomic propositions cannot be valid at the same time. The
paper shows several ways to apply this information to improve the
Büchi automaton built from an LTL specification. As a result, we get
smaller automata with shorter edge labels that are easier to
understand andmore importantly, for which the explicit model
checking process performs better.
---
Practical Stutter-Invariance Checks for ω-Regular Languages
Thibaud Michaud and Alexandre Duret-Lutz
LRDE, EPITA, Le Kremlin-Bicêtre, France
https://www.lrde.epita.fr/wiki/Publications/michaud.15.spin
Abstract:
We propose several automata-based constructions that check whether a
specification is stutter-invariant. These constructions assume that
a specification and its negation can be translated into Büchi
automata, but aside from that, they are independent of the
specification formalism. These transformations were inspired by a
construction due to Holzmann and Kupferman, but that we broke down
into two operations that can have different realizations, and that
can be combined in different ways. As it turns out, implementing
only one of these operations is needed to obtain a functional
stutter-invariant check. Finally we have implemented these
techniques in a tool so that users can easily check whether an LTL
or PSL formula is stutter-invariant.
--
Alexandre Duret-Lutz
Bonjour,
nous avons le plaisir de vous annoncer la sortie du n°33 du bulletin du LRDE.
C'est un numéro spécial dédié aux séminaires des étudiants-chercheurs du LRDE
qui auront lieu le lundi 6 juillet 2015.
Vous y trouverez le programme des deux demi-journées avec les résumés des
présentations.
Nous y présentons également les nouveaux stagiaires et les futurs thésards qui nous
ont rejoints cette année.
Vous pouvez télécharger le bulletin en couleur à la page suivante :
http://www.lrde.epita.fr/wiki/LrdeBulletin/l-air-de-rien-33
--
Daniela Becker
