@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{templatevoid 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} }

@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} }

@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}, 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.}, note = {To appear}, pdf = {adl/renkin.22.forte.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} }