I am professor at EPITA Paris, part of the Automata and applications research group at LRE.
I work on linear temporal logic, ω-automata, and their application to model checking or reactive controler synthesis.
I develop and maintain Spot, a C++ library for doing the above.
Effective Reductions of Mealy Machines
Florian Renkin, Philipp Schlehuber-Caissier, Alexandre Duret-Lutz, Adrien Pommellet. Effective Reductions of Mealy Machines. 42nd International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2022), Jun 2022, Lucca, Italy. ⟨hal-03695793⟩
Practical Applications of the Alternating Cycle Decomposition
Antonio Casares, Alexandre Duret-Lutz, Klara J. Meyer, Florian Renkin, Salomon Sickert. Practical Applications of the Alternating Cycle Decomposition. Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'22), Apr 2022, Munich, Germany. pp.99--117, ⟨10.1007/978-3-030-99527-0_6⟩. ⟨hal-04580366⟩
From Spot 2.0 to Spot 2.10: What's New?
Alexandre Duret-Lutz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi, et al.. From Spot 2.0 to Spot 2.10: What's New?. Proceedings of the 34th International Conference on Computer Aided Verification (CAV'22), Aug 2022, Technion, Israel. ⟨hal-03695817⟩
Practical "Paritizing" of Emerson-Lei Automata
Florian Renkin, Alexandre Duret-Lutz, Adrien Pommellet. Practical "Paritizing" of Emerson-Lei Automata. 18th International Symposium on Automated Technology for Verification and Analysis (ATVA'20), Oct 2020, Hanoi, Vietnam. pp.127-143, ⟨10.1007/978-3-030-59152-6_7⟩. ⟨hal-02891970⟩
Seminator 2 can complement generalized Büchi automata via improved semi-determinization
František Blahoudek, Alexandre Duret-Lutz, Jan Strejček. Seminator 2 can complement generalized Büchi automata via improved semi-determinization. Proceedings of the 32nd International Conference on Computer-Aided Verification (CAV'20), Jul 2020, Los Angeles, United States. pp.15--27, ⟨10.1007/978-3-030-53291-8_2⟩. ⟨hal-04580364⟩
Model checking with generalized Rabin and Fin-less automata
Vincent Bloemen, Alexandre Duret-Lutz, Jaco van De Pol. Model checking with generalized Rabin and Fin-less automata. International Journal on Software Tools for Technology Transfer, 2019, 21 (3), pp.307--324. ⟨10.1007/s10009-019-00508-4⟩. ⟨hal-04580365⟩
Generic Emptiness Check for Fun and Profit
Christel Baier, František Blahoudek, Alexandre Duret-Lutz, Joachim Klein, David Müller, et al.. Generic Emptiness Check for Fun and Profit. Proceedings of the 17th International Symposium on Automated Technology for Verification and Analysis (ATVA'19), Oct 2019, Taipei, Taiwan. pp.445--461, ⟨10.1007/978-3-030-31784-3_26⟩. ⟨hal-04580363⟩
Parallel Explicit Model Checking for Generalized Büchi Automata
Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud. Parallel Explicit Model Checking for Generalized Büchi Automata. 21th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015, Apr 2015, London, United Kingdom. pp.613-627, ⟨10.1007/978-3-662-46681-0_56⟩. ⟨hal-01216666⟩
SAT-Based Minimization of Deterministic ω-Automata
Souheib Baarir, Alexandre Duret-Lutz. SAT-Based Minimization of Deterministic ω-Automata. Logic for Programming, Artificial Intelligence, and Reasoning, Nov 2015, Suva, Fiji. pp.79--87, ⟨10.1007/978-3-662-48899-7_6⟩. ⟨hal-01462805⟩
A Type System for Weighted Automata and Rational Expressions
Akim Demaille, Alexandre Duret-Lutz, Sylvain Lombardy, Luca Saiu, Jacques Sakarovitch. A Type System for Weighted Automata and Rational Expressions. Implementation and Application of Automata, CIAA 2014, Jul 2014, Giessen, Germany. pp.162--175, ⟨10.1007/978-3-319-08846-4_12⟩. ⟨hal-01069654⟩
Symbolic Model Checking of stutter invariant properties Using Generalized Testing Automata
Ala Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon, Yann Thierry-Mieg. Symbolic Model Checking of stutter invariant properties Using Generalized Testing Automata. 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2014, Apr 2014, Grenoble, France. pp.440-454, ⟨10.1007/978-3-642-54862-8_38⟩. ⟨hal-01216559⟩
Implementation Concepts in Vaucanson 2
Akim Demaille, Alexandre Duret-Lutz, Sylvain Lombardy, Jacques Sakarovitch. Implementation Concepts in Vaucanson 2. Implementation and Application of Automata, CIAA 2013, Jul 2013, Halifax, Canada. pp.122-133, ⟨10.1007/978-3-642-39274-0_12⟩. ⟨hal-00845816⟩
Three SCC-based Emptiness Checks for Generalized Büchi Automata
Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud. Three SCC-based Emptiness Checks for Generalized Büchi Automata. 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'13), Dec 2013, Stellenbosch, South Africa. pp.668-682, ⟨10.1007/978-3-642-45221-5_44⟩. ⟨hal-01066992⟩
Strength-Based Decomposition of the Property Büchi Automaton for Faster Model Checking
Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud. Strength-Based Decomposition of the Property Büchi Automaton for Faster Model Checking. 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'13), Mar 2013, Rome, Italy. pp.580-593, ⟨10.1007/978-3-642-36742-7_42⟩. ⟨hal-01066995⟩
Model Checking using Generalized Testing Automata
Ala Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon. Model Checking using Generalized Testing Automata. LNCS Transactions on Petri Nets and Other Models of Concurrency, 2012, 7400 (VI), pp.94-122. ⟨10.1007/978-3-642-35179-2_5⟩. ⟨hal-00855991⟩
{Generalized Büchi Automata versus Testing Automata for Model Checking}
Ala Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon. {Generalized Büchi Automata versus Testing Automata for Model Checking}. 2nd workshop on Scalable and Usable Model Checking for Petri Nets and other models of Concurrency (SUMo 2011), Jun 2011, Newcastle, United Kingdom. pp.65-79. ⟨hal-01282490⟩
Self-Loop Aggregation Product - A New Hybrid Approach to On-the-Fly LTL Model Checking
Alexandre Duret-Lutz, Kaïs Klai, Denis Poitrenaud, Yann Thierry-Mieg. Self-Loop Aggregation Product - A New Hybrid Approach to On-the-Fly LTL Model Checking. 9th International Symposium on Automated Technology for Verification and Analysis (ATVA'11), Oct 2011, Taipei, Taiwan. pp.336-350, ⟨10.1007/978-3-642-24372-1_24⟩. ⟨hal-01288132⟩
On-the-fly Emptiness Check of Transition-Based Streett Automata
Alexandre Duret-Lutz, Denis Poitrenaud, Jean-Michel Couvreur. On-the-fly Emptiness Check of Transition-Based Streett Automata. 7th International Symposium on Automated Technology for Verification and Analysis, ATVA 2009, Oct 2009, Macao, China. pp.213-227, ⟨10.1007/978-3-642-04761-9_17⟩. ⟨hal-00468314⟩
An XML Format Proposal for the Description of Weighted Automata, Transducers and Regular Expressions
Akim Demaille, Alexandre Duret-Lutz, Florian Lesaint, Sylvain Lombardy, Jacques Sakarovitch, et al.. An XML Format Proposal for the Description of Weighted Automata, Transducers and Regular Expressions. Finite-State Methods and Natural Language Processing, 2008, Ispra, Italy. pp.199-206. ⟨hal-00859354⟩
Emptiness Check of Powerset Buchi Automata
Souheib Baarir, Alexandre Duret-Lutz. Emptiness Check of Powerset Buchi Automata. 7th International Conference on Application of Concurrency to System Design (ACSD'07), Jul 2007, Bratislava, Slovakia. pp.41-50, ⟨10.1109/ACSD.2007.49⟩. ⟨hal-01305778⟩
Emptiness Check of Powerset Büchi Automata using Inclusion Tests
Souheib Baarir, Alexandre Duret-Lutz. Emptiness Check of Powerset Büchi Automata using Inclusion Tests. [Technical Report] lip6.2006.003, LIP6. 2006. ⟨hal-02545696⟩
On-the-Fly Emptiness Checks for Generalized Büchi Automata
Jean-Michel Couvreur, Alexandre Duret-Lutz, Denis Poitrenaud. On-the-Fly Emptiness Checks for Generalized Büchi Automata. 12th International SPIN Workshop on Model Checking of Software, Aug 2005, San Francisco, United States. pp.169-184, ⟨10.1007/11537328_15⟩. ⟨hal-01487942⟩
Nouvelles techniques de Model Checking pour la vérification de systèmes complexes
Yann Thierry-Mieg, Souheib Baarir, Alexandre Duret-Lutz, Fabrice Kordon. Nouvelles techniques de Model Checking pour la vérification de systèmes complexes. Génie logiciel : le magazine de l'ingénierie du logiciel et des systèmes, 2004, 69, pp.17-23. ⟨hal-01175956⟩
Improving Reachability Analysis for Partially Symmetric High Level Petri Nets
Souheib Baarir, Jean-Michel Ilié, Alexandre Duret-Lutz. Improving Reachability Analysis for Partially Symmetric High Level Petri Nets. 12th IEEE/ACM International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS '04), Oct 2004, Volendam, Netherlands. pp.5-8. ⟨hal-01496154⟩
SPOT: an Extensible Model Checking Library using Transition-based Generalized Büchi Automata
Alexandre Duret-Lutz, Denis Poitrenaud. SPOT: an Extensible Model Checking Library using Transition-based Generalized Büchi Automata. 12th IEEE/ACM International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS '04), Oct 2004, Volendam, Netherlands. pp.76-83, ⟨10.1109/MASCOT.2004.1348184⟩. ⟨hal-01496158⟩