Publications of Alexandre Duret-Lutz

[duret.17.hdr]
Alexandre Duret-Lutz. Contributions to LTL and ω-Automata for Model Checking. Habilitation thesis, Université Pierre et Marie Curie (Paris 6), February 2017. [ bib | pdf | slides ]
[duret.16.atva]
Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud, and Etienne Renault. Heuristics for checking liveness properties with partial order reductions. In Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA'16), volume 9938 of Lecture Notes in Computer Science, pages 340–356. Springer, October 2016. [ bib | pdf ]
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 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.

[duret.16.atva2]
Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Renault, and Laurent Xu. Spot 2.0 –- a framework for LTL and ω-automata manipulation. In Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA'16), volume 9938 of Lecture Notes in Computer Science, pages 122–129. Springer, October 2016. [ bib | pdf ]
We present Spot 2.0, a C++ library with Python bindings and an assortment of command-line tools designed to manipulate LTL and ω-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 ω-automata and model checking.

[renault.16.sttt]
Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, and Denis Poitrenaud. Variations on parallel explicit model checking for generalized Büchi automata. International Journal on Software Tools for Technology Transfer (STTT), ??(??):1–21, April 2016. [ bib | DOI | pdf ]
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ü 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.

[baarir.15.lpar]
Souheib Baarir and Alexandre Duret-Lutz. SAT-based minimization of deterministic ω-automata. In Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'15), volume 9450 of Lecture Notes in Computer Science, pages 79–87. Springer, November 2015. [ bib | DOI | pdf ]
We describe a tool that inputs a deterministic ω-automaton with any acceptance condition, and synthesizes an equivalent ω-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 ω-automata equivalent to given properties, for different acceptance conditions.

[blahoudek.15.spin]
František Blahoudek, Alexandre Duret-Lutz, Vojtčech Rujbr, and Jan Strejček. On refinement of Büchi automata for explicit model checking. In Proceedings of the 22th International SPIN Symposium on Model Checking of Software (SPIN'15), volume 9232 of Lecture Notes in Computer Science, pages 66–83. Springer, August 2015. [ bib | DOI | pdf ]
In explicit model checking, systems are typically described in an implicit and compact way. Some valid information about the system can be easily derived directly from this description, for example that some atomic propositions cannot be valid at the same time. The paper shows several ways to apply this information to improve the Büchi automaton built from an LTL specification. As a result, we get smaller automata with shorter edge labels that are easier to understand and, more importantly, for which the explicit model checking process performs better.

[michaud.15.spin]
Thibaud Michaud and Alexandre Duret-Lutz. Practical stutter-invariance checks for ω-regular languages. In Proceedings of the 22th International SPIN Symposium on Model Checking of Software (SPIN'15), volume 9232 of Lecture Notes in Computer Science, pages 84–101. Springer, August 2015. [ bib | DOI | pdf ]
We propose several automata-based constructions that check whether a specification is stutter-invariant. These constructions assume that a specification and its negation can be translated into Büchi automata, but aside from that, they are independent of the specification formalism. These transformations were inspired by a construction due to Holzmann and Kupferman, but that we broke down into two operations that can have different realizations, and that can be combined in different ways. As it turns out, implementing only one of these operations is needed to obtain a functional stutter-invariant check. Finally we have implemented these techniques in a tool so that users can easily check whether an LTL or PSL formula is stutter-invariant.

[babiak.15.cav]
Tomáš Babiak, František Blahoudek, Alexandre Duret-Lutz, Joachim Klein, Jan Křetínský, David Müller, David Parker, and Jan Strejček. The Hanoi Omega-Automata format. In Proceedings of the 27th International Conference on Computer Aided Verification (CAV'15), volume 9206 of Lecture Notes in Computer Science, pages 479–486. Springer, July 2015. [ bib | DOI | pdf | slides | poster ]
We propose a flexible exchange format for ω-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üchi, 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.

[renault.15.tacas]
Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, and Denis Poitrenaud. Parallel explicit model checking for generalized Büchi automata. In Christel Baier and Cesare Tinelli, editors, Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'15), volume 9035 of Lecture Notes in Computer Science, pages 613–627. Springer, April 2015. [ bib | DOI | pdf ]
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.

[blahoudek.14.spin]
František Blahoudek, Alexandre Duret-Lutz, Mojmír Křetínský, and Jan Strejček. Is there a best Büchi automaton for explicit model checking? In Proceedings of the 21th International SPIN Symposium on Model Checking of Software (SPIN'14), pages 68–76. ACM, July 2014. [ bib | DOI | pdf ]
LTL to Bü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ü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.

[demaille.14.ciaa]
Akim Demaille, Alexandre Duret-Lutz, Sylvain Lombardy, Luca Saiu, and Jacques Sakarovitch. A type system for weighted automata and rational expressions. In Proceedings of Implementation and Application of Automata, 19th International Conference (CIAA'14), Giessen, Germany, July 2014. [ bib | DOI | pdf ]
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.

[baarir.14.forte]
Souheib Baarir and Alexandre Duret-Lutz. Mechanizing the minimization of deterministic generalized Büchi automata. In Proceedings of the 34th IFIP International Conference on Formal Techniques for Distributed Objects, Components and Systems (FORTE'14), volume 8461 of Lecture Notes in Computer Science, pages 266–283. Springer, June 2014. [ bib | DOI | pdf | slides ]
Deterministic Bü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.

[bensalem.14.tacas]
Ala Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon, and Yann Thierry-Mieg. Symbolic model checking of stutter invariant properties using generalized testing automata. In Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14), volume 8413 of Lecture Notes in Computer Science, pages 440–454, Grenoble, France, April 2014. Springer. [ bib | DOI | pdf ]
In a previous work, we showed that a kind of ω-automata known as Transition-based Generalized Testing Automata (TGTA) can outperform the Büchi automata traditionally used for explicit model checking when verifying stutter-invariant properties. In this work, we investigate the use of these generalized testing automata to improve 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üchi Automata.

[duret.14.ijccbs]
Alexandre Duret-Lutz. LTL translation improvements in Spot 1.0. International Journal on Critical Computer-Based Systems, 5(1/2):31–54, March 2014. [ bib | DOI | pdf ]
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ü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.

Note: This is an extended version of [duret.11.vecos].

[renault.13.lpar]
Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, and Denis Poitrenaud. Three SCC-based emptiness checks for generalized Büchi automata. In Ken McMillan, Aart Middeldorp, and Andrei Voronkov, editors, Proceedings of the 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'13), volume 8312 of Lecture Notes in Computer Science, pages 668–682. Springer, December 2013. [ bib | DOI | pdf ]
The automata-theoretic approach for the verification of linear time properties involves checking the emptiness of a Büchi automaton. However generalized Bü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.

[duret.13.atva]
Alexandre Duret-Lutz. Manipulating LTL formulas using Spot 1.0. In Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA'13), volume 8172 of Lecture Notes in Computer Science, pages 442–445, Hanoi, Vietnam, October 2013. Springer. [ bib | DOI | pdf | slides ]
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üchi-Automata translators.

[fronc.13.atva]
Lukasz Fronc and Alexandre Duret-Lutz. LTL model checking with Neco. In Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA'13), volume 8172 of Lecture Notes in Computer Science, pages 451–454, Hanoi, Vietnam, October 2013. Springer. [ bib | DOI | pdf | slides ]
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.

[babiak.13.spin]
Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír Křetínský, and Jan Strejček. Compositional approach to suspension and other improvements to LTL translation. In Proceedings of the 20th International SPIN Symposium on Model Checking of Software (SPIN'13), volume 7976 of Lecture Notes in Computer Science, pages 81–98. Springer, July 2013. [ bib | DOI | pdf | slides ]
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ü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ü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.

[demaille.13.ciaa]
Akim Demaille, Alexandre Duret-Lutz, Sylvain Lombardy, and Jacques Sakarovitch. Implementation concepts in Vaucanson 2. In Oscar H. Ibarra and Zhe Dang, editors, Proceedings of Implementation and Application of Automata, 18th International Conference (CIAA'13), volume 2759 of Lecture Notes in Computer Science, pages 96–107, Santa Barbara, CA, USA, July 2013. Springer. [ bib | DOI | pdf ]
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.

[renault.13.tacas]
Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, and Denis Poitrenaud. Strength-based decomposition of the property Büchi automaton for faster model checking. In Nir Piterman and Scott A. Smolka, editors, Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'13), volume 7795 of Lecture Notes in Computer Science, pages 580–593. Springer, March 2013. [ bib | DOI | pdf ]
The automata-theoretic approach for model checking of linear-time temporal properties involves the emptiness check of a large Bü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.

[duret.12.ciaa]
Alexandre Duret-Lutz. The Spot library, and its online translator from LTL (and PSL) to Büchi automata. Distributed in the CIAA'12 conference booklet, not in the main proceedings, July 2012. Two-page flyer for the software demo session. [ bib | pdf ]
[sakarovitch.12.ciaa]
Alexandre Duret-Lutz, Sylvain Lombardy, Jacques Sakarovitch, and Hsu-Chun Yen. Vaucanson 1.4.1. Distributed in the CIAA'12 conference booklet, not in the main proceedings, July 2012. Two-page flyer for the software demo session. [ bib | pdf ]
[bensalem.12.topnoc]
Ala Eddine Ben Salem, Alexandre Duret-Lutz, and Fabrice Kordon. Model checking using generalized testing automata. Transactions on Petri Nets and Other Models of Concurrency (ToPNoC VI), 7400:94–112, 2012. [ bib | DOI | pdf ]
Geldenhuys and Hansen showed that a kind of ω-automata known as Testing Automata (TA) can, in the case of stuttering-insensitive properties, outperform the Büchi automata traditionally used in the automata-theoretic approach to model checking.

In previous work, we compared TA against Transition-based Generalized Büchi Automata (TGBA), and concluded that TA were more interesting when counterexamples were expected, otherwise TGBA were more efficient.

In this work we introduce a new kind of automata, dubbed 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.

[duret.11.atva]
Alexandre Duret-Lutz, Kais Klai, Denis Poitrenaud, and Yann Thierry-Mieg. Self-loop aggregation product –- a new hybrid approach to on-the-fly LTL model checking. In Proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis (ATVA'11), volume 6996 of Lecture Notes in Computer Science, pages 336–350, Taipei, Taiwan, October 2011. Springer. [ bib | DOI | pdf | slides ]
We present the 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ü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ü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.

[duret.11.vecos]
Alexandre Duret-Lutz. LTL translation improvements in Spot. In Proceedings of the 5th International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS'11), Electronic Workshops in Computing, Tunis, Tunisia, September 2011. British Computer Society. [ bib | pdf | slides | proceedings ]
Spot is a library of model-checking algorithms. This paper focuses on the module translating LTL formulæ 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.

[bensalem.11.sumo]
Ala Eddine Ben Salem, Alexandre Duret-Lutz, and Fabrice Kordon. Generalized Büchi automata versus testing automata for model checking. In Proceedings of the second International Workshop on Scalable and Usable Model Checking for Petri Net and other models of Concurrency (SUMO'11), volume 726 of Workshop Proceedings, Newcastle, UK, June 2011. CEUR. [ bib | pdf ]
Geldenhuys and Hansen have shown that a kind of ω-automaton known as testing automata can outperform the Büchi automata traditionally used in the automata-theoretic approach to model checking. This work completes their experiments by including a comparison with generalized Büchi automata; by using larger state spaces derived from Petri nets; and by distinguishing violated formulæ (for which testing automata fare better) from verified formulæ (where testing automata are hindered by their two-pass emptiness check).

[duret.11.arxiv]
Alexandre Duret-Lutz, Kais Klai, Denis Poitrenaud, and Yann Thierry-Mieg. Combining explicit and symbolic approaches for better on-the-fly LTL model checking. Technical Report 1106.5700, arXiv, June 2011. Extended version of our ATVA'11 paper, presenting two new techniques instead of one. [ bib | pdf | http ]
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ü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 Symbolic Observation Product assumes a globally stuttering property (e.g., LTL-X) to aggregate states. The 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.

[duret.11.sumo]
Alexandre Duret-Lutz. Building LTL model checkers using Transition-based Generalized Büchi Automata. Invited talk to SUMo'11, June 2011. [ bib | slides ]
[duret.09.atva]
Alexandre Duret-Lutz, Denis Poitrenaud, and Jean-Michel Couvreur. On-the-fly emptiness check of transition-based Streett automata. In Zhiming Liu and Anders P. Ravn, editors, Proceedings of the 7th International Symposium on Automated Technology for Verification and Analysis (ATVA'09), volume 5799 of Lecture Notes in Computer Science, pages 213–227. Springer, 2009. [ bib | DOI | pdf | slides ]
In the automata theoretic approach to model checking, checking a state-space S against a linear-time property φ can be done in O(|S|× 2O(|φ|)) time. When model checking under n strong fairness hypotheses expressed as a Generalized Büchi automaton, this complexity becomes O(|S|×2O(|φ|+n)).

Here we describe an algorithm to check the emptiness of Streett automata, which allows model checking under n strong fairness hypotheses in O(|S|× 2O(|φ|)×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.

[demaille.08.fsmnlp]
Akim Demaille, Alexandre Duret-Lutz, Florian Lesaint, Sylvain Lombardy, Jacques Sakarovitch, and Florent Terrones. An XML format proposal for the description of weighted automata, transducers, and regular expressions. In Proceedings of the seventh international workshop on Finite-State Methods and Natural Language Processing (FSMNLP'08), Ispra, Italia, September 2008. [ bib | pdf ]
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.

[baarir.07.msr]
Souheib Baarir and Alexandre Duret-Lutz. Test de vacuité pour automates de Büchi ensemblistes avec tests d'inclusion. In Actes du 6e Colloque Francophone sur la Modélisation des Systèmes Réactifs (MSR'07), pages 19–34. Hermes-Lavoisier, October 2007. [ bib ]
Nous présentons deux algorithmes d'emptiness check pour les automates de Büchi dont les états sont des ensembles qui peuvent s'inclure les uns les autres. Le premier est équivalent à un emptiness check traditionnel, mais utilise des tests d'inclusion pour diriger la construction à la volée de l'automate. Le second est beaucoup plus rapide, mais peut retourner de faux négatifs. Nous illustrons et évaluons l'amélioration avec une réduction basée sur les symétries.

[baarir.07.acsd]
Souheib Baarir and Alexandre Duret-Lutz. Emptiness check of powerset Büchi automata. In Proceedings of the 7th International Conference on Application of Concurrency to System Design (ACSD'07), pages 41–50. IEEE Computer Society, July 2007. [ bib | DOI | pdf | slides ]
We introduce two emptiness checks for Bü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.

[duret.07.phd]
Alexandre Duret-Lutz. Contributions à l'approche automate pour la vérification de propriétés de systèmes concurrents. PhD thesis, Université Pierre et Marie Curie (Paris 6), July 2007. [ bib | pdf | slides | www ]
[german.07.cae]
Daniel M. German, Lloyd Burchill, Alexandre Duret-Lutz, Sébastien Pérez-Duarte, Emmanuel Pérez-Duarte, and Josh Sommers. Flattening the viewable sphere. In Proceedings of the Third Eurographics Conference on Computational Aesthetics in Graphics, Visualization and Imaging (CAe'07), pages 23–28. Eurographics Association, 2007. Artistic Submission. [ bib | DOI | pdf ]
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.

[baarir.06.tr03]
Souheib Baarir and Alexandre Duret-Lutz. Emptiness check of powerset Büchi automata. Technical report 2006/003, Université Pierre et Marie Curie, LIP6-CNRS, Paris, France, October 2006. [ bib | pdf ]
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ü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.

[couvreur.05.spin]
Jean-Michel Couvreur, Alexandre Duret-Lutz, and Denis Poitrenaud. On-the-fly emptiness checks for generalized Büchi automata. In Patrice Godefroid, editor, Proceedings of the 12th International SPIN Workshop on Model Checking of Software, volume 3639 of Lecture Notes in Computer Science, pages 143–158. Springer, August 2005. [ bib | DOI | pdf | slides ]
Emptiness check is a key operation in the automata-theoretic approach to LTL verification. However, it is usually done on Büchi automata with a single u acceptance condition. We review existing on-the-fly emptiness-check algorithms for generalized Bü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.

[baarir.04.mascots]
Souheib Baarir, Jean-Michel Ilié, and Alexandre Duret-Lutz. Improving reachability analysis for partially symmetric high level petri nets. In Proceedings of the Poster Session of the 12th IEEE/ACM International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS'04), pages 5–8, Volendam, The Netherlands, October 2004. [ bib | DOI | pdf | poster ]
[duret.04.mascots]
Alexandre Duret-Lutz and Denis Poitrenaud. Spot: an extensible model checking library using transition-based generalized Büchi automata. In Proceedings of the 12th IEEE/ACM International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS'04), pages 76–83, Volendam, The Netherlands, October 2004. IEEE Computer Society. [ bib | DOI | pdf ]
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ü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.

[thierry-mieg.04.gl]
Yann Thierry-Mieg, Souheib Baarir, Alexandre Duret-Lutz, and Fabrice Kordon. Nouvelles techniques de model-checking pour la vérification de systèmes complexes. Génie Logiciel, (69):17–23, June 2004. [ bib | pdf ]
[burrus.03.mpool]
Nicolas Burrus, Alexandre Duret-Lutz, Thierry Géraud, David Lesage, and Raphaël Poss. A static C++ object-oriented programming (scoop) paradigm mixing benefits of traditional oop and generic programming. In Proceedings of the Workshop on Multiple Paradigm with OO Languages (MPOOL'03), Anaheim, California, October 2003. [ bib | pdf | proceedings ]
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.

[duret.03.msc]
Alexandre Duret-Lutz and Rachid Rebiha. Spot: une bibliothèque de vérification de propriétés de logique temporelle à temps linéaire. Master's thesis, DEA Systèmes Informatiques Répartis, Université de Paris 6, September 2003. [ bib | pdf ]
[xue.03.icip]
Heru Xue, Thierry Géraud, and Alexandre Duret-Lutz. Multi-band segmentation using morphological clustering and fusion; application to color image segmentation. In Proceedings of the IEEE International Conference on Image Processing (ICIP 2003), Barcelona, Spain, September 2003. [ bib | DOI ]
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.

[darbon.02.ismm]
Jérôme Darbon, Thierry Géraud, and Alexandre Duret-Lutz. Generic implementation of morphological image operators. In Mathematical Morphology, Proceedings of the 6th International Symposium (ISMM), pages 175–184, Sydney, Australia, April 2002. Sciro Publishing. [ bib | pdf ]
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.

[duret.01.ae]
Alexandre Duret-Lutz. Expression templates in Ada. In Proceedings of the 6th International Conference on Reliable Software Technologies (Ada-Europe'01), volume 2043 of Lecture Notes in Computer Science, pages 191–202, Leuven, Belgium, May 2001. ©Springer-Verlag. Best paper award. [ bib | DOI | pdf ]
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.

[geraud.01.ai]
Thierry Géraud, Yoann Fabre, and Alexandre Duret-Lutz. Applying generic programming to image processing. In M.H. Hamsa, editor, Proceedings of the IASTED International Conference on Applied Informatics (AI'01)–-Symposium Advances in Computer Applications, pages 577–581, Innsbruck, Austria, February 2001. ACTA Press. [ bib ]
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.

[duret.01.coots]
Alexandre Duret-Lutz, Thierry Géraud, and Akim Demaille. Design patterns for generic programming in C++. In Proceedings of the 6th USENIX Conference on Object-Oriented Technologies and Systems (COOTS'01), pages 189–202, San Antonio, Texas, USA, January 2001. USENIX Association. [ bib | pdf | .html ]
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.

[duret.00.gcseyrw]
Alexandre Duret-Lutz. Olena: a component-based platform for image processing, mixing generic, generative and OO programming. In Proceedings of 2nd International Symposium on Generative and Component-Based Software Engineering (GCSE 2000), pages 653–659, Erfurt, Germany, October 2000. Young Researchers Workshop (published in “Net.ObjectDays2000”). [ bib | .html ]
[geraud.00.icpr]
Thierry Géraud, Yoann Fabre, Alexandre Duret-Lutz, Dimitri Papadopoulos-Orfanos, and Jean-François Mangin. Obtaining genericity for image processing and pattern recognition algorithms. In Proceedings of the 15th International Conference on Pattern Recognition (ICPR'00), volume 4, pages 816–819, Barcelona, Spain, September 2000. IEEE Computer Society. [ bib ]
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.

[geraud.00.europlop]
Thierry Géraud and Alexandre Duret-Lutz. Generic programming redesign of patterns. In M. Devos and A. Rüping, editors, Proceedings of the 5th European Conference on Pattern Languages of Programs (EuroPLoP'00). UVK, Univ. Verlag, Konstanz, July 2000. [ bib | pdf ]
[duret.00.tr01]
Alexandre Duret-Lutz and Thierry Géraud. Improving object-oriented generic programming. Technical Report 0001, EPITA Research and Development Laboratory, Paris, April 2000. [ bib | pdf ]
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.

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 void foo(AbstractA&) for classic object-orientation, and from template<class A> void foo(A&) for classic generic programming, towards template<class A> void foo(ConceptA<A>&). This results in a better support of procedure overloading, which is of prime importance for libraries where each algorithm implementation can have numerous variations.

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.

[clouard.99.tr]
Régis Clouard, Abderrahim Elmoataz, François Angot, Olivier Lezoray, and Alexandre Duret-Lutz. Une bibliothèque et un environnement de programmation d'opérateurs de traitement d'images. Technical Report 99008, GREYC-ISMRA, Caen, France, November 1999. [ bib | http ]
[duret.99.tr03]
Alexandre Duret-Lutz and Thierry Géraud. Patrons de conception statiques pour la programmation générique en C++. Technical Report 9903, EPITA Research and Development Laboratory, Paris, September 1999. [ bib | pdf ]
[geraud.99.tr01]
Thierry Géraud and Alexandre Duret-Lutz. Composants génériques de calcul scientifique. Technical Report 9901, EPITA Research and Development Laboratory, Paris, March 1999. [ bib | pdf ]
Dans le cadre de l'écriture en C++ d'une bibliothèque de traitements d'images et d'un atelier de programmation par composants d'une chaîne de traitements, nous nous sommes fixés deux objectifs principaux : rendre les traitements génériques vis-à-vis du type de ses entrées sans entraîner de surcoût significatif à l'exécution, et pouvoir exécuter un traitement lorsqu'il a eté introduit ultérieurement à la compilation de l'atelier.

Le premier objectif est atteint a l'aide de programmation générique et de la traduction en polymorphisme statique de certains idiomes (design patterns) définis pour le polymorphisme dynamique. La problématique du second objectif est double. Tout d'abord, nous devions réaliser la mise en correspondance d'un traitement dont les entrées-sorties sont des types abstraits et de la routine générique, chargée du traitement, dont les paramètres sont des types concrets ; ensuite, nous devions pouvoir compiler et lier de nouveaux traitements a la volée, lors de l'exécution de l'atelier. Pour atteindre ce double objectif, nous utilisons de la programmation générative et nous pratiquons l'instanciation paresseuse (lazy) de code générique.

Les solutions que nous apportons permettent la gestion de composants réutilisables de calcul scientifique, ce qui, à notre connaissance, est original.