Florian Renkin

@article{renkin.23.fmsd,
author = {Florian Renkin and Philipp Schlehuber-Caissier and Alexandre Duret-Lutz and Adrien Pommellet},
abstract = {\texttt{ltlsynt} is a tool for synthesizing a reactive circuit satisfying a specification expressed as an LTL formula. \texttt{ltlsynt} generally follows a textbook approach: the LTL specification is translated into a parity game whose winning strategy can be seen as a Mealy machine modeling a valid controller. This article details each step of this approach, and presents various refinements integrated over the years. Some of these refinements are unique to \texttt{ltlsynt}: for instance, \texttt{ltlsynt} supports multiple ways to encode a Mealy machine as an AIG circuit, features multiple simplification algorithms for the intermediate Mealy machine, and bypasses the usual game-theoretic approach for some subclasses of LTL formulas in favor of more direct constructions.},
doi = {10.1007/s10703-022-00407-6},
journal = {Formal Methods in System Design},
keywords = {reactive synthesis, Mealy machines, parity automata, parity games, LTL formulas},
title = {Dissecting ltlsynt},
url = {https://doi.org/10.1007/s10703-022-00407-6},
day = 14,
month = jul,
year = 2023
}

@article{renkin.23.scp,
author = {Florian Renkin and Alexandre Duret-Lutz and Adrien Pommellet and Philipp Schlehuber-Caissier},
abstract = {We present functions for reducing Mealy machines, initially detailed in our FORTE'22 article. These functions are now integrated into Spot 2.11.2, where they are used as part of the \texttt{ltlsynt} tool for reactive synthesis. Of course, since Spot is a library, these functions can also be used on their own, and we provide Python bindings for easy experiments. The reproducible capsule benchmarks these functions on Mealy machines from various sources, and compare them to the \textsc{MeMin} tool.},
doi = {10.1016/j.scico.2023.102995},
issn = {0167-6423},
journal = {Science of Computer Programming},
keywords = {Mealy machines, synthesis, SAT},
title = {The {M}ealy-Machine Reduction Functions of {S}pot},
url = {https://www.sciencedirect.com/science/article/pii/S0167642323000771},
year = 2023
}

@misc{jacobs.22.arxiv,
author = {Swen Jacobs and Guillermo Alberto~Perez and Remco Abraham and V{\'e}ronique Bruy{\`e}re and Micha{\¨e}l Cadilhac and Maximilien Colange and Charly Delfosse and Tom van~Dijk and Alexandre Duret-Lutz and Peter Faymonville and Bernd Finkbeiner and Ayrat Khalimov and Felix Klein and Michael Luttenberger and Klara~J. Meyer and Thibaud Michaud and Adrien Pommellet and Florian Renkin and Philipp Schlehuber-Caissier and Mouhammad Sakr and Salomon Sickert and Ga{\¨e}tan Staquet and Cl{\'e}ment Tamines and Leander Tentrup and Adam Walker},
copyright = {Creative Commons Attribution 4.0 International},
doi = {10.48550/ARXIV.2206.00251},
keywords = {Reactive synthesis, algorithmic verification, zero-sum games},
publisher = {arXiv},
title = {The Reactive Synthesis Competition (SYNTCOMP): 2018-2021},
url = {https://arxiv.org/abs/2206.00251},
year = 2022
}

@inproceedings{duretlutz.22.cav,
author = {Alexandre Duret-Lutz and Etienne Renault and Maximilien Colange and Florian Renkin and Alexandre Gbaguidi~Aisse and Philipp Schlehuber-Caissier and Thomas Medioni and Antoine Martin and J{\'e}r{\^o}me Dubois and Cl{\'e}ment Gillard and Henrich Lauko},
abstract = {Spot is a C++17 library for LTL and $\omega$-automata manipulation, with command-line utilities, and Python bindings. This paper summarizes its evolution over the past six years, since the release of Spot 2.0, which was the first version to support $\omega$-automata with arbitrary acceptance conditions, and the last version presented at a conference. Since then, Spot has been extended with several features such as acceptance transformations, alternating automata, games, LTL synthesis, and more. We also shed some lights on the data-structure used to store automata.},
booktitle = {Proceedings of the 34th International Conference on Computer Aided Verification (CAV'22)},
doi = {10.1007/978-3-031-13188-2_9},
pages = {174--187},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {From {S}pot 2.0 to {S}pot 2.10: What's New?},
url = {https://link.springer.com/chapter/10.1007/978-3-031-13188-2_9},
volume = {13372},
month = aug,
year = 2022
}

@inproceedings{renkin.22.forte,
author = {Florian Renkin and Philipp Schlehuber-Caissier and Alexandre Duret-Lutz and Adrien Pommellet},
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 \textsc{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.},
booktitle = {Proceedings of the 42nd International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE'22)},
doi = {10.1007/978-3-031-08679-3_8},
pages = {170--187},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Effective Reductions of {M}ealy Machines},
url = {https://link.springer.com/chapter/10.1007/978-3-031-08679-3_8},
volume = {13273},
month = jun,
year = 2022
}

@inproceedings{casares.22.tacas,
author = {Antonio Casares and Alexandre Duret-Lutz and Klara~J. Meyer and Florian Renkin and Salomon Sickert},
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.},
booktitle = {Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
doi = {10.1007/978-3-030-99527-0_6},
pages = {99--117},
series = {Lecture Notes in Computer Science},
title = {Practical Applications of the {A}lternating {C}ycle {D}ecomposition},
url = {https://link.springer.com/chapter/10.1007/978-3-030-99527-0_6},
month = apr,
year = 2022
}

@misc{renkin.21,
author = {Florian Renkin and Philipp Schlehuber-Caissier and Alexandre Duret-Lutz and Adrien Pommellet},
abstract = {We summarize \texttt{ltlsynt}'s evolution since 2018.},
howpublished = {Presented at the SYNT'21 workshop, without proceedings.},
title = {Improvements to \texttt{ltlsynt}},
month = jul,
year = 2021
}

@inproceedings{renkin.20.atva,
author = {Florian Renkin and Alexandre Duret-Lutz and Adrien Pommellet},
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.},
booktitle = {Proceedings of the 18th International Symposium on Automated Technology for Verification and Analysis (ATVA'20)},
doi = {10.1007/978-3-030-59152-6_7},
pages = {127--143},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Practical ``Paritizing'' of Emerson-Lei Automata},
url = {https://link.springer.com/chapter/10.1007/978-3-030-59152-6_7},
volume = {12302},
month = oct,
year = 2020
}