Algorithmic verification; Reactive synthesis; Zero-sum games; Evaluation scheme; Experimental evaluation; Logic-elements; Memory element; Zero-sum game; Software; Information Systems
Résumé :
[en] 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.
Disciplines :
Sciences informatiques
Auteur, co-auteur :
Jacobs, Swen; CISPA Helmholtz Center for Information Security, Saarbrücken, Germany
Pérez, Guillermo A.; University of Antwerp – Flanders Make, Antwerpen, Belgium
Abraham, Remco; University of Twente, Enschede, Netherlands
Bruyère, Véronique; University of Mons, Mons, Belgium
Cadilhac, Michaël; DePaul University, Chicago, United States
Colange, Maximilien; EPITA Research Laboratory, France
Delfosse, Charly; University of Mons, Mons, Belgium
van Dijk, Tom; University of Twente, Enschede, Netherlands
Duret-Lutz, Alexandre; EPITA Research Laboratory, France
Abraham, R.: Symbolic LTL reactive synthesis (2021). http://essay.utwente.nl/87386/
K.R. Apt E. Grädel Lectures in Game Theory for Computer Scientists 2011 Cambridge Cambridge University Press http://www.cambridge.org/gb/knowledge/isbn/item5760379
T. Babiak T. Badie A. Duret-Lutz et al. Compositional approach to suspension and other improvements to LTL translation Proceedings of the 20th International SPIN Symposium on Model Checking of Software (SPIN’13) 2013 Berlin Springer 81 98 10.1007/978-3-642-39176-7_6
T. Babiak F. Blahoudek A. Duret-Lutz et al. D. Kroening C.S. Pasareanu et al. The Hanoi omega-automata format Computer Aided Verification – 27th International Conference, CAV 2015 2015 Berlin Springer 479 486 10.1007/978-3-319-21690-4_31
C. Baier J. Katoen Principles of Model Checking 2008 Cambridge MIT Press
A. Balint D. Diepold D. Gall et al. C.A.C. Coello et al. EDACC – an advanced platform for the experiment design, administration and analysis of empirical algorithms Selected Papers 2011 Berlin Springer 586 599 10.1007/978-3-642-25566-3_46
Biere, A.: Hardware model checking competition (2007). http://fmv.jku.at/hwmcc/
Biere, A.: Aiger format and toolbox (2011). http://fmv.jku.at/aiger/
R. Bloem R. Könighofer M. Seidl K.L. McMillan X. Rival Sat-based synthesis methods for safety specs Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014 2014 Berlin Springer 1 20 10.1007/978-3-642-54013-4_1
Bohy, A.: Antichain based algorithms for the synthesis of reactive systems. PhD thesis, University of Mons (2014)
A. Bohy V. Bruyère E. Filiot et al. P. Madhusudan S.A. Seshia et al. Acacia+, a tool for LTL synthesis CAV, LNCS 2012 Berlin Springer 652 657 10.1007/978-3-642-31424-7_45
U. Boker O. Kupferman A. Steinitz K. Lodaya M. Mahajan Parityizing rabin and streett IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010 2010 412 423 10.4230/LIPIcs.FSTTCS.2010.412 Schloss Dagstuhl – Leibniz-Zentrum für Informatik
V. Bruyère G.A. Pérez J. Raskin et al. E. Filiot R.M. Jungers I. Potapov et al. Partial solvers for generalized parity games Reachability Problems – 13th International Conference, RP 2019 2019 Berlin Springer 63 78 10.1007/978-3-030-30806-3_6
M. Cadilhac G.A. Pérez Acacia-bonsai: a modern implementation of downset-based LTL realizability Tools and Algorithms for the Construction and Analysis of Systems – 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023 2023 Berlin Springer 192 207
A. Camacho C.J. Muise J.A. Baier et al. LTL realizability via safety and reachability games IJCAI 2018 4683 4691 ijcai.org
A. Casares T. Colcombet N. Fijalkow N. Bansal E. Merelli J. Worrell Optimal transformations of games and automata using Muller conditions 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021 2021 123:1 123:14 10.4230/LIPIcs.ICALP.2021.123 Schloss Dagstuhl – Leibniz-Zentrum für Informatik
A. Casares A. Duret-Lutz K.J. Meyer et al. D. Fisman G. Rosu et al. Practical applications of the alternating cycle decomposition Tools and Algorithms for the Construction and Analysis of Systems – 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022 2022 Berlin Springer 99 117 10.1007/978-3-030-99527-0_6
K. Chatterjee T.A. Henzinger N. Piterman H. Seidl Generalized parity games Foundations of Software Science and Computational Structures, 10th International Conference, FOSSACS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 2007 Berlin Springer 153 167 10.1007/978-3-540-71389-0_12
A. Church Application of recursive arithmetic to the problem of circuit synthesis Summaries of the Summer Institute of Symbolic Logic 1957 Providence Am. Math. Soc. 3 50
Church, A.: Logic, arithmetic, and automata. J. Symb. Log. 29(4) (1964)
E.M. Clarke T.A. Henzinger H. Veith et al. Handbook of Model Checking 2018 Berlin Springer 10.1007/978-3-319-10575-8
L. de Alfaro P. Roy Solving games via three-valued abstraction refinement Inf. Comput. 2010 208 6 666 676 2663523 10.1016/j.ic.2009.05.007 https://doi.org/10.1016/j.ic.2009.05.007
M. De Berg O. Cheong M.J. van Kreveld et al. Computational Geometry: Algorithms and Applications 2008 3 Berlin Springer 10.1007/978-3-540-77974-2 https://www.worldcat.org/oclc/227584184
A. Duret-Lutz A. Lewkowicz A. Fauchille et al. Spot 2.0 — a framework for LTL and ω-automata manipulation Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA’16) 2016 Berlin Springer 122 129 10.1007/978-3-319-46520-3_8
R. Ehlers Symbolic bounded synthesis International Conference on Computer Aided Verification 2010 Berlin Springer 365 379 10.1007/978-3-642-14295-6_33
R. Ehlers Unbeast: symbolic bounded synthesis International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2011 Berlin Springer 272 275
J. Esparza J. Křetínský S. Sickert A. Dawar E. Grädel One theorem to rule them all: a unified translation of LTL into ω-automata Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS’18) 2018 New York ACM 384 393 10.1145/3209108.3209161
J. Esparza J. Kretínský S. Sickert A unified translation of linear temporal logic to ω-automata J. ACM 2020 67 6 33:1 33:61 4174098 10.1145/3417995
P. Faymonville B. Finkbeiner L. Tentrup R. Majumdar V. Kuncak Bosy: an experimentation framework for bounded synthesis Computer Aided Verification – 29th International Conference, CAV 2017 2017 Berlin Springer 325 332 10.1007/978-3-319-63390-9_17
B. Finkbeiner F. Klein S. Chaudhuri A. Farzan Bounded cycle synthesis Proceedings, Part I 2016 Berlin Springer 118 135 10.1007/978-3-319-41528-4_7
B. Finkbeiner F. Klein R. Piskac et al. R.A. Eisenberg et al. Synthesizing functional reactive programs Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell, Haskell@ICFP 2019 2019 New York ACM 162 175 10.1145/3331545.3342601
B. Finkbeiner F. Klein R. Piskac et al. I. Dillig S. Tasiran et al. Temporal stream logic: synthesis beyond the bools Computer Aided Verification – 31st International Conference, CAV 2019 2019 Berlin Springer 609 629 10.1007/978-3-030-25540-4_35
B. Finkbeiner G. Geier N. Passing Specification decomposition for reactive synthesis Proceedings for the 13th NASA Formal Methods Symposium (NFM’21) 2021 10.1007/978-3-030-76384-8_8
O. Friedmann M. Lange Z. Liu A.P. Ravn Solving parity games in practice Automated Technology for Verification and Analysis, 7th International Symposium, ATVA 2009 2009 Berlin Springer 182 196 10.1007/978-3-642-04761-9_15
G. Geier P. Heim F. Klein et al. C.W. Barrett J. Yang et al. Syntroids: synthesizing a game for FPGAs using temporal logic specifications Formal Methods in Computer Aided Design, FMCAD 2019 2019 Los Alamitos IEEE 138 146 10.23919/FMCAD.2019.8894261
Jacobs, S.: Extended AIGER format for synthesis. CoRR (2014). http://arxiv.org/abs/1405.5793. arXiv:1405.5793
Jacobs, S., Perez, G.A.: Data and scripts used for the SYNTCOMP report 2018–2021 (2023). https://doi.org/10.5281/zenodo.7588780
S. Jacobs M. Sakr A. Silva K.R.M. Leino AIGEN: random generation of symbolic transition systems Computer Aided Verification – 33rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021, Proceedings, Part II 2021 Berlin Springer 435 446 10.1007/978-3-030-81688-9_20
S. Jacobs F. Klein S. Schirmer R. Piskac R. Dimitrova A high-level LTL synthesis format: TLSF v1.1 Proceedings Fifth Workshop on Synthesis, SYNT@CAV 2016 2016 112 132 10.4204/EPTCS.229.10
S. Jacobs N. Basset R. Bloem et al. D. Fisman S. Jacobs et al. The 4th reactive synthesis competition (SYNTCOMP 2017): benchmarks, participants & results Proceedings Sixth Workshop on Synthesis, SYNT@CAV 2017 2017 116 143 10.4204/EPTCS.260.10
S. Jacobs R. Bloem R. Brenguier et al. The first reactive synthesis competition (SYNTCOMP 2014) Int. J. Softw. Tools Technol. Transf. 2017 19 3 367 390 10.1007/s10009-016-0416-3 https://doi.org/10.1007/s10009-016-0416-3
J. Kretínský T. Meggendorfer S. Sickert S.K. Lahiri C. Wang Owl: a library for ω-words, automata, and LTL Automated Technology for Verification and Analysis – 16th International Symposium, ATVA 2018 2018 Berlin Springer 543 550 10.1007/978-3-030-01090-4_34
O. Lijzenga T. van Dijk J. Raskin D. Bresolin Symbolic parity game solvers that yield winning strategies Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2020 2020 18 32 10.4204/EPTCS.326.2
Luttenberger, M.: Strategy iteration using non-deterministic strategies for solving parity games. CoRR (2008). http://arxiv.org/abs/0806.2923. arXiv:0806.2923
M. Luttenberger P.J. Meyer S. Sickert Practical synthesis of reactive systems from LTL specifications via parity games Acta Inform. 2020 57 1–2 3 36 4072241 10.1007/s00236-019-00349-3
Meyer, P.J., Sickert, S.: Modernising Strix. Presented at the 10th Workshop on Synthesis (2021)
P.J. Meyer S. Sickert M. Luttenberger H. Chockler G. Weissenbacher Strix: explicit reactive synthesis strikes back! Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018 2018 Berlin Springer 578 586 10.1007/978-3-319-96145-3_31
D. Müller S. Sickert P. Bouyer A. Orlandini P.S. Pietro LTL to deterministic Emerson–Lei automata Proceedings of the Eighth International Symposium on Games, Automata, Logics and Formal Verification (GandALF’17) 2017 180 194 10.4204/EPTCS.256.13
Pérez, G.A.: The extended HOA format for synthesis. CoRR (2019). http://arxiv.org/abs/1912.05793. arXiv:1912.05793
Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. Log. Methods Comput. Sci. 3(3) (2007). https://doi.org/10.2168/LMCS-3(3:5)2007
A. Pnueli The temporal logic of programs 18th Annual Symposium on Foundations of Computer Science 1977 Providence IEEE Comput. Soc. 46 57 10.1109/SFCS.1977.32
F. Renkin A. Duret-Lutz A. Pommellet Practical “paritizing” of Emerson–Lei automata Proceedings of the 18th International Symposium on Automated Technology for Verification and Analysis (ATVA’20) 2020 Berlin Springer 127 143 10.1007/978-3-030-59152-6_7
Renkin, F., Schlehuber, P., Duret-Lutz, A., et al.: Improvements to ltlsynt. Presented at the 10th Workshop on Synthesis (2021) https://hal.archives-ouvertes.fr/hal-03523385
F. Renkin P. Schlehuber-Caissier A. Duret-Lutz et al. Effective reductions of Mealy machines Proceedings of the 42nd International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE’22) 2022 Berlin Springer 114 130 10.1007/978-3-031-08679-3_8
S. Safra On the complexity of omega-automata 29th Annual Symposium on Foundations of Computer Science, White Plains 1988 New York IEEE Comput. Soc. 319 327 10.1109/SFCS.1988.21948
M. Seidl R. Könighofer G.P. Fettweis W. Nebel Partial witnesses from preprocessed quantified Boolean formulas Design, Automation & Test in Europe Conference & Exhibition, DATE 2014 2014 1 6 10.7873/DATE.2014.162
S. Sickert J. Esparza et al. H. Hermanns L. Zhang N. Kobayashi et al. An efficient normalisation procedure for linear temporal logic and very weak alternating automata LICS ’20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science 2020 New York ACM 831 844 10.1145/3373718.3394743
A. Stump G. Sutcliffe C. Tinelli S. Demri D. Kapur C. Weidenbach Starexec: a cross-community infrastructure for logic solving Automated Reasoning – 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014 2014 Berlin Springer 367 373 10.1007/978-3-319-08587-6_28
L. Tentrup M.N. Rabe Clausal abstraction for DQBF SAT, Lecture Notes in Computer Science 2019 Berlin Springer 388 405
T. Van Dijk Oink: an implementation and evaluation of modern parity game solvers Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’18) 2018 Berlin Springer 291 308 10.1007/978-3-319-89960-2_16
T. Van Dijk B. Rubbens J. Leroux J. Raskin Simple fixpoint iteration to solve parity games Proceedings Tenth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2019 2019 123 139 10.4204/EPTCS.305.9
T. Van Dijk J. van de Pol Sylvan: multi-core framework for decision diagrams Int. J. Softw. Tools Technol. Transf. 2017 19 6 675 696 10.1007/s10009-016-0433-2
M.Y. Vardi P. Wolper R.A. DeMillo Automata theoretic techniques for modal logics of programs (extended abstract) Proceedings of the 16th Annual ACM Symposium on Theory of Computing 1984 New York ACM 446 456 10.1145/800057.808711
