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
I am happy to announce that the following paper has been accepted in
the International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR’15) :
SAT-based Minimization of Deterministic ω-Automata
Souheib Baarir and Alexandre Duret-Lutz.
LRDE, EPITA, Le Kremlin-Bicêtre, France
A+,
Soheib.
