Top

Formal Methods in System Design

Published in:

14-07-2023

Dissecting ltlsynt

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

Published in: Formal Methods in System Design | Issue 2-3/2022

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

ltlsynt is a tool for synthesizing a reactive circuit satisfying a specification expressed as an LTL formula. 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 ltlsynt: for instance, 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.

previous article Synbit: synthesizing bidirectional programs using unidirectional sketches

next article Church synthesis on register automata over linearly ordered data domains

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Available only for authorised users

This option was not detailed as it was not found to be better than \(X=1\).

An error in this context is either insufficient memory or the acceptance condition needing more than 32 colors, the default number of colors in Spot.

Strategies which cannot be encoded without gates.

Abel A, Reineke J (2015) MeMin: SAT-based exact minimization of incompletely specified Mealy machines. In: Proceedings for the 34th international conference on computer-aided design (ICCAD’15). IEEE Press, pp 94–101, https://doi.org/10.1109/ICCAD.2015.7372555

Babiak T, Badie T, Duret-Lutz A, et al (2013) Compositional approach to suspension and other improvements to LTL translation. In: Proceedings of the 20th international SPIN symposium on model checking of software (SPIN’13), lecture notes in computer science, vol 7976. Springer, pp 81–98, https://doi.org/10.1007/978-3-642-39176-7_6

Babiak T, Blahoudek F, Duret-Lutz A, et al (2015) The Hanoi Omega-Automata Format. In: Proceedings of the 27th conference on computer aided verification (CAV’15), lecture notes in computer science, vol 8172. Springer, pp 442–445, https://doi.org/10.1007/978-3-319-21690-4_31

Biere A (2007) The aiger and-inverter graph (aig) format version 20070427

Brayton R, Mishchenko A (2010) Abc: An academic industrial-strength verification tool. In: Proceedings of the 22nd conference on computer aided verification (CAV’10). Springer, pp 24–40, https://doi.org/10.1007/978-3-642-14295-6_5

Bryant RE (1986) Graph-based algorithms for boolean function manipulation. IEEE Transact Comput 35(8):677–691CrossRef

Casares A, Colcombet T, Fijalkow N (2021) Optimal transformations of games and automata using Muller conditions. In: Bansal N, Merelli E, Worrell J (eds) Proceedings of the 48th International colloquium on automata, languages, and programming (ICALP’21), Leibniz international proceedings in informatics (LIPIcs), vol 198. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, pp 123:1–123:14. https://doi.org/10.4230/LIPIcs.ICALP.2021.123

Casares A, Duret-Lutz A, Meyer KJ, Renkin F, Sickert S (2022) Practical applications of the Alternating Cycle Decomposition. In: Proceedings of the 28th international conference on tools and algorithms for the construction and analysis of systems, lecture notes in computer science, vol 13244, pp. 99–117. https://doi.org/10.1007/978-3-030-99527-0_6

Černá I, Pelánek R (2003) Relating hierarchy of temporal properties to model checking. In: Rovan B, Vojtáǎ P (eds) Proceedings of the 28th international symposium on mathematical foundations of computer science (MFCS’03), lecture notes in computer science, vol 2747. Springer-Verlag, Bratislava, Slovak Republic, pp 318–327

10.

Dax C, Eisinger J, Klaedtke F (2007) Mechanizing the powerset construction for restricted classes of \(\omega \)-automata. In: Namjoshi KS, Yoneda T, Higashino T, et al (eds) Proceedings of the 5th international symposium on automated technology for verification and analysis (ATVA’07), lecture notes in computer science, vol 4762. Springer, https://doi.org/10.1007/978-3-540-75596-8_17

11.

van Dijk T (2018) Oink: An implementation and evaluation of modern parity game solvers. In: Proceedings of the 24th international conference on tools and algorithms for the construction and analysis of systems (TACAS’18), Springer, pp 291–308, https://doi.org/10.1007/978-3-319-89960-2_16

12.

Duret-Lutz A (2014) LTL translation improvements in Spot 1.0. InterJ Crit Comput-Based Syst 5(1/2):31–54. https://doi.org/10.1504/IJCCBS.2014.059594CrossRef

13.

Duret-Lutz A, Renault E, Colange M, et al (2022) From Spot 2.0 to Spot 2.10: What’s new? In: Proceedings of the 34th international conference on computer aided verification (CAV’22), lecture notes in computer science, vol 13372. Springer, pp 174–187, https://doi.org/10.1007/978-3-031-13188-2_9

14.

Emerson EA, Lei CL (1987) Modalities for model checking: branching time logic strikes back. Sci Comput Program 8(3):275–306. https://doi.org/10.1016/0167-6423(87)90036-0MathSciNetCrossRef

15.

Esparza J, Křetínský J, Sickert S (2018) One theorem to rule them all: A unified translation of LTL into \(\omega \)-automata. In: Dawar A, Grädel E (eds) Proceedings of the 33rd annual ACM/IEEE symposium on logic in computer science (LICS’18). ACM, pp 384–393, https://doi.org/10.1145/3209108.3209161

16.

Etessami K, Holzmann GJ (2000) Optimizing Büchi automata. In: Palamidessi C (ed) Proceedings of the 11th international conference on concurrency theory (Concur’00), lecture notes in computer science, vol 1877. Springer-Verlag, Pennsylvania, USA, pp 153–167

17.

Finkbeiner B, Geier G, Passing N (2021) Specification decomposition for reactive synthesis. In: Proceedings for the 13th NASA formal methods symposium (NFM’21), to appear. https://arxiv.org/abs/2103.08459

18.

Jacobs S, Bloem R, Brenguier R et al (2017) The first reactive synthesis competition (syntcomp 2014). Inter J Softw Tools Technol Trans 19(3):367–390CrossRef

19.

Jacobs S, Bloem R, Colange M, et al (2019) The 5th reactive synthesis competition (SYNTCOMP 2018): Benchmarks, participants & results. CoRR abs/1904.07736

20.

Jurdziński M (2000) Small progress measures for solving parity games. In: Proceedings of the 17th symposium on theoretical aspects of computer science (STACS 2000), lecture notes in computer science, vol 1770. Springer-Verlag, pp 290–301

21.

Kupferman O, Rosenberg A (2010) The blowup in translating LTL to deterministic automata. In: Revised Selected and Invited Papers for the 6th international workshop, on model checking and artificial intelligence (MoChArt’10), lecture notes in computer science, vol 6572. Springer, pp 85–94,https://doi.org/10.1007/978-3-642-20674-0_6

22.

Löding C (2001) Efficient minimization of deterministic weak \(\omega \)-automata. Inform Process Lett 79(3):105–109. https://doi.org/10.1016/S0020-0190(00)00183-6ADSMathSciNetCrossRef

23.

Major J, Blahoudek F, Strejcek J, et al (2019) ltl3tela: LTL to small deterministic or nondeterministic Emerson-Lei automata. In: Proceedings of the 17th international symposium on automated technology for verification and analysis (ATVA’19), lecture notes in computer science, vol 11781. Springer, pp 357–365, https://doi.org/10.1007/978-3-030-31784-3_21

24.

Manna Z, Pnueli A (1990) A hierarchy of temporal properties. In: Proceedings of the sixth annual ACM symposium on Principles of distributed computing (PODC’90). ACM, New York, NY, USA, pp 377–410

25.

Minato S (1992) Fast generation of irredundant sum-of-products forms from binary decision diagrams. In: Proceedings of the third Synthesis and Simulation and Meeting International Interchange workshop (SASIMI’92), Kobe, Japan, pp 64–73

26.

Mishchenko A, Chatterjee S, Brayton R (2006) Dag-aware aig rewriting a fresh look at combinational logic synthesis. In: Proceedings of the 43rd annual Design automation conference. association for computing machinery, New York, NY, USA, DAC ’06, p 532-535, https://doi.org/10.1145/1146909.1147048

27.

Müller D, Sickert S (2017) LTL to deterministic Emerson-Lei automata. In: Bouyer P, Orlandini A, Pietro PS (eds) Proceedings of the eighth international symposium on games, automata, logics and formal verification (GandALF’17), pp 180–194, https://doi.org/10.4204/EPTCS.256.13

28.

Pfleeger CP (1973) State reduction in incompletely specified finite-state machines. IEEE Transact Comput C–22(12):1099–1102. https://doi.org/10.1016/j.compeleceng.2006.06.001MathSciNetCrossRef

29.

Redziejowski R (2012) An improved construction of deterministic omega-automaton using derivatives. Fundamenta Inform 119(3–4):393–406. https://doi.org/10.3233/FI-2012-744MathSciNetCrossRef

30.

Renkin F, Duret-Lutz A, Pommellet A (2020) Practical “paritizing” of Emerson-Lei automata. In: Proceedings of the 18th international symposium on automated technology for verification and analysis (ATVA’20), lecture notes in computer science, vol 12302. Springer, pp 127–143. https://doi.org/10.1007/978-3-030-59152-6_7

31.

Renkin F, Schlehuber-Caissier P, Duret-Lutz A, Pommellet A (2022) Effective reductions of Mealy machines. In: Proceedings of the 42nd international conference on formal techniques for distributed objects, components, and systems (FORTE’22). Springer, lecture notes in computer science, vol 13273, pp. 114–130. https://doi.org/10.1007/978-3-031-08679-3_8

32.

Safra S, Vardi MY (1989) On \(\omega \)-automata and temporal logic. In: Proceedings of the twenty-first annual ACM Symposium on theory of computing (STOC’89). ACM, pp 127–137, https://doi.org/10.1145/73007.73019

33.

Zielonka W (1998) Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor Comput Sci 200(1):135–183. https://doi.org/10.1016/S0304-3975(98)00009-7MathSciNetCrossRef

Title: Dissecting ltlsynt
Authors: Florian Renkin
Philipp Schlehuber-Caissier
Alexandre Duret-Lutz
Adrien Pommellet
Publication date: 14-07-2023
Publisher: Springer US
Published in: Formal Methods in System Design / Issue 2-3/2022
Print ISSN: 0925-9856
Electronic ISSN: 1572-8102
DOI: https://doi.org/10.1007/s10703-022-00407-6

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Other articles of this Issue 2-3/2022

Enhancing active model learning with equivalence checking using simulation relations

Preface for the formal methods in system design special issue on SYNT 2021

Synbit: synthesizing bidirectional programs using unidirectional sketches

Church synthesis on register automata over linearly ordered data domains

Symbolic encoding of LL(1) parsing and its applications

Finite-trace and generalized-reactivity specifications in temporal synthesis

Premium Partner