[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

Dissecting ltlsynt

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13
Fig. 14
Fig. 15
Fig. 16
Fig. 17
Fig. 18
Fig. 19
Fig. 20
Fig. 21
Fig. 22
Fig. 23
Fig. 24
Fig. 25
Fig. 26
Fig. 27
Fig. 28

Similar content being viewed by others

Data availability

Instructions to reproduce the benchmarks presented in this article are available from https://www.lrde.epita.fr/~frenkin/fmsd22/artifact

Notes

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

  2. 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.

  3. Strategies which cannot be encoded without gates.

References

  1. 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

  2. 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

  3. 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

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

  5. 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

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

    Article  Google Scholar 

  7. 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

  8. 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

  9. Č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.059594

    Article  Google Scholar 

  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-0

    Article  MathSciNet  Google Scholar 

  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–390

    Article  Google Scholar 

  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-6

    Article  ADS  MathSciNet  Google Scholar 

  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.001

    Article  MathSciNet  Google Scholar 

  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-744

    Article  MathSciNet  Google Scholar 

  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-7

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. EPITA Research Laboratory, EPITA, 14–16 rue Voltaire, 94270, Kremlin-Bicêtre, France

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

Authors
  1. Florian Renkin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Philipp Schlehuber-Caissier
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alexandre Duret-Lutz
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Adrien Pommellet
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Florian Renkin.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Appendix A

Appendix A

1.1 A Explanation of restrictions of the direct construction

In this appendix, we explain why some restrictions have to be applied to the sub-formulas. Note that these restrictions sometimes allow us to create a direct strategy, but as our procedure is based on syntactical analysis, we may not be able to find all such cases.

Fig. 29
figure 29

Building a wrong direct strategy for the formula \(\textsf{G}((i \wedge \bar{o}) \vee \bar{i}) \leftrightarrow \textsf{G}\textsf{F}(o)\)

Full size image

1.2 Why we don’t have an output in \(\phi _1\)

Consider the formula \(\textsf{G}((i \wedge \bar{o}) \vee \bar{i}) \leftrightarrow \textsf{G}\textsf{F}(\bar{o})\). A possible corresponding Büchi automaton is shown in Fig. 29. Our procedure would assign \(\bar{o}\) to the edge that goes from 1 to 0 and result in an automaton where the states have no outgoing edge labeled by i. Thus, it is not an actual strategy.

Fig. 30
figure 30

Building a wrong direct strategy for the formula \((\textsf{G}\textsf{F}(i) \wedge \textsf{G}\textsf{F}(\bar{i})) \leftrightarrow \textsf{G}\textsf{F}(\bar{i} \wedge o)\)

Full size image

1.3 Why \(b_2\) and \(\lnot b_2\) must be realizable

We now explain why \(b_2\) and its negation have to be realizable. Let us consider an example where \(b_2\) is unrealizable (without loss of generality thanks to symmetry): the formula \(\textsf{G}\textsf{F}(i) \leftrightarrow \textsf{G}\textsf{F}(\bar{i} \wedge o)\) where o is an output proposition.

The translation of \(\textsf{G}\textsf{F}(i)\) results in a Büchi automaton with two states shown in Fig. 30a. The procedure will assign \(\bar{i} \wedge o\) to the edges colored with \(\textcircled {0}\) and the condition associated to these edges is now \(\bot \); these edges are therefore removed. We end up with a “strategy” described in Fig. 30b featuring two states labeled with \(\bar{i} \wedge \bar{o}\); it is not input-complete, thus it is not an actual strategy.

Rights and permissions

Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Renkin, F., Schlehuber-Caissier, P., Duret-Lutz, A. et al. Dissecting ltlsynt. Form Methods Syst Des 61, 248–289 (2022). https://doi.org/10.1007/s10703-022-00407-6

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-022-00407-6

Keywords

Search

Navigation