Showing 1–4 of 4 results for author: Renkin, F

From Spot 2.0 to Spot 2.10: What's New?

Authors: Alexandre Duret-Lutz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard, Henrich Lauko

Abstract: Spot is a C ++ 17 library for LTL and $ω$-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 $ω$-automata with arbitrary acceptance conditions, and the last version presented at a conference. Since then, Spot has been extended with several feature… ▽ More Spot is a C ++ 17 library for LTL and $ω$-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 $ω$-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. △ Less

Submitted 20 June, 2022; originally announced June 2022.

Journal ref: Proceedings of the 34th International Conference on Computer Aided Verification (CAV'22), Aug 2022, Technion, Israel

Effective Reductions of Mealy Machines

Authors: Florian Renkin, Philipp Schlehuber-Caissier, Alexandre Duret-Lutz, 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 MeMin and solves the minimization problem, the latter is a novel approach derived from simulationbased reductions but may not guarantee a minimized machine. However, we argue that it offers a good enough compromise between the size… ▽ More 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 MeMin and solves the minimization problem, the latter is a novel approach derived from simulationbased 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 MeMin on a large collection of test cases made of well-known instances as well as new ones. △ Less

Submitted 21 June, 2022; originally announced June 2022.

Journal ref: 42nd International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2022), Jun 2022, Lucca, Italy

The Reactive Synthesis Competition (SYNTCOMP): 2018-2021

Authors: Swen Jacobs, Guillermo A. Perez, Remco Abraham, Veronique Bruyere, Michael Cadilhac, Maximilien Colange, Charly Delfosse, Tom van Dijk, Alexandre Duret-Lutz, Peter Faymonville, Bernd Finkbeiner, Ayrat Khalimov, Felix Klein, Michael Luttenberger, Klara Meyer, Thibaud Michaud, Adrien Pommellet, Florian Renkin, Philipp Schlehuber-Caissier, Mouhammad Sakr, Salomon Sickert, Gaetan Staquet, Clement Tamines, Leander Tentrup, Adam Walker

Abstract: We report on the last four editions of the reactive synthesis competition (SYNTCOMP 2018-2021). We briefly describe the evaluation scheme and the experimental setup of SYNTCOMP. Then, we introduce new benchmark classes that have been added to the SYNTCOMP library and give an overview of the participants of SYNTCOMP. Finally, we present and analyze the results of our experimental evaluations, inclu… ▽ More We report on the last four editions of the reactive synthesis competition (SYNTCOMP 2018-2021). We briefly describe the evaluation scheme and the experimental setup of SYNTCOMP. Then, we introduce new benchmark classes that have been added to the SYNTCOMP library and give an overview of the participants of SYNTCOMP. Finally, we present and analyze the results of our experimental evaluations, including a ranking of tools with respect to quantity and quality - that is, the total size in terms of logic and memory elements - of solutions. △ Less

Submitted 6 May, 2024; v1 submitted 1 June, 2022; originally announced June 2022.

Comments: accepted for publication in STTT

Improvements to ltlsynt

Authors: Florian Renkin, Philipp Schlehuber, Alexandre Duret-Lutz, Adrien Pommellet

Abstract: ltlsynt is a tool for LTL reactive synthesis. We summarize its evolution since 2018. ltlsynt is a tool for LTL reactive synthesis. We summarize its evolution since 2018. △ Less

Submitted 14 January, 2022; originally announced January 2022.

Journal ref: 10th Workshop on Synthesis, Jul 2021, Los Angeles, United States