adl.bib
@inproceedings{baarir.04.mascots,
author = {Souheib Baarir and Jean-Michel Ili{\'e} and Alexandre
Duret-Lutz},
title = {Improving Reachability Analysis for Partially Symmetric
High Level Petri Nets},
booktitle = {Proceedings of the Poster Session of the 12th IEEE/ACM
International Symposium on Modeling, Analysis, and
Simulation of Computer and Telecommunication Systems
(MASCOTS'04)},
editors = {Pete Harrison and Doug DeGroot},
year = {2004},
address = {Volendam, The Netherlands},
month = oct,
pages = {5--8},
pdf = {adl/baarir.04.mascots.pdf},
poster = {adl/baarir.04.mascots.poster.pdf},
doi = {10.1109/MASCOT.2004.6}
}
@techreport{baarir.06.tr03,
author = {Souheib Baarir and Alexandre Duret-Lutz},
title = {Emptiness Check of Powerset {B\"u}chi Automata},
institution = {Universit{\'e} Pierre et Marie Curie, LIP6-CNRS},
year = {2006},
type = {Technical report},
number = {2006/003},
address = {Paris, France},
month = oct,
pdf = {adl/baarir.06.tr03.pdf},
abstract = {A possible attack on the state explosion of the
automata-theoretic approach to model-checking is to build
an automaton B whose states represent sets of states of the
original automaton A to check for emptiness. This paper
introduces two emptiness checks for B{\"u}chi automata
whose states represent sets that may include each other.
The first check on B is equivalent to a traditional
emptiness check on A but uses inclusion tests to direct and
further reduce the on-the-fly construction of B. The second
check is impressively faster but may return false
negatives. We illustrate and benchmark both using a
symmetry-based reduction.}
}
@inproceedings{baarir.07.acsd,
author = {Souheib Baarir and Alexandre Duret-Lutz},
title = {Emptiness Check of Powerset {B\"u}chi Automata},
booktitle = {Proceedings of the 7th International Conference on
Application of Concurrency to System Design (ACSD'07)},
editors = {Twan Basten and Gabriel Juh{\'a}s and Sandeep Shukla},
year = {2007},
month = jul,
pages = {41--50},
publisher = {IEEE Computer Society},
pdf = {adl/baarir.07.acsd.pdf},
slides = {adl/baarir.07.acsd.slides.pdf},
abstract = {We introduce two emptiness checks for B{\"u}chi automata
whose states represent sets that may include each other.
The first is equivalent to a traditional emptiness check
but uses inclusion tests to direct the on-the-fly
construction of the automaton. The second is impressively
faster but may return false negatives. We illustrate and
benchmark the improvement on a symmetry-based reduction.},
doi = {10.1109/ACSD.2007.49}
}
@inproceedings{baarir.07.msr,
author = {Souheib Baarir and Alexandre Duret-Lutz},
title = {Test de vacuit{\'e} pour automates de {B\"u}chi
ensemblistes avec tests d'inclusion},
booktitle = {Actes du 6e Colloque Francophone sur la Mod{\'e}lisation
des Syst{\`e}mes R{\'e}actifs (MSR'07)},
editors = {Jean-Michel Muller and {\'E}ric Niel and Laurent
Pi{\'e}trac},
publisher = {Hermes-Lavoisier},
year = {2007},
month = oct,
pages = {19--34},
abstract = {Nous pr{\'e}sentons deux algorithmes d'emptiness check
pour les automates de B{\"u}chi dont les {\'e}tats sont des
ensembles qui peuvent s'inclure les uns les autres. Le
premier est {\'e}quivalent {\`a} un emptiness check
traditionnel, mais utilise des tests d'inclusion pour
diriger la construction {\`a} la vol{\'e}e de l'automate.
Le second est beaucoup plus rapide, mais peut retourner de
faux n{\'e}gatifs. Nous illustrons et {\'e}valuons
l'am{\'e}lioration avec une r{\'e}duction bas{\'e}e sur les
sym{\'e}tries.}
}
@inproceedings{baarir.14.forte,
author = {Souheib Baarir and Alexandre Duret-Lutz},
title = {Mechanizing the Minimization of Deterministic Generalized
{B\"u}chi Automata},
booktitle = {Proceedings of the 34th IFIP International Conference on
Formal Techniques for Distributed Objects, Components and
Systems (FORTE'14)},
year = {2014},
month = jun,
pages = {266--283},
publisher = {Springer},
pdf = {adl/baarir.14.forte.pdf},
slides = {adl/baarir.14.forte.slides.pdf},
series = {Lecture Notes in Computer Science},
volume = {8461},
abstract = {Deterministic B{\"u}chi automata (DBA) are useful to
(probabilistic) model checking and synthesis. We survey
techniques used to obtain and minimize DBAs for different
classes of properties. We extend these techniques to
support DBA that have generalized and transition-based
acceptance (DTGBA) as they can be even smaller. Our
minimization technique---a reduction to a SAT
problem---synthesizes a DTGBA equivalent to the input DTGBA
for any given number of states and number of acceptance
sets (assuming such automaton exists). We present
benchmarks using a framework that implements all these
techniques.},
doi = {10.1007/978-3-662-43613-4_17}
}
@inproceedings{baarir.15.lpar,
author = {Souheib Baarir and Alexandre Duret-Lutz},
booktitle = {Proceedings of the 20th International Conference on Logic
for Programming, Artificial Intelligence, and Reasoning
(LPAR-20)},
title = {{SAT}-based Minimization of Deterministic
$\omega$-Automata},
year = {2015},
month = nov,
pages = {79--87},
publisher = {Springer},
volume = {9450},
series = {Lecture Notes in Computer Science},
abstract = {We describe a tool that inputs a deterministic
$\omega$-automaton with any acceptance condition, and
synthesizes an equivalent $\omega$-automaton with another
arbitrary acceptance condition and a given number of
states, if such an automaton exists. This tool, that relies
on a SAT-based encoding of the problem, can be used to
provide minimal $\omega$-automata equivalent to given
properties, for different acceptance conditions.},
pdf = {adl/baarir.15.lpar.pdf},
doi = {10.1007/978-3-662-48899-7_6}
}
@inproceedings{babiak.13.spin,
author = {Tom{\'a}{\v{s}} Babiak and Thomas Badie and Alexandre
Duret-Lutz and Mojm{\'i}r K{\v{r}}et{\'i}nsk{\'y} and Jan
Strej{\v{c}}ek},
title = {Compositional Approach to Suspension and Other
Improvements to {LTL} Translation},
booktitle = {Proceedings of the 20th International SPIN Symposium on
Model Checking of Software (SPIN'13)},
year = 2013,
volume = {7976},
series = {Lecture Notes in Computer Science},
pages = {81--98},
month = jul,
publisher = {Springer},
abstract = {Recently, there was defined a fragment of LTL (containing
fairness properties among other interesting formulae) whose
validity over a given infinite word depends only on an
arbitrary suffix of the word. Building upon an existing
translation from LTL to B{\"u}chi automata, we introduce a
compositional approach where subformulae of this fragment
are translated separately from the rest of an input formula
and the produced automata are composed in a way that the
subformulae are checked only in relevant accepting strongly
connected components of the final automaton. Further, we
suggest improvements over some procedures commonly applied
to generalized B{\"u}chi automata, namely over generalized
acceptance simplification and over degeneralization.
Finally we show how existing simulation-based reductions
can be implemented in a signature-based framework in a way
that improves the determinism of the automaton.},
pdf = {adl/babiak.13.spin.pdf},
slides = {adl/babiak.13.spin.slides.pdf},
doi = {10.1007/978-3-642-39176-7_6}
}
@inproceedings{babiak.15.cav,
author = {Tom{\'{a}\v{s}} Babiak and Franti{\v{s}}ek Blahoudek and
Alexandre Duret-Lutz and Joachim Klein and Jan K{\v
r}et{\'{\i}}nsk{\'{y}} and David M{\"u}ller and David
Parker and Jan Strej{\v{c}}ek},
title = {The {H}anoi {O}mega-{A}utomata Format},
booktitle = {Proceedings of the 27th International Conference on
Computer Aided Verification (CAV'15)},
year = 2015,
volume = {9206},
series = {Lecture Notes in Computer Science},
pages = {479--486},
month = jul,
publisher = {Springer},
abstract = { We propose a flexible exchange format for
$\omega$-automata, as typically used in formal
verification, and implement support for it in a range of
established tools. Our aim is to simplify the interaction
of tools, helping the research community to build upon
other people's work. A key feature of the format is the use
of very generic acceptance conditions, specified by Boolean
combinations of acceptance primitives, rather than being
limited to common cases such as B\"uchi, Streett, or Rabin.
Such flexibility in the choice of acceptance conditions can
be exploited in applications, for example in probabilistic
model checking, and furthermore encourages the development
of acceptance-agnostic tools for automata manipulations.
The format allows acceptance conditions that are either
state-based or transition-based, and also supports
alternating automata.},
doi = {10.1007/978-3-319-21690-4_31},
pdf = {adl/babiak.15.cav.pdf},
poster = {adl/babiak.15.cav.poster.pdf},
slides = {adl/babiak.15.cav.slides.pdf}
}
@inproceedings{baier.19.atva,
author = {Christel Baier and Franti\v{s}ek Blahoudek and Alexandre
Duret-Lutz and Joachim Klein and David M\"uller and Jan
Strej\v{c}ek},
title = {Generic Emptiness Check for Fun and Profit},
booktitle = {Proceedings of the 17th International Symposium on
Automated Technology for Verification and Analysis
(ATVA'19)},
year = {2019},
volume = {11781},
series = {Lecture Notes in Computer Science},
pages = {445--461},
month = oct,
publisher = {Springer},
abstract = {We present a new algorithm for checking the emptiness of
$\omega$-automata with an Emerson-Lei acceptance condition
(i.e., a positive Boolean formula over sets of states or
transitions that must be visited infinitely or finitely
often). The algorithm can also solve the model checking
problem of probabilistic positiveness of MDP under a
property given as a deterministic Emerson-Lei automaton.
Although both these problems are known to be NP-complete
and our algorithm is exponential in general, it runs in
polynomial time for simpler acceptance conditions like
generalized Rabin, Streett, or parity. In fact, the
algorithm provides a unifying view on emptiness checks for
these simpler automata classes. We have implemented the
algorithm in Spot and PRISM and our experiments show
improved performance over previous solutions.},
pdf = {adl/baier.19.atva.pdf},
slides = {adl/baier.19.atva.slides.mefosyloma.pdf},
slides2 = {adl/baier.19.atva.slides.pdf},
doi = {10.1007/978-3-030-31784-3_26}
}
@incollection{barnat.18.hpcr,
author = {Jiri Barnat and Vincent Bloemen and Alexandre Duret-Lutz
and Alfons Laarman and Laure Petrucci and Jaco van de Pol
and Etienne Renault},
editor = {Youssef Hamadi and Lakhdar Sais},
title = {Parallel Model Checking Algorithms for Linear-Time
Temporal Logic},
booktitle = {Handbook of Parallel Constraint Reasoning},
year = {2018},
publisher = {Springer International Publishing},
address = {Cham},
chapter = 12,
pages = {457--507},
abstract = {Model checking is a fully automated, formal method for
demonstrating absence of bugs in reactive systems. Here,
bugs are violations of properties in Linear-time Temporal
Logic (LTL). A fundamental challenge to its application is
the exponential explosion in the number of system states.
The current chapter discusses the use of parallelism in
order to overcome this challenge. We reiterate the textbook
automata-theoretic approach, which reduces the model
checking problem to the graph problem of finding cycles. We
discuss several parallel algorithms that attack this
problem in various ways, each with different
characteristics: Depth-first search (DFS) based algorithms
rely on heuristics for good parallelization, but exhibit a
low complexity and good on-the-fly behavior. Breadth-first
search (BFS) based approaches, on the other hand, offer
good parallel scalability and support distributed
parallelism. In addition, we present various simpler model
checking tasks, which still solve a large and important
subset of the LTL model checking problem, and show how
these can be exploited to yield more efficient algorithms.
In particular, we provide simplified DFS-based search
algorithms and show that the BFS-based algorithms exhibit
optimal runtimes in certain cases.},
isbn = {978-3-319-63516-3},
doi = {10.1007/978-3-319-63516-3_12},
pdf = {adl/barnat.18.hpcr.pdf}
}
@inproceedings{bensalem.11.sumo,
author = {Ala Eddine Ben{ S}alem and Alexandre Duret-Lutz and
Fabrice Kordon},
title = {Generalized {B\"u}chi Automata versus Testing Automata for
Model Checking},
booktitle = {Proceedings of the second International Workshop on
Scalable and Usable Model Checking for Petri Net and other
models of Concurrency (SUMO'11)},
address = {Newcastle, UK},
year = {2011},
month = jun,
volume = {726},
publisher = {CEUR},
series = {Workshop Proceedings},
pdf = {adl/bensalem.11.sumo.pdf},
abstract = {Geldenhuys and Hansen have shown that a kind of
$\omega$-automaton known as \emph{testing automata} can
outperform the B{\"u}chi automata traditionally used in the
automata-theoretic approach to model checking. This work
completes their experiments by including a comparison with
generalized B{\"u}chi automata; by using larger state
spaces derived from Petri nets; and by distinguishing
violated formul\ae{} (for which testing automata fare
better) from verified formul\ae{} (where testing automata
are hindered by their two-pass emptiness check).}
}
@article{bensalem.12.topnoc,
author = {Ala Eddine Ben{ S}alem and Alexandre Duret-Lutz and
Fabrice Kordon},
title = {Model Checking using Generalized Testing Automata},
journal = {Transactions on Petri Nets and Other Models of Concurrency
(ToPNoC VI)},
volume = 7400,
series = {Lecture Notes in Computer Science},
year = 2012,
publisher = {Springer},
pages = {94--112},
pdf = {adl/bensalem.12.topnoc.pdf},
abstract = {Geldenhuys and Hansen showed that a kind of
$\omega$-automata known as \emph{Testing Automata} (TA)
can, in the case of stuttering-insensitive properties,
outperform the B{\"u}chi automata traditionally used in the
automata-theoretic approach to model checking. \par In
previous work, we compared TA against
\emph{Transition-based Generalized B{\"u}chi Automata}
(TGBA), and concluded that TA were more interesting when
counterexamples were expected, otherwise TGBA were more
efficient. \par In this work we introduce a new kind of
automata, dubbed \emph{Transition-based Generalized Testing
Automata} (TGTA), that combine ideas from TA and TGBA.
Implementation and experimentation of TGTA show that they
outperform other approaches in most of the cases.},
doi = {10.1007/978-3-642-35179-2_5}
}
@inproceedings{bensalem.14.tacas,
author = {Ala Eddine Ben{ S}alem and Alexandre Duret-Lutz and
Fabrice Kordon and Yann Thierry-Mieg},
title = {Symbolic Model Checking of Stutter Invariant Properties
Using Generalized Testing Automata},
booktitle = {Proceedings of the 20th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems
(TACAS'14)},
year = {2014},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {8413},
pages = {440--454},
address = {Grenoble, France},
month = apr,
abstract = {In a previous work, we showed that a kind of
$\omega$-automata known as \emph{Tran\-sition-based
Generalized Testing Automata} (TGTA) can outperform the
B{\"u}chi automata traditionally used for \textit{explicit}
model checking when verifying stutter-invariant properties.
In this work, we investigate the use of these generalized
testing automata to improve \textit{symbolic} model
checking of stutter-invariant LTL properties. We propose an
efficient symbolic encoding of stuttering transitions in
the product between a model and a TGTA. Saturation
techniques available for decision diagrams then benefit
from the presence of stuttering self-loops on all states of
TGTA. Experimentation of this approach confirms that it
outperforms the symbolic approach based on
(transition-based) Generalized B{\"u}chi Automata.},
pdf = {adl/bensalem.14.tacas.pdf},
doi = {10.1007/978-3-642-54862-8_38}
}
@inproceedings{blahoudek.14.spin,
author = {Franti\v{s}ek Blahoudek and Alexandre Duret-Lutz and
Mojm\'{i}r K\v{r}et\'{i}nsk\'{y} and Jan Strej\v{c}ek},
title = {Is There a Best {B\"u}chi Automaton for Explicit Model
Checking?},
booktitle = {Proceedings of the 21th International SPIN Symposium on
Model Checking of Software (SPIN'14)},
year = {2014},
publisher = {ACM},
pages = {68--76},
month = jul,
abstract = {LTL to B{\"u}chi automata (BA) translators are
traditionally optimized to produce automata with a small
number of states or a small number of non-deterministic
states. In this paper, we search for properties of
B{\"u}chi automata that really influence the performance of
explicit model checkers. We do that by manual analysis of
several automata and by experiments with common LTL-to-BA
translators and realistic verification tasks. As a result
of these experiences, we gain a better insight into the
characteristics of automata that work well with Spin.},
pdf = {adl/blahoudek.14.spin.pdf},
doi = {10.1145/2632362.2632377}
}
@inproceedings{blahoudek.15.spin,
author = {Franti\v{s}ek Blahoudek and Alexandre Duret-Lutz and
Vojt\v{c}ech Rujbr and Jan Strej\v{c}ek},
title = {On Refinement of {B\"u}chi Automata for Explicit Model
Checking},
booktitle = {Proceedings of the 22th International SPIN Symposium on
Model Checking of Software (SPIN'15)},
year = 2015,
pages = {66--83},
month = aug,
series = {Lecture Notes in Computer Science},
volume = 9232,
publisher = {Springer},
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{\"u}chi automaton built from an LTL specification. As a
result, we get smaller automata with shorter edge labels
that are easier to understand and, more importantly, for
which the explicit model checking process performs better.},
pdf = {adl/blahoudek.15.spin.pdf},
doi = {10.1007/978-3-319-23404-5_6}
}
@inproceedings{blahoudek.17.lpar,
author = {Franti\v{s}ek Blahoudek and Alexandre Duret-Lutz and
Mikul\'{a}\v{s} Kloko\v{c}ka and Mojm\'{\i}r
K\v{r}et\'{\i}nsk\'{y} and Jan Strej\v{c}ek},
title = {Seminator: A Tool for Semi-Determinization of
Omega-Automata},
booktitle = {Proceedings of the 21th International Conference on Logic
for Programming, Artificial Intelligence, and Reasoning
(LPAR-21)},
year = {2017},
editor = {Thomas Eiter and David Sands and Geoff Sutcliffe},
volume = {46},
series = {EPiC Series in Computing},
pages = {356--367},
month = may,
publisher = {EasyChair Publications},
pdf = {adl/blahoudek.17.lpar.pdf},
abstract = {We present a tool that transforms nondeterministic
$\omega$-automata to semi-deterministic $\omega$-automata.
The tool Seminator accepts transition-based generalized
B\"uchi automata (TGBA) as an input and produces automata
with two kinds of semi-determinism. The implemented
procedure performs degeneralization and
semi-determinization simultaneously and employs several
other optimizations. We experimentally evaluate Seminator
in the context of LTL to semi-deterministic automata
translation.},
doi = {10.29007/k5nl}
}
@inproceedings{blahoudek.20.cav,
author = {Franti\v{s}ek Blahoudek and Alexandre Duret-Lutz and Jan
Strej\v{c}ek},
title = {{S}eminator~2 Can Complement Generalized {B\"u}chi
Automata via Improved Semi-Determinization},
booktitle = {Proceedings of the 32nd International Conference on
Computer-Aided Verification (CAV'20)},
year = {2020},
publisher = {Springer},
volume = {12225},
series = {Lecture Notes in Computer Science},
pages = {15--27},
month = jul,
abstract = {We present the second generation of the tool Seminator
that transforms transition-based generalized B{\"u}chi
automata (TGBAs) into equivalent semi-deterministic
automata. The tool has been extended with numerous
optimizations and produces considerably smaller automata
than its first version. In connection with the
state-of-the-art LTL to TGBAs translator Spot, Seminator~2
produces smaller (on average) semi-deterministic automata
than the direct LTL to semi-deterministic automata
translator \texttt{ltl2ldgba} of the Owl library. Further,
Seminator~2 has been extended with an improved NCSB
complementation procedure for semi-deterministic automata,
providing a new way to complement automata that is
competitive with state-of-the-art complementation tools.},
doi = {10.1007/978-3-030-53291-8_2},
pdf = {adl/blahoudek.20.cav.pdf},
slides = {adl/blahoudek.20.cav.slides.pdf},
talk = {adl/blahoudek.20.cav.talk.mp4},
teaser = {adl/blahoudek.20.cav.teaser.mp4}
}
@inproceedings{bloemen.17.spin,
author = {Vincent Bloemen and Alexandre Duret-Lutz and Jaco van de
Pol},
title = {Explicit State Model Checking with Generalized {B\"u}chi
and {R}abin Automata},
booktitle = {Proceedings of the 24th International SPIN Symposium on
Model Checking of Software (SPIN'17)},
pages = {50--59},
year = {2017},
publisher = {ACM},
month = jul,
pdf = {adl/bloemen.17.spin.pdf},
doi = {10.1145/3092282.3092288},
abstract = {In the automata theoretic approach to explicit state LTL
model checking, the synchronized product of the model and
an automaton that represents the negated formula is checked
for emptiness. In practice, a (transition-based
generalized) B\"uchi automaton (TGBA) is used for this
procedure.
This paper investigates whether using a more general form
of acceptance, namely transition-based generalized Rabin
automata (TGRAs), improves the model checking procedure.
TGRAs can have significantly fewer states than TGBAs,
however the corresponding emptiness checking procedure is
more involved. With recent advances in probabilistic model
checking and LTL to TGRA translators, it is only natural to
ask whether checking a TGRA directly is more advantageous
in practice.
We designed a multi-core TGRA checking algorithm and
performed experiments on a subset of the models and
formulas from the 2015 Model Checking Contest. We observed
that our algorithm can be used to replace a TGBA checking
algorithm without losing performance. In general, we found
little to no improvement by checking TGRAs directly.}
}
@article{bloemen.19.sttt,
author = {Vincent Bloemen and Alexandre Duret-Lutz and Jaco van de
Pol},
title = {Model checking with generalized {R}abin and {F}in-less
automata},
journal = {International Journal on Software Tools for Technology
Transfer},
publisher = {Springer},
year = {2019},
month = jun,
volume = 21,
number = 3,
pages = {307--324},
pdf = {adl/bloemen.19.sttt.pdf},
doi = {10.1007/s10009-019-00508-4},
abstract = { In the automata theoretic approach to explicit state LTL
model checking, the synchronized product of the model and
an automaton that represents the negated formula is checked
for emptiness. In practice, a (transition-based
generalized) B\"uchi automaton (TGBA) is used for this
procedure.
This paper investigates whether using a more general form
of acceptance, namely a transition-based generalized Rabin
automaton (TGRA), improves the model checking procedure.
TGRAs can have significantly fewer states than TGBAs,
however the corresponding emptiness checking procedure is
more involved. With recent advances in probabilistic model
checking and LTL to TGRA translators, it is only natural to
ask whether checking a TGRA directly is more advantageous
in practice.
We designed a multi-core TGRA checking algorithm and
performed experiments on a subset of the models and
formulas from the 2015 Model Checking Contest and generated
LTL formulas for models from the BEEM database. While we
found little to no improvement by checking TGRAs directly,
we show how various aspects of a TGRA's structure
influences the model checking performance.
In this paper, we also introduce a Fin-less acceptance
condition, which is a disjunction of TGBAs. We show how to
convert TGRAs into automata with Fin-less acceptance and
show how a TGBA emptiness procedure can be extended to
check Fin-less automata.
\textbf{Note:} This is an extended version
of~\cite{bloemen.17.spin}.}
}
@inproceedings{burrus.03.mpool,
author = {Nicolas Burrus and Alexandre Duret-Lutz and Thierry
G\'eraud and David Lesage and Rapha\"el Poss},
title = {A Static {C++} Object-Oriented Programming (SCOOP)
Paradigm Mixing Benefits of Traditional OOP and Generic
Programming},
booktitle = {Proceedings of the Workshop on Multiple Paradigm with OO
Languages (MPOOL'03)},
year = {2003},
address = {Anaheim, California},
month = oct,
pdf = {adl/burrus.03.mpool.pdf},
proceedings = {http://www.fz-juelich.de/nic-series/volume27/volume27.html},
abstract = {Object-oriented and generic programming are both supported
in C++. OOP provides high expressiveness whereas GP leads
to more efficient programs by avoiding dynamic typing. This
paper presents SCOOP, a new paradigm which enables both
classical OO design and high performance in C++ by mixing
OOP and GP. We show how classical and advanced OO features
such as virtual methods, multiple inheritance, argument
covariance, virtual types and multimethods can be
implemented in a fully statically typed model, hence
without run-time overhead.}
}
@inproceedings{casares.22.tacas,
author = {Antonio Casares and Alexandre Duret-Lutz and Klara J.
Meyer and Florian Renkin and Salomon Sickert},
title = {Practical Applications of the {A}lternating {C}ycle
{D}ecomposition},
booktitle = {Proceedings of the 28th International Conference on Tools
and Algorithms for the Construction and Analysis of
Systems},
year = {2022},
series = {Lecture Notes in Computer Science},
month = apr,
volume = {13244},
pdf = {adl/casares.22.tacas.pdf},
slides2 = {adl/casares.22.tacas.slides.pdf},
slides = {adl/casares.22.tacas.slides2.pdf},
pages = {99--117},
doi = {10.1007/978-3-030-99527-0_6},
abstract = {In 2021, Casares, Colcombet, and Fijalkow introduced the
Alternating Cycle Decomposition (ACD) to study properties
and transformations of Muller automata. We present the
first practical implementation of the ACD in two different
tools, Owl and Spot, and adapt it to the framework of
Emerson-Lei automata, i.e., $\omega$-automata whose
acceptance conditions are defined by Boolean formulas. The
ACD provides a transformation of Emerson-Lei automata into
parity automata with strong optimality guarantees: the
resulting parity automaton is minimal among those automata
that can be obtained by duplication of states. Our
empirical results show that this transformation is usable
in practice. Further, we show how the ACD can generalize
many other specialized constructions such as deciding
typeness of automata and degeneralization of generalized
B{\"u}chi automata, providing a framework of practical
algorithms for $\omega$-automata.}
}
@techreport{clouard.99.tr,
author = {R\'egis Clouard and Abderrahim Elmoataz and Fran\c{c}ois
Angot and Olivier Lezoray and Alexandre Duret-Lutz},
title = {Une biblioth\`eque et un environnement de programmation
d'op\'erateurs de traitement d'images},
institution = {GREYC-ISMRA},
year = {1999},
number = {99008},
address = {Caen, France},
month = nov,
url = {http://www.greyc.ismra.fr/~regis/Pandore/}
}
@inproceedings{couvreur.05.spin,
author = {Jean-Michel Couvreur and Alexandre Duret-Lutz and Denis
Poitrenaud},
title = {On-the-Fly Emptiness Checks for Generalized {B\"u}chi
Automata},
booktitle = {Proceedings of the 12th International SPIN Workshop on
Model Checking of Software},
pages = {143--158},
year = {2005},
editor = {Patrice Godefroid},
volume = {3639},
series = {Lecture Notes in Computer Science},
month = aug,
publisher = {Springer},
pdf = {adl/couvreur.05.spin.draft.pdf},
slides = {adl/couvreur.05.spin.slides.pdf},
abstract = { Emptiness check is a key operation in the
automata-theoretic approach to LTL verification. However,
it is usually done on B{\"u}chi automata with a single u
acceptance condition. We review existing on-the-fly
emptiness-check algorithms for generalized B{\"u}chi
automata (i.e., with multiple acceptance conditions) and u
show how they compete favorably with emptiness-checks for
degeneralized automata, especially in presence of weak
fairness assumptions. We also introduce a new
emptiness-check algorithm, some heuristics to improve
existing checks, and propose algorithms to compute
accepting runs in the case of multiple acceptance
conditions. },
doi = {10.1007/11537328_15}
}
@inproceedings{darbon.02.ismm,
author = {J\'er\^ome Darbon and Thierry G\'eraud and Alexandre
Duret-Lutz},
title = {Generic Implementation of Morphological Image Operators},
booktitle = {Mathematical Morphology, Proceedings of the 6th
International Symposium (ISMM)},
pages = {175--184},
year = {2002},
address = {Sydney, Australia},
month = apr,
publisher = {Sciro Publishing},
pdf = {adl/darbon.02.ismm.pdf},
abstract = { Several libraries dedicated to mathematical morphology
exist. But they lack genericity, that is to say, the
ability for operators to accept input of different
natures---2D binary images, graphs enclosing floating
values, etc. We describe solutions which are integrated in
Olena, a library providing morphological operators. We
demonstrate with some examples that translating
mathematical formulas and algorithms into source code is
made easy and safe with Olena. Moreover, experimental
results show that no extra costs at run-time are induced.
}
}
@inproceedings{demaille.08.fsmnlp,
author = {Akim Demaille and Alexandre Duret-Lutz and Florian Lesaint
and Sylvain Lombardy and Jacques Sakarovitch and Florent
Terrones},
title = {An {XML} format proposal for the description of weighted
automata, transducers, and regular expressions},
booktitle = {Proceedings of the seventh international workshop on
Finite-State Methods and Natural Language Processing
(FSMNLP'08)},
year = {2008},
address = {Ispra, Italia},
month = sep,
abstract = {We present an XML format that allows to describe a large
class of finite weighted automata and transducers. Our
design choices stem from our policy of making the
implementation as simple as possible. This format has been
tested for the communication between the modules of our
automata manipulation platform Vaucanson, but this document
is less an experiment report than a position paper intended
to open the discussion among the community of automata
software writers.},
pdf = {adl/demaille.08.fsmnlp.pdf}
}
@inproceedings{demaille.13.ciaa,
author = {Akim Demaille and Alexandre Duret-Lutz and Sylvain
Lombardy and Jacques Sakarovitch},
title = {Implementation Concepts in {V}aucanson 2},
booktitle = {Proceedings of Implementation and Application of Automata,
18th International Conference (CIAA'13)},
pages = {96--107},
year = 2013,
editor = {Oscar H. Ibarra and Zhe Dang},
publisher = {Springer},
volume = 2759,
series = {Lecture Notes in Computer Science},
address = {Santa Barbara, CA, USA},
month = jul,
project = {Vaucanson},
abstract = {Vaucanson is an open source C++ platform dedicated to the
computation with finite weighted automata. It is generic:
it allows to write algorithms that apply on a wide set of
mathematical objects. Initiated ten years ago, several
shortcomings were discovered along the years, especially
problems related to code complexity and obfuscation as well
as performance issues. This paper presents the concepts
underlying Vaucanson 2, a complete rewrite of the platform
that addresses these issues.},
pdf = {adl/demaille.13.ciaa.pdf},
doi = {10.1007/978-3-642-39274-0_12}
}
@inproceedings{demaille.14.ciaa,
author = {Akim Demaille and Alexandre Duret-Lutz and Sylvain
Lombardy and Luca Saiu and Jacques Sakarovitch},
title = {A Type System for Weighted Automata and Rational
Expressions},
booktitle = {Proceedings of Implementation and Application of Automata,
19th International Conference (CIAA'14)},
year = 2014,
fixmepublisher = {Springer},
fixmeseries = {Lecture Notes in Computer Science},
address = {Giessen, Germany},
month = jul,
abstract = {We present a type system for automata and rational
expressions, expressive enough to encompass weighted
automata and transducers in a single coherent formalism.
The system allows to express useful properties about the
applicability of operations including binary heterogeneous
functions over automata.\\ We apply the type system to the
design of the Vaucanson platform, a library dedicated to
the computation with finite weighted automata, in which
genericity and high efficiency are obtained at the lowest
level through the use of template metaprogramming, by
letting the template system play the role of a static type
system for automata. Between such a low-level layer and the
interactive high-level interface, the type system plays the
crucial role of a mediator and allows for a
cleanly-structured use of dynamic compilation. },
pdf = {adl/demaille.14.ciaa.pdf},
doi = {10.1007/978-3-319-08846-4_12}
}
@inproceedings{duret.00.gcseyrw,
author = {Alexandre Duret-Lutz},
title = {Olena: a Component-Based Platform for Image Processing,
mixing Generic, Generative and {OO} Programming},
booktitle = {Proceedings of 2nd International Symposium on Generative
and Component-Based Software Engineering (GCSE 2000)},
publisher = {Young Researchers Workshop (published in
``Net.ObjectDays2000'')},
year = {2000},
address = {Erfurt, Germany},
pages = {653--659},
month = oct,
url = {http://www.lrde.epita.fr/dload/papers/gcse00-yrw/olena.html}
}
@techreport{duret.00.tr01,
author = {Alexandre Duret-Lutz and Thierry G{\'e}raud},
title = {Improving Object-Oriented Generic Programming},
institution = {EPITA Research and Development Laboratory},
year = {2000},
type = {Technical Report},
number = {0001},
address = {Paris},
month = apr,
pdf = {adl/duret.00.tr01.pdf},
abstract = { Great efforts have gone into building scientific
libraries dedicated to particular application domains and a
main issue is to manage the large number of data types
involved in a given domain. An ideal algorithm
mplementation should be general: it should be written once
and process data in an abstract way. Moreover, it should be
efficient. For several years, some libraries have been
using generic programming to address this problem. In this
report, we present two major improvements of this paradigm.
\par In generic libraries, a concept is the description of
a set of requirements on a type that parameterizes an
algorithm implementation (the notion of concept replaces
the classical object-oriented notion of abstract class). A
problem is that, until now, concepts are only defined in
the documentation. We managed to make them explicit in the
program by representing a concept by a type; moreover,
(multiple) concept inheritance is fully supported. The
procedure signature thus evolves from \texttt{void
foo(AbstractA\&)} for classic object-orientation, and from
\texttt{template void foo(A\&)} for classic
generic programming, towards \texttt{template void
foo(ConceptA\&)}. This results in a better support of
procedure overloading, which is of prime importance for
libraries where each algorithm implementation can have
numerous variations. \par Another problem is that the
generic programming paradigm suffers from a lack of
appropriate design patterns. We observed that classical
patterns of Gamma et al. can be translated into this
paradigm while handling operation polymorphism by
parametric polymorphism. In these patterns, method calls
can be solved statically, because the inferior type of each
object in generic programming is known at compile-time. We
thus preserve their modularity and reusability properties
but we avoid the performance penalty due to their dynamic
behavior, which is a critical issue in numerical computing.
This results in better design capabilities for
object-oriented generic libraries. }
}
@inproceedings{duret.01.ae,
author = {Alexandre Duret-Lutz},
title = {Expression Templates in {Ada}},
booktitle = {Proceedings of the 6th International Conference on
Reliable Software Technologies (Ada-Europe'01)},
year = {2001},
address = {Leuven, Belgium},
month = may,
pages = {191--202},
volume = {2043},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
note = {Best paper award.},
pdf = {adl/duret.01.ae.pdf},
abstract = {High-order matrix or vector expressions tend to be
penalized by the use of huge temporary variables.
Expression templates is a C++ technique which can be used
to avoid these temporaries, in a way that is transparent to
the user. We present an Ada adaptation of this technique
which---while not transparent---addresses the same
efficiency issue as the original. We make intensive use of
the signature idiom to combine packages together, and
discuss its importance in generic programming. Finally, we
express some concerns about generic programming in Ada.},
doi = {10.1007/3-540-45136-6_15}
}
@inproceedings{duret.01.coots,
author = {Alexandre Duret-Lutz and Thierry G\'eraud and Akim
Demaille},
title = {Design Patterns for Generic Programming in {C++}},
booktitle = {Proceedings of the 6th USENIX Conference on
Object-Oriented Technologies and Systems (COOTS'01)},
year = {2001},
address = {San Antonio, Texas, USA},
month = jan,
pages = {189--202},
publisher = {USENIX Association},
pdf = {adl/duret.01.coots.pdf},
url = {http://www.usenix.org/publications/library/proceedings/coots01/duret.html},
abstract = {Generic programming is a paradigm whose wide adoption by
the C++ community is quite recent. In this scheme most
classes and procedures are parameterized, leading to the
construction of general and efficient software components.
In this paper, we show how some design patterns from Gamma
et al. can be adapted to this paradigm. Although these
patterns rely highly on dynamic binding, we show that, by
intensive use of parametric polymorphism, the method calls
in these patterns can be resolved at compile-time. In
intensive computations, the generic patterns bring a
significant speed-up compared to their classical peers. }
}
@mastersthesis{duret.03.msc,
author = {Alexandre Duret-Lutz and Rachid Rebiha},
title = {SPOT\,: une biblioth{\`e}que de v{\'e}rification de
propri{\'e}t{\'e}s de logique temporelle {\`a} temps
lin{\'e}aire},
school = {DEA Syst{\`e}mes Informatiques R{\'e}partis,
Universit{\'e} de Paris 6},
month = sep,
year = {2003},
pdf = {adl/duret.03.msc.pdf}
}
@inproceedings{duret.04.mascots,
author = {Alexandre Duret-Lutz and Denis Poitrenaud},
title = {SPOT: an Extensible Model Checking Library using
Transition-based Generalized {B\"u}chi Automata},
booktitle = {Proceedings of the 12th IEEE/ACM International Symposium
on Modeling, Analysis, and Simulation of Computer and
Telecommunication Systems (MASCOTS'04)},
editors = {Doug DeGroot and Pete Harrison},
year = {2004},
address = {Volendam, The Netherlands},
month = oct,
publisher = {IEEE Computer Society},
pages = {76--83},
pdf = {adl/duret.04.mascots.draft.pdf},
abstract = { Spot is a C++ library offering model checking bricks that
can be combined and interfaced with third party tools to
build a model checker. It relies on Transition-based
Generalized B{\"u}chi Automata (TGBA) and does not need to
degeneralize these automata to check their emptiness. We
motivate the choice of TGBA by illustrating a very simple
(yet efficient) translation of LTL into TGBA. We then show
how it supports on-the-fly computations, and how it can be
extended or integrated in other tools. },
doi = {10.1109/MASCOT.2004.1348184}
}
@phdthesis{duret.07.phd,
author = {Alexandre Duret-Lutz},
title = {Contributions {\`a} l'approche automate pour la
v{\'e}rification de propri{\'e}t{\'e}s de syst{\`e}mes
concurrents},
school = {Universit{\'e} Pierre et Marie Curie (Paris 6)},
year = {2007},
month = jul,
pdf = {adl/duret.07.phd.pdf},
slides = {adl/duret.07.phd.slides.pdf},
www = {../th.html}
}
@inproceedings{duret.09.atva,
author = {Alexandre Duret-Lutz and Denis Poitrenaud and Jean-Michel
Couvreur},
title = {On-the-fly Emptiness Check of Transition-based {S}treett
Automata},
booktitle = {Proceedings of the 7th International Symposium on
Automated Technology for Verification and Analysis
(ATVA'09)},
year = {2009},
editor = {Zhiming Liu and Anders P. Ravn},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
pages = {213--227},
volume = {5799},
pdf = {adl/duret.09.atva.pdf},
slides = {adl/duret.09.atva.slides.pdf},
abstract = {In the automata theoretic approach to model checking,
checking a state-space $S$ against a linear-time property
$\varphi$ can be done in $\mathrm{O}(|S|\times
2^{\mathrm{O}(|\varphi|)})$ time. When model checking under
$n$ strong fairness hypotheses expressed as a Generalized
B\"uchi automaton, this complexity becomes
$\mathrm{O}(|S|\times 2^{\mathrm{O}(|\varphi|+n)})$.\par
Here we describe an algorithm to check the emptiness of
Streett automata, which allows model checking under $n$
strong fairness hypotheses in $\mathrm{O}(|S|\times
2^{\mathrm{O}(|\varphi|)}\times n)$. We focus on
transition-based Streett automata, because it allows us to
express strong fairness hypotheses by injecting Streett
acceptance conditions into the state-space without any blowup.},
doi = {10.1007/978-3-642-04761-9_17}
}
@techreport{duret.11.arxiv,
author = {Alexandre Duret-Lutz and Kais Klai and Denis Poitrenaud
and Yann Thierry-Mieg},
title = {Combining Explicit and Symbolic Approaches for Better
On-the-Fly {LTL} Model Checking},
institution = {arXiv},
year = 2011,
number = {1106.5700},
month = jun,
note = {Extended version of our ATVA'11 paper, presenting two new
techniques instead of one.},
url = {http://arxiv.org/abs/1106.5700},
pdf = {adl/duret.11.arxiv.pdf},
abstract = {We present two new hybrid techniques that replace the
synchronized product used in the automata-theoretic
approach for LTL model checking. The proposed products are
explicit graphs of aggregates (symbolic sets of states)
that can be interpreted as B{\"u}chi automata. These hybrid
approaches allow on the one hand to use classical
emptiness-check algorithms and build the graph on-the-fly,
and on the other hand, to have a compact encoding of the
state space thanks to the symbolic representation of the
aggregates. The \emph{Symbolic Observation Product} assumes
a globally stuttering property (e.g., LTL-X) to aggregate
states. The \emph{Self-Loop Aggregation Product} does not
require the property to be globally stuttering (i.e., it
can tackle full LTL), but dynamically detects and exploits
a form of stuttering where possible. Our experiments show
that these two variants, while incomparable with each
other, can outperform other existing approaches.}
}
@inproceedings{duret.11.atva,
author = {Alexandre Duret-Lutz and Kais Klai and Denis Poitrenaud
and Yann Thierry-Mieg},
title = {Self-Loop Aggregation Product --- A New Hybrid Approach to
On-the-Fly {LTL} Model Checking},
booktitle = {Proceedings of the 9th International Symposium on
Automated Technology for Verification and Analysis
(ATVA'11)},
year = {2011},
series = {Lecture Notes in Computer Science},
address = {Taipei, Taiwan},
month = oct,
publisher = {Springer},
volume = {6996},
pages = {336--350},
abstract = {We present the \emph{Self-Loop Aggregation Product}
(SLAP), a new hybrid technique that replaces the
synchronized product used in the automata-theoretic
approach for LTL model checking. The proposed product is an
explicit graph of aggregates (symbolic sets of states) that
can be interpreted as a B{\"u}chi automata. The criterion
used by SLAP to aggregate states from the Kripke structure
is based on the analysis of self-loops that occur in the
B{\"u}chi automaton expressing the property to verify. Our
hybrid approach allows on the one hand to use classical
emptiness-check algorithms and build the graph on-the-fly,
and on the other hand, to have a compact encoding of the
state space thanks to the symbolic representation of the
aggregates. Our experiments show that this technique often
outperforms other existing (hybrid or fully symbolic)
approaches.},
pdf = {adl/duret.11.atva.pdf},
slides = {adl/duret.11.atva.slides.pdf},
doi = {10.1007/978-3-642-24372-1_24}
}
@misc{duret.11.sumo,
author = {Alexandre Duret-Lutz},
title = {Building {LTL} Model Checkers using {T}ransition-based
{G}eneralized {B\"u}chi {A}utomata},
howpublished = {Invited talk to SUMo'11},
month = jun,
year = {2011},
slides = {adl/duret.11.sumo.slides.pdf}
}
@inproceedings{duret.11.vecos,
author = {Alexandre Duret-Lutz},
title = {{LTL} Translation Improvements in {Spot}},
booktitle = {Proceedings of the 5th International Workshop on
Verification and Evaluation of Computer and Communication
Systems (VECoS'11)},
year = {2011},
series = {Electronic Workshops in Computing},
address = {Tunis, Tunisia},
month = sep,
publisher = {British Computer Society},
abstract = {Spot is a library of model-checking algorithms. This paper
focuses on the module translating LTL formul{\ae} into
automata. We discuss improvements that have been
implemented in the last four years, we show how Spot's
translation competes on various benchmarks, and we give
some insight into its implementation.},
proceedings = {http://ewic.bcs.org/category/15853},
pdf = {adl/duret.11.vecos.pdf},
slides = {adl/duret.11.vecos.slides.pdf}
}
@misc{duret.12.ciaa,
author = {Alexandre Duret-Lutz},
title = {The {S}pot Library, and its Online Translator from {LTL}
(and {PSL}) to {B\"u}chi Automata},
note = {Two-page flyer for the software demo session.},
month = jul,
year = {2012},
howpublished = {Distributed in the CIAA'12 conference booklet, not in the
main proceedings},
pdf = {adl/duret.12.ciaa.flyer.pdf}
}
@inproceedings{duret.13.atva,
author = {Alexandre Duret-Lutz},
title = {Manipulating {LTL} formulas using {Spot} 1.0},
booktitle = {Proceedings of the 11th International Symposium on
Automated Technology for Verification and Analysis
(ATVA'13)},
year = 2013,
series = {Lecture Notes in Computer Science},
volume = {8172},
pages = {442--445},
address = {Hanoi, Vietnam},
month = oct,
publisher = {Springer},
abstract = {We present a collection of command-line tools designed to
generate, filter, convert, simplify, lists of Linear-time
Temporal Logic formulas. These tools were introduced in the
release 1.0 of Spot, and we believe they should be of
interest to anybody who has to manipulate LTL formulas. We
focus on two tools in particular: ltlfilt, to filter and
transform formulas, and ltlcross to cross-check
LTL-to-B{\"u}chi-Automata translators.},
pdf = {adl/duret.13.atva.pdf},
slides = {adl/duret.13.atva.slides.pdf},
doi = {10.1007/978-3-319-02444-8_31}
}
@article{duret.14.ijccbs,
author = {Alexandre Duret-Lutz},
title = {{LTL} Translation Improvements in {S}pot 1.0},
journal = {International Journal on Critical Computer-Based Systems},
year = {2014},
volume = {5},
number = {1/2},
pages = {31--54},
month = mar,
pdf = {adl/duret.14.ijccbs.draft.pdf},
abstract = { Spot is a library of model-checking algorithms started in
2003. This paper focuses on its module for translating
linear-time temporal logic (LTL) formulas into B{\"u}chi
automata: one of the steps required in the
automata-theoretic approach to LTL model-checking.
We detail the different algorithms involved in this
translation: the core translation itself, which performs
many simplifications thanks to its use of binary decision
diagrams; the pre-processing of the LTL formulas with
rewriting rules chosen to help their translation; and
various post-processing algorithms whose use depends on the
intent of the translation: do we favor deterministic
automata, or small automata?
Using different benchmarks, we show how Spot competes with
other LTL translators, and how it has improved over the
years.
\textbf{Note:} This is an extended version
of~\cite{duret.11.vecos}.},
doi = {10.1504/IJCCBS.2014.059594}
}
@inproceedings{duret.16.atva,
author = {Alexandre Duret-Lutz and Fabrice Kordon and Denis
Poitrenaud and Etienne Renault},
title = {Heuristics for Checking Liveness Properties with Partial
Order Reductions},
booktitle = {Proceedings of the 14th International Symposium on
Automated Technology for Verification and Analysis
(ATVA'16)},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
volume = {9938},
pages = {340--356},
year = {2016},
month = oct,
pdf = {adl/duret.16.atva.pdf},
abstract = {Checking liveness properties with partial-order reductions
requires a cycle proviso to ensure that an action cannot be
postponed forever. The proviso forces each cycle to contain
at least one fully expanded state. We present new
heuristics to select which state to expand, hoping to
reduce the size of the resulting graph. The choice of the
state to expand is done when encountering a
\emph{dangerous} edge. Almost all existing provisos expand
the source of this edge, while this paper also explores the
expansion of the destination and the use of SCC-based
information.},
doi = {10.1007/978-3-319-46520-3_22}
}
@inproceedings{duret.16.atva2,
author = {Alexandre Duret-Lutz and Alexandre Lewkowicz and Amaury
Fauchille and Thibaud Michaud and Etienne Renault and
Laurent Xu},
title = {Spot 2.0 --- a framework for {LTL} and $\omega$-automata
manipulation},
booktitle = {Proceedings of the 14th International Symposium on
Automated Technology for Verification and Analysis
(ATVA'16)},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
volume = {9938},
pages = {122--129},
year = {2016},
month = oct,
pdf = {adl/duret.16.atva2.pdf},
abstract = {We present Spot 2.0, a C++ library with Python bindings
and an assortment of command-line tools designed to
manipulate LTL and $\omega$-automata in batch. New
automata-manipulation tools were introduced in Spot 2.0;
they support arbitrary acceptance conditions, as
expressible in the Hanoi Omega Automaton format. Besides
being useful to researchers who have automata to process,
its Python bindings can also be used in interactive
environments to teach $\omega$-automata and model checking.},
doi = {10.1007/978-3-319-46520-3_8}
}
@phdthesis{duret.17.hdr,
author = {Alexandre Duret-Lutz},
title = {Contributions to LTL and $\omega$-Automata for Model
Checking},
school = {Universit{\'e} Pierre et Marie Curie (Paris 6)},
year = {2017},
month = feb,
pdf = {adl/duret.17.hdr.pdf},
slides = {adl/duret.17.hdr.slides.pdf},
type = {Habilitation Thesis}
}
@inproceedings{duret.22.cav,
author = {Alexandre~Duret-Lutz and Etienne Renault and Maximilien
Colange and Florian Renkin and Alexandre Gbaguidi~Aisse and
Philipp Schlehuber-Caissier and Thomas Medioni and Antoine
Martin and J{\'e}r{\^o}me Dubois and Cl{\'e}ment Gillard
and Henrich Lauko},
title = {From {S}pot 2.0 to {S}pot 2.10: What's New?},
booktitle = {Proceedings of the 34th International Conference on
Computer Aided Verification (CAV'22)},
year = 2022,
volume = {13372},
series = {Lecture Notes in Computer Science},
pages = {174--187},
month = aug,
publisher = {Springer},
abstract = {Spot is a C++17 library for LTL and $\omega$-automata
manipulation, with command-line utilities, and Python
bindings. This paper summarizes its evolution over the past
six years, since the release of Spot 2.0, which was the
first version to support $\omega$-automata with arbitrary
acceptance conditions, and the last version presented at a
conference. Since then, Spot has been extended with several
features such as acceptance transformations, alternating
automata, games, LTL synthesis, and more. We also shed some
lights on the data-structure used to store automata. },
pdf = {adl/duret.22.cav.pdf},
slides = {adl/duret.22.cav.slides.pdf},
doi = {10.1007/978-3-031-13188-2_9}
}
@techreport{duret.99.tr03,
author = {Alexandre Duret-Lutz and Thierry G\'eraud},
title = {Patrons de conception statiques pour la programmation
g\'en\'erique en {C++}},
institution = {EPITA Research and Development Laboratory},
year = {1999},
type = {Technical Report},
number = {9903},
address = {Paris},
month = sep,
pdf = {adl/duret.99.tr03.pdf}
}
@inproceedings{fronc.13.atva,
author = {{\L}ukasz Fronc and Alexandre Duret-Lutz},
title = {{LTL} Model Checking with {N}eco},
booktitle = {Proceedings of the 11th International Symposium on
Automated Technology for Verification and Analysis
(ATVA'13)},
year = 2013,
series = {Lecture Notes in Computer Science},
volume = {8172},
pages = {451--454},
address = {Hanoi, Vietnam},
month = oct,
publisher = {Springer},
abstract = {We introduce neco-spot, an LTL model checker for Petri net
models. It builds upon Neco, a compiler turning Petri nets
into native shared libraries that allows fast on-the-fly
exploration of the state-space, and upon Spot, a C++
library of model-checking algorithms. We show the
architecture of Neco and explain how it was combined with
Spot to build an LTL model checker.},
pdf = {adl/fronc.13.atva.pdf},
slides = {adl/fronc.13.atva.slides.pdf},
doi = {10.1007/978-3-319-02444-8_33}
}
@inproceedings{geraud.00.europlop,
author = {Thierry G\'eraud and Alexandre Duret-Lutz},
title = {Generic Programming Redesign of Patterns},
booktitle = {Proceedings of the 5th European Conference on Pattern
Languages of Programs (EuroPLoP'00)},
year = {2000},
month = jul,
page = {283--294},
editor = {M. Devos and A. R\"uping},
publisher = {UVK, Univ. Verlag, Konstanz},
adress = {Irsee, Germany},
pdf = {adl/geraud.00.europlop.pdf}
}
@inproceedings{geraud.00.icpr,
author = {Thierry G\'eraud and Yoann Fabre and Alexandre Duret-Lutz
and Dimitri Papadopoulos-Orfanos and Jean-Fran\c{c}ois
Mangin},
title = {Obtaining Genericity for Image Processing and Pattern
Recognition Algorithms},
booktitle = {Proceedings of the 15th International Conference on
Pattern Recognition (ICPR'00)},
year = {2000},
month = sep,
address = {Barcelona, Spain},
volume = {4},
pages = {816--819},
publisher = {IEEE Computer Society},
abstract = { Algorithm libraries dedicated to image processing and
pattern recognition are not reusable; to run an algorithm
on particular data, one usually has either to rewrite the
algorithm or to manually "copy, paste, and modify". This is
due to the lack of genericity of the programming paradigm
used to implement the libraries. In this paper, we present
a recent paradigm that allows algorithms to be written once
and for all and to accept input of various types. Moreover,
this total reusability can be obtained with a very
comprehensive writing and without significant cost at
execution, compared to a dedicated algorithm. This new
paradigm is called "generic programming" and is fully
supported by the C++ language. We show how this paradigm
can be applied to image processing and pattern recognition
routines. The perspective of our work is the creation of a
generic library.}
}
@inproceedings{geraud.01.ai,
author = {Thierry G\'eraud and Yoann Fabre and Alexandre Duret-Lutz},
title = {Applying Generic Programming to Image Processing},
booktitle = {Proceedings of the IASTED International Conference on
Applied Informatics (AI'01)---Symposium Advances in
Computer Applications},
year = {2001},
address = {Innsbruck, Austria},
month = feb,
pages = {577--581},
publisher = {ACTA Press},
editor = {M.H.~Hamsa},
abstract = { This paper presents the evolution of algorithms
implementation in image processing libraries and discusses
the limits of these implementations in terms of
reusability. In particular, we show that in C++, an
algorithm can have a general implementation; said
differently, an implementation can be generic, i.e.,
independent of both the input aggregate type and the type
of the data contained in the input aggregate. A total
reusability of algorithms can therefore be obtained;
moreover, a generic implementation is more natural and does
not introduce a meaningful additional cost in execution
time as compared to an implementation dedicated to a
particular input type. }
}
@techreport{geraud.99.tr01,
author = {Thierry G\'eraud and Alexandre Duret-Lutz},
title = {Composants g\'en\'eriques de calcul scientifique},
institution = {EPITA Research and Development Laboratory},
year = {1999},
type = {Technical Report},
number = {9901},
address = {Paris},
month = mar,
pdf = {adl/geraud.99.tr01.pdf},
abstract = {Dans le cadre de l'{\'e}criture en C++ d'une
biblioth{\`e}que de traitements d'images et d'un atelier de
programmation par composants d'une cha{\^i}ne de
traitements, nous nous sommes fix{\'e}s deux objectifs
principaux : rendre les traitements g{\'e}n{\'e}riques
vis-{\`a}-vis du type de ses entr{\'e}es sans entra{\^i}ner
de surco{\^u}t significatif {\`a} l'ex{\'e}cution, et
pouvoir ex{\'e}cuter un traitement lorsqu'il a et{\'e}
introduit ult{\'e}rieurement {\`a} la compilation de
l'atelier. \par Le premier objectif est atteint a l'aide de
programmation g{\'e}n{\'e}rique et de la traduction en
polymorphisme statique de certains idiomes (\textit{design
patterns}) d{\'e}finis pour le polymorphisme dynamique. La
probl{\'e}matique du second objectif est double. Tout
d'abord, nous devions r{\'e}aliser la mise en
correspondance d'un traitement dont les entr{\'e}es-sorties
sont des types abstraits et de la routine
g{\'e}n{\'e}rique, charg{\'e}e du traitement, dont les
param{\`e}tres sont des types concrets ; ensuite, nous
devions pouvoir compiler et lier de nouveaux traitements a
la vol{\'e}e, lors de l'ex{\'e}cution de l'atelier. Pour
atteindre ce double objectif, nous utilisons de la
programmation g{\'e}n{\'e}rative et nous pratiquons
l'instanciation paresseuse (\textit{lazy}) de code
g{\'e}n{\'e}rique.\par Les solutions que nous apportons
permettent la gestion de composants r{\'e}utilisables de
calcul scientifique, ce qui, {\`a} notre connaissance, est original. }
}
@inproceedings{german.07.cae,
author = {Daniel M. German and Lloyd Burchill and Alexandre
Duret-Lutz and S{\'e}bastien P{\'e}rez-Duarte and Emmanuel
P{\'e}rez-Duarte and Josh Sommers},
title = {Flattening the Viewable Sphere},
booktitle = {Proceedings of the Third Eurographics Conference on
Computational Aesthetics in Graphics, Visualization and
Imaging (CAe'07)},
year = {2007},
location = {Alberta, Canada},
pages = {23--28},
numpages = {6},
doi = {10.2312/COMPAESTH/COMPAESTH07/023-028},
publisher = {Eurographics Association},
note = {Artistic Submission},
abstract = {The viewable sphere corresponds to the space that
surrounds us. The evolution of photography and panoramic
software and hardware has made it possible for anybody to
capture the viewable sphere. It is now up to the artist to
determine what can be done with this raw material. In this
paper we explore the underdeveloped field of flat panoramas
from an artistic point of view. We argue that its future
lies in the exploration of conformal mappings, specialized
software, and the interaction of its practitioners via the
Internet.},
pdf = {adl/german.07.cae.pdf}
}
@techreport{jacobs.22.arxiv,
author = {Swen Jacobs and Guillermo Alberto~Perez and Remco Abraham
and V{\'e}ronique Bruy{\`e}re and Micha{\"e}l Cadilhac and
Maximilien Colange and Charly Delfosse and Tom van~Dijk and
Alexandre Duret-Lutz and Peter Faymonville and Bernd
Finkbeiner and Ayrat Khalimov and Felix Klein and Michael
Luttenberger and Klara~J. Meyer and Thibaud Michaud and
Adrien Pommellet and Florian Renkin and Philipp
Schlehuber-Caissier and Mouhammad Sakr and Salomon Sickert
and Ga{\"e}tan Staquet and Cl{\'e}ment Tamines and Leander
Tentrup and Adam Walker},
abstract = {We report on the last four editions of the reactive
synthesis competition (SYNTCOMP 2018-2021). We briefly
describe the evaluation scheme and the experimental setup
of SYNTCOMP. Then, we introduce new benchmark classes that
have been added to the SYNTCOMP library and give an
overview of the participants of SYNTCOMP. Finally, we
present and analyze the results of our experimental
evaluations, including a ranking of tools with respect to
quantity and quality of solutions.},
doi = {10.48550/ARXIV.2206.00251},
publisher = {arXiv},
title = {The Reactive Synthesis Competition ({SYNTCOMP}):
2018--2021},
url = {https://arxiv.org/abs/2206.00251},
year = 2022,
pdf = {adl/jacobs.22.arxiv.pdf}
}
@inproceedings{michaud.15.spin,
author = {Thibaud Michaud and Alexandre Duret-Lutz},
title = {Practical Stutter-Invariance Checks for {$\omega$}-Regular
Languages},
booktitle = {Proceedings of the 22th International SPIN Symposium on
Model Checking of Software (SPIN'15)},
year = 2015,
pages = {84--101},
series = {Lecture Notes in Computer Science},
volume = 9232,
publisher = {Springer},
month = aug,
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{\"u}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.},
pdf = {adl/michaud.15.spin.pdf},
doi = {10.1007/978-3-319-23404-5_7}
}
@inproceedings{renault.13.lpar,
author = {Etienne Renault and Alexandre Duret-Lutz and Fabrice
Kordon and Denis Poitrenaud},
title = {Three {SCC}-based Emptiness Checks for Generalized
{B\"u}chi Automata},
booktitle = {Proceedings of the 19th International Conference on Logic
for Programming, Artificial Intelligence, and Reasoning
(LPAR-19)},
editor = {Ken McMillan and Aart Middeldorp and Andrei Voronkov },
year = {2013},
pages = {668--682},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {8312},
month = dec,
abstract = { The automata-theoretic approach for the verification of
linear time properties involves checking the emptiness of a
B{\"u}chi automaton. However generalized B{\"u}chi
automata, with multiple acceptance sets, are preferred when
verifying under weak fairness hypotheses. Existing
emptiness checks for which the complexity is independent of
the number of acceptance sets are all based on the
enumeration of Strongly Connected Components (SCCs).
In this paper, we review the state of the art SCC
enumeration algorithms to study how they can be turned into
emptiness checks. This leads us to define two new emptiness
check algorithms (one of them based on the Union Find data
structure), introduce new optimizations, and show that one
of these can be of benefit to a classic SCCs enumeration
algorithm. We have implemented all these variants to
compare their relative performances and the overhead
induced by the emptiness check compared to the
corresponding SCCs enumeration algorithm. Our experiments
shows that these three algorithms are comparable.},
pdf = {adl/renault.13.lpar.pdf},
doi = {10.1007/978-3-642-45221-5_44}
}
@inproceedings{renault.13.tacas,
author = {Etienne Renault and Alexandre Duret-Lutz and Fabrice
Kordon and Denis Poitrenaud},
title = {Strength-Based Decomposition of the Property {B\"u}chi
Automaton for Faster Model Checking},
booktitle = {Proceedings of the 19th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems
(TACAS'13)},
editor = {Nir Piterman and Scott A. Smolka},
year = {2013},
month = mar,
pages = {580--593},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {7795},
abstract = {The automata-theoretic approach for model checking of
linear-time temporal properties involves the emptiness
check of a large B{\"u}chi automaton. Specialized
emptiness-check algorithms have been proposed for the cases
where the property is represented by a weak or terminal
automaton.
When the property automaton does not fall into these
categories, a general emptiness check is required. This
paper focuses on this class of properties. We refine
previous approaches by classifying strongly-connected
components rather than automata, and suggest a
decomposition of the property automaton into three smaller
automata capturing the terminal, weak, and the remaining
strong behaviors of the property. The three corresponding
emptiness checks can be performed independently, using the
most appropriate algorithm.
Such a decomposition approach can be used with any
automata-based model checker. We illustrate the interest of
this new approach using explicit and symbolic LTL model
checkers.},
pdf = {adl/renault.13.tacas.pdf},
doi = {10.1007/978-3-642-36742-7_42}
}
@inproceedings{renault.15.tacas,
author = {Etienne Renault and Alexandre Duret-Lutz and Fabrice
Kordon and Denis Poitrenaud},
title = {Parallel Explicit Model Checking for Generalized {B\"u}chi
Automata},
booktitle = {Proceedings of the 19th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems
(TACAS'15)},
editor = {Christel Baier and Cesare Tinelli},
year = 2015,
month = apr,
pages = {613--627},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 9035,
abstract = {We present new parallel emptiness checks for LTL model
checking. Unlike existing parallel emptiness checks, these
are based on an SCC enumeration, support generalized Buchi
acceptance, and require no synchronization points nor
repair procedures. A salient feature of our algorithms is
the use of a global union-find data structure in which
multiple threads share structural information about the
automaton being checked. Our prototype implementation has
encouraging performances: the new emptiness checks have
better speedup than existing algorithms in half of our
experiments.},
pdf = {adl/renault.15.tacas.pdf},
doi = {10.1007/978-3-662-46681-0_56}
}
@article{renault.16.sttt,
author = {Etienne Renault and Alexandre Duret-Lutz and Fabrice
Kordon and Denis Poitrenaud},
title = {Variations on Parallel Explicit Model Checking for
Generalized {B\"u}chi Automata},
journal = {International Journal on Software Tools for Technology
Transfer (STTT)},
year = 2017,
note = {First published online on 26 April 2016.},
volume = 19,
number = 6,
pages = {653--673},
month = nov,
publisher = {Springer},
abstract = {We present new parallel explicit emptiness checks for LTL
model checking. Unlike existing parallel emptiness checks,
these are based on a Strongly Connected Component (SCC)
enumeration, support generalized {B\"u}chi acceptance, and
require no synchronization points nor recomputing
procedures. A salient feature of our algorithms is the use
of a global union-find data structure in which multiple
threads share structural information about the automaton
checked. Besides these basic algorithms, we present one
architectural variant isolating threads that write to the
union-find, and one extension that decomposes the automaton
based on the strength of its SCCs to use more optimized
emptiness checks. The results from an extensive
experimentation of our algorithms and their variations show
encouraging performances, especially when the decomposition
technique is used.
\textbf{Note:} This is an extended version
of~\cite{renault.15.tacas}.},
doi = {10.1007/s10009-016-0422-5},
pdf = {adl/renault.16.sttt.pdf}
}
@inproceedings{renkin.20.atva,
author = {Florian Renkin and Alexandre Duret-Lutz and Adrien
Pommellet},
title = {Practical ``Paritizing'' of Emerson-Lei Automata},
booktitle = {Proceedings of the 18th International Symposium on
Automated Technology for Verification and Analysis
(ATVA'20)},
year = {2020},
volume = {12302},
series = {Lecture Notes in Computer Science},
pages = {127--143},
month = oct,
publisher = {Springer},
abstract = {We introduce a new algorithm that takes a
\emph{Transition-based Emerson-Lei Automaton} (TELA), that
is, an $\omega$-automaton whose acceptance condition is an
arbitrary Boolean formula on sets of transitions to be seen
infinitely or finitely often, and converts it into a
\emph{Transition-based Parity Automaton} (TPA). To reduce
the size of the output TPA, the algorithm combines and
optimizes two procedures based on a \emph{latest appearance
record} principle, and introduces a \emph{partial
degeneralization}. Our motivation is to use this algorithm
to improve our LTL synthesis tool, where producing
deterministic parity automata is an intermediate step.},
pdf = {adl/renkin.20.atva.pdf},
doi = {10.1007/978-3-030-59152-6_7}
}
@misc{renkin.21.synt,
author = {Florian Renkin and Philipp Schlehuber and Alexandre
Duret-Lutz and Adrien Pommellet},
title = {Improvements to \texttt{ltlsynt}},
howpublished = {Presented at the SYNT'21 workshop, without proceedings.},
year = {2021},
month = jul,
abstract = {We summarize \texttt{ltlsynt}'s evolution since 2018.},
pdf = {adl/renkin.21.synt.pdf}
}
@inproceedings{renkin.22.forte,
author = {Florian Renkin and Philipp Schlehuber-Caissier and
Alexandre Duret-Lutz and Adrien Pommellet},
title = {Effective Reductions of {M}ealy Machines},
year = 2022,
booktitle = {Proceedings of the 42nd International Conference on Formal
Techniques for Distributed Objects, Components, and Systems
(FORTE'22)},
series = {Lecture Notes in Computer Science},
volume = 13273,
pages = {170--187},
month = jun,
publisher = {Springer},
abstract = {We revisit the problem of reducing incompletely specified
Mealy machines with reactive synthesis in mind. We propose
two techniques: the former is inspired by the tool {\sc
MeMin} and solves the minimization problem, the latter is a
novel approach derived from simulation-based reductions but
may not guarantee a minimized machine. However, we argue
that it offers a good enough compromise between the size of
the resulting Mealy machine and performance. The proposed
methods are benchmarked against \textsc{MeMin} on a large
collection of test cases made of well-known instances as
well as new ones.},
doi = {10.1007/978-3-031-08679-3_8},
pdf = {adl/renkin.22.forte.pdf}
}
@article{renkin.23.fmsd,
author = {Florian Renkin and Philipp Schlehuber-Caissier and
Alexandre Duret-Lutz and Adrien Pommellet},
title = {Dissecting ltlsynt},
journal = {Formal Methods in System Design},
year = {2023},
note = {Available online since 14 July 2023},
doi = {https://doi.org/10.1007/s10703-022-00407-6},
abstract = {ltlsynt is a tool for synthesizing a reactive circuit
satisfying a specification expressed as an LTL formula.
ltlsynt generally follows a textbook approach: the LTL
specification is translated into a parity game whose
winning strategy can be seen as a Mealy machine modeling a
valid controller. This article details each step of this
approach, and presents various refinements integrated over
the years. Some of these refinements are unique to ltlsynt:
for instance, ltlsynt supports multiple ways to encode a
Mealy machine as an AIG circuit, features multiple
simplification algorithms for the intermediate Mealy
machine, and bypasses the usual game-theoretic approach for
some subclasses of LTL formulas in favor of more direct
constructions.},
pdf = {adl/renkin.23.fmsd.pdf}
}
@article{renkin.23.scp,
author = {Florian Renkin and Philipp Schlehuber-Caissier and
Alexandre Duret-Lutz and Adrien Pommellet},
title = {The {M}ealy-machine reduction functions of {S}pot},
journal = {Science of Computer Programming},
year = {2023},
month = aug,
volume = 230,
number = 102995,
doi = {10.1016/j.scico.2023.102995},
abstract = {We present functions for reducing Mealy machines,
initially detailed in our FORTE'22 article. These functions
are now integrated into Spot 2.11.2, where they are used as
part of the ltlsynt tool for reactive synthesis. Of course,
since Spot is a library, these functions can also be used
on their own, and we provide Python bindings for easy
experiments. The reproducible capsule benchmarks these
functions on Mealy machines from various sources, and
compare them to the MeMin tool.},
pdf = {adl/renkin.23.scp.pdf}
}
@misc{sakarovitch.12.ciaa,
author = {Alexandre Duret-Lutz and Sylvain Lombardy and Jacques
Sakarovitch and Hsu-Chun Yen},
title = {{V}aucanson 1.4.1},
note = {Two-page flyer for the software demo session.},
month = jul,
year = {2012},
howpublished = {Distributed in the CIAA'12 conference booklet, not in the
main proceedings},
pdf = {adl/sakarovitch.12.ciaa.flyer.pdf}
}
@article{thierry-mieg.04.gl,
author = {Yann Thierry-Mieg and Souheib Baarir and Alexandre
Duret-Lutz and Fabrice Kordon},
title = {Nouvelles techniques de model-checking pour la
v{\'e}rification de syst{\`e}mes complexes},
journal = {G{\'e}nie Logiciel},
year = {2004},
number = {69},
pages = {17--23},
month = jun,
pdf = {adl/thierry-mieg.04.gl.pdf}
}
@misc{tourneur.17.misc,
author = {Vincent Tourneur and Alexandre Duret-Lutz},
title = {Fixes for two equations in \emph{The Blow-Up in
Translating LTL to Deterministic Automata} by {K}upferman
and {R}osenberg},
howpublished = {Online PDF.},
note = {The original authors have reviewed the fixes and agreed
with them.},
month = feb,
year = 2017,
pdf = {adl/tourneur.17.misc.pdf}
}
@inproceedings{xue.03.icip,
author = {Heru Xue and Thierry G{\'e}raud and Alexandre Duret-Lutz},
title = {Multi-band Segmentation using Morphological Clustering and
Fusion; Application to Color Image Segmentation},
booktitle = {Proceedings of the IEEE International Conference on Image
Processing (ICIP 2003)},
year = {2003},
address = {Barcelona, Spain},
month = sep,
abstract = { In this paper we propose a novel approach for color image
segmentation. Our approach is based on segmentation of
subsets of bands using mathematical morphology followed by
the fusion of the resulting segmentation "channels". For
color images the band subsets are chosen as RG, RB and GB
pairs, whose 2D histograms are processed as projections of
a 3D histogram. The segmentations in 2D color spaces are
obtained using the watershed algorithm. These 2D
segmentations are then combined to obtain a final result
using a region split-and-merge process. The CIE $L^*a^*b^*$
color space is used to measure the color distance. Our
approach results in improved performance and can be
generalized for multiband segmentation of images such as
multi-spectral satellite images.},
doi = {10.1109/ICIP.2003.1246971}
}