An ω-word (omega-word) is a word of infinite length. In our context, each letter is used to describe the state of a system at a given time, and the sequence of letters shows the evolution of the system as the (discrete) time is incremented. An ω-automaton is used to represent sets of ω-words. Those look like the classical Nondeterministic Finite Automata in the sense that they also have states and transitions. However, ω-automata recognize ω-words instead of finite words. In this context, the notion of final state makes no sense, and is replaced by the notion of acceptance condition: a run of the automaton (i.e., an infinite sequence alternating states and edges in a way that is compatible with the structure of the automaton) is accepting if it satisfies the constraint given by the acceptance condition.
In the Automata and Applications group, we are developing and implementing algorithms for the manipulation of ω-automata for model-checking purposes, among which:
- conversion between various acceptance conditions [1,2]
- translations between logics (LTL, PSL) and ω-automata [3,4]
- minimization, determinization, complementation and emptiness checking [5-9]
- state-space reduction and exploration [10,11]
Another application of ω-automata that the group is working on is the synthesis of reactive controllers [12]. The goal is to automatically synthesize a control law, such as an AIGER circuit, from a high-level specification, typically given in LTL. This specification is first translated into an ω-automaton, which is then turned into a two-player game: the environment defines which events may occur, and the system must respond in a way that ensures the specification is satisfied. A winning strategy for the system can then be extracted and turned into an executable controller.
The team develops and maintains a wide range of algorithms in Spot, a free and open-source software library, to manipulate ω-automata and temporal logics specifically for applications in model checking and controller synthesis [13].
Related Publications
[1]
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. https://doi.org/10.1007/s10009-019-00508-4.
[2]
Florian Renkin • Alexandre Duret-Lutz • Adrien Pommellet. "Practical "Paritizing" of Emerson--Lei Automata". Proceedings of the 18th International Symposium on Automated Technology for Verification and Analysis (ATVA'20). 2020. https://doi.org/10.1007/978-3-030-59152-6_7.
[3]
František Blahoudek • Alexandre Duret-Lutz • Vojtčech Rujbr • Jan Strejček. "On Refinement of Büchi Automata for Explicit Model Checking". Proceedings of the 22th International SPIN Symposium on Model Checking of Software (SPIN'15). 2015. https://doi.org/10.1007/978-3-319-23404-5_6.
[4]
Alexandre Duret-Lutz. "LTL Translation Improvements in Spot 1.0". International Journal on Critical Computer-Based Systems. 2014. https://doi.org/10.1504/IJCCBS.2014.059594.
[5]
Souheib Baarir • Alexandre Duret-Lutz. "SAT-based Minimization of Deterministic $\omega$-Automata". Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'15). 2015. https://doi.org/10.1007/978-3-662-48899-7_6.
[6]
František Blahoudek • Alexandre Duret-Lutz • Mikuláš Klokočka and Mojmír Křetínský • Jan Strejček. "Seminator: A Tool for Semi-Determinization of Omega-Automata". Proceedings of the 21th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LP<AR'17). 2017. https://doi.org/10.29007/k5nl.
[7]
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). 2020. https://doi.org/10.1007/978-3-030-53291-8_2.
[8]
Christel Baier • František Blahoudek • Alexandre Duret-Lutz and Joachim Klein • David Müller • Jan Strejček. "Generic Emptiness Check for Fun and Profit". Proceedings of the 17th International Symposium on Automated Technology for Verification and Analysis (ATVA'19). 2019. https://doi.org/10.1007/978-3-030-31784-3_26.
[9]
Alexandre Duret-Lutz • Denis Poitrenaud • Jean-Michel Couvreur. "On-the-fly Emptiness Check of Transition-based Streett Automata". Proceedings of the 7th International Symposium on Automated Technology for Verification and Analysis (ATVA'09). 2009. https://doi.org/10.1007/978-3-642-04761-9_17.
[10]
Florian Renkin • Philipp Schlehuber-Caissier and Alexandre Duret-Lutz • Adrien Pommellet. "Effective Reductions of Mealy Machines". Proceedings of the 42nd International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE'22). 2022. https://doi.org/10.1007/978-3-031-08679-3_8.
[11]
Alexandre Duret-Lutz • Fabrice Kordon • Denis Poitrenaud • Étienne Renault. "Heuristics for Checking Liveness Properties with Partial Order Reductions". Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA'16). 2016. https://doi.org/10.1007/978-3-319-46520-3_22.
[12]
Jacobs, Swen • Basset, Nicolas • Bloem, Roderick • Brenguier, Romain • Colange, Maximilien • Faymonville, Peter • Finkbeiner, Bernd • Khalimov, Ayrat • Klein, Felix • Michaud, Thibaud and Pérez, Guillermo A. • Raskin, Jean-François • Sankur, Ocan and Tentrup, Leander. "The 4th Reactive Synthesis Competition (SYNTCOMP 2017): Benchmarks, Participants & Results". Proceedings Sixth Workshop on Synthesis. 2017. https://doi.org/10.4204/EPTCS.260.10.
[13]
Alexandre Duret-Lutz • Étienne Renault • Maximilien Colange and Florian Renkin • Alexandre Gbaguidi Aisse • Philipp Schlehuber-Caissier • Thomas Medioni • Antoine Martin • Jérôme Dubois • Clément Gillard • Henrich Lauko. "From Spot 2.0 to Spot 2.10: What's New?". Proceedings of the 34th International Conference on Computer Aided Verification (CAV'22). 2022. https://doi.org/10.1007/978-3-031-13188-2_9.