nach oben

Acta Informatica

Erschienen in:

21.11.2019 | Original Article

Practical synthesis of reactive systems from LTL specifications via parity games

You can teach an old dog new tricks: making a classic approach structured, forward-explorative, and incremental

verfasst von: Michael Luttenberger, Philipp J. Meyer, Salomon Sickert

Erschienen in: Acta Informatica | Ausgabe 1-2/2020

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

The synthesis of reactive systems from linear temporal logic (LTL) specifications is an important aspect in the design of reliable software and hardware. We present our adaption of the classic automata-theoretic approach to LTL synthesis, implemented in the tool Strix which has won the two last synthesis competitions (Syntcomp2018/2019). The presented approach is (1) structured, meaning that the states used in the construction have a semantic structure that is exploited in several ways, it performs a (2) forward exploration such that it often constructs only a small subset of the reachable states, and it is (3) incremental in the sense that it reuses results from previous inconclusive solution attempts. Further, we present and study different guiding heuristics that determine where to expand the on-demand constructed arena. Moreover, we show several techniques for extracting an implementation (Mealy machine or circuit) from the witness of the tree-automaton emptiness check. Lastly, the chosen constructions use a symbolic representation of the transition functions to reduce runtime and memory consumption. We evaluate the proposed techniques on the Syntcomp2019 benchmark set and show in more detail how the proposed techniques compare to the techniques implemented in other leading LTL synthesis tools.

Vorheriger Artikel Preface for the SYNT

Nächster Artikel Performance heuristics for GR(1) synthesis and related algorithms

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

See [3] for an introduction to reactive synthesis and related graph games.

https://strix.model.in.tum.de/.

We will later see the advantage of using nondeterministic strategies (multiple actions allowed) compared to deterministic strategies (only one action allowed).

We represent the intermediate states simply by circular shaped nodes in the figures.

Should \({{\mathcal {O}}}_{\delta }\) determine that all automata will accept any possible input–output pairs from now on, it simplifies the successor state to \(\top \) which, again by construction, is always won by

https://static-content.springer.com/image/art%3A10.1007%2Fs00236-019-00349-3/MediaObjects/236_2019_349_IEq293_HTML.gif

Actually, the edges are also labeled by corresponding inputs and outputs coming from the environment and the controller, respectively.

http://www.syntcomp.org/.

Strix was ranked on the first place.

...or \(|\log _{10} \frac{x + 1}{y + 1}|\) to compensate for circuits of size 0.

Abel, A., Reineke, J.: MeMin: SAT-based exact minimization of incompletely specified Mealy machines. In: Proceedings of the IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2015, Austin, TX, USA, November 2–6, 2015, pp. 94–101 (2015). https://doi.org/10.1109/ICCAD.2015.7372555

Babiak, T., Blahoudek, F., Duret-Lutz, A., Klein, J., Kretínský, J., Müller, D., Parker, D., Strejcek, J.: The Hanoi omega-automata format. In: Computer Aided Verification—27th International Conference, CAV 2015, San Francisco, CA, USA, July 18–24, 2015, Proceedings, Part I, pp. 479–486 (2015). https://doi.org/10.1007/978-3-319-21690-4_31 CrossRef

Bloem, R., Chatterjee, K., Jobstmann, B.: Graph games and reactive synthesis. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 921–962. Springer, Berlin (2018). https://doi.org/10.1007/978-3-319-10575-8_27 CrossRef

Bloem, R., Jacobs, S., Khalimov, A.: Parameterized synthesis case study: AMBA AHB. In: Proceedings 3rd Workshop on Synthesis, SYNT 2014, Vienna, Austria, July 23–24, 2014., pp. 68–83 (2014). https://doi.org/10.4204/EPTCS.157.9 MathSciNetCrossRef

Bohy, A., Bruyère, V., Filiot, E., Jin, N., Raskin, J.: Acacia+, a tool for LTL synthesis. In: Computer Aided Verification—24th International Conference, CAV 2012, Berkeley, CA, USA, July 7–13, 2012 Proceedings, pp. 652–657 (2012). https://doi.org/10.1007/978-3-642-31424-7_45 CrossRef

Brayton, R.K., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, pp. 24–40 (2010). https://doi.org/10.1007/978-3-642-14295-6_5 CrossRef

Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Computer Aided Verification—26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18–22, 2014. Proceedings, pp. 334–342 (2014). https://doi.org/10.1007/978-3-319-08867-9_22 CrossRef

Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0—a framework for LTL and \(\omega \)-automata manipulation. In: Automated Technology for Verification and Analysis—14th International Symposium, ATVA 2016, Chiba, Japan, October 17–20, 2016, Proceedings, pp. 122–129 (2016). https://doi.org/10.1007/978-3-319-46520-3_8 CrossRef

Ehlers, R.: Unbeast: symbolic bounded synthesis. In: Tools and Algorithms for the Construction and Analysis of Systems—17th International Conference, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings, pp. 272–275 (2011). https://doi.org/10.1007/978-3-642-19835-9_25 CrossRef

10.

Ehlers, R.: Symbolic bounded synthesis. Form. Methods Syst. Des. 40(2), 232–262 (2012). https://doi.org/10.1007/s10703-011-0137-x CrossRefMATH

11.

Ehlers, R., Adabala, K.: Reactive synthesis of graphical user interface glue code. In: Y. Chen, C. Cheng, J. Esparza (eds.) Automated Technology for Verification and Analysis—17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28–31, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11781, pp. 387–403. Springer (2019). https://doi.org/10.1007/978-3-030-31784-3_23 CrossRef

12.

Esparza, J., Kretínský, J., Raskin, J., Sickert, S.: From LTL and limit-deterministic Büchi automata to deterministic parity automata. In: Tools and Algorithms for the Construction and Analysis of Systems—23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings, Part I, pp. 426–442 (2017). https://doi.org/10.1007/978-3-662-54577-5_25 CrossRef

13.

Esparza, J., Kretínský, J., Sickert, S.: One theorem to rule them all: A unified translation of LTL into \(\omega \)-automata. In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09–12, 2018, pp. 384–393 (2018). https://doi.org/10.1145/3209108.3209161

14.

Faymonville, P., Finkbeiner, B., Tentrup, L.: BoSy: An experimentation framework for bounded synthesis. In: Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II, pp. 325–332 (2017). https://doi.org/10.1007/978-3-319-63390-9_17 CrossRef

15.

Filiot, E., Jin, N., Raskin, J.: Antichains and compositional algorithms for LTL synthesis. Form. Methods Syst. Des. 39(3), 261–296 (2011). https://doi.org/10.1007/s10703-011-0115-3 CrossRefMATH

16.

Finkbeiner, B., Klein, F., Piskac, R., Santolucito, M.: Synthesizing functional reactive programs. In: Eisenberg, R.A. (ed.) Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell, Haskell@ICFP 2019, Berlin, Germany, August 18–23, 2019, pp. 162–175. ACM (2019). https://doi.org/10.1145/3331545.3342601

17.

Friedmann, O., Lange, M.: Two local strategy iteration schemes for parity game solving. Int. J. Found. Comput. Sci. 23(3), 669–685 (2012). https://doi.org/10.1142/S0129054112400333 MathSciNetCrossRefMATH

18.

Geier, G., Heim, P., Klein, F., Finkbeiner, B.: Synthroids: Synthesizing a game for fpgas using temporal logic specifications. In: FMCAD, pp. 1–5. IEEE (2019)

19.

Gerstacker, C., Klein, F., Finkbeiner, B.: Bounded synthesis of reactive programs. In: Automated Technology for Verification and Analysis—16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7–10, 2018, Proceedings, pp. 441–457 (2018). https://doi.org/10.1007/978-3-030-01090-4_26 CrossRef

20.

Giannakopoulou, D., Lerda, F.: From states to transitions: Improving translation of LTL formulae to Büchi automata. In: Formal Techniques for Networked and Distributed Systems—FORTE 2002, 22nd IFIP WG 6.1 International Conference Houston, Texas, USA, November 11–14, 2002, Proceedings, pp. 308–326 (2002). https://doi.org/10.1007/3-540-36135-9_20 CrossRef

21.

Godhal, Y., Chatterjee, K., Henzinger, T.A.: Synthesis of AMBA AHB from formal specification: a case study. STTT (Int. J. Softw. Tools. Technol. Trans.) 15(5–6), 585–601 (2013). https://doi.org/10.1007/s10009-011-0207-9 CrossRef

22.

Grädel, E., Thomas, W., Wilke, T.: Automata, Logics, and Infinite Games: A Guide to Current Research, Lecture Notes in Computer Science, vol. 2500. Springer (2002). https://doi.org/10.1007/3-540-36387-4 MATH

23.

Jacobs, S., Basset, N., Bloem, R., Brenguier, R., Colange, M., Faymonville, P., Finkbeiner, B., Khalimov, A., Klein, F., Michaud, T., Pérez, G.A., Raskin, J., Sankur, O., Tentrup, L.: The 4th reactive synthesis competition (SYNTCOMP 2017): Benchmarks, participants & results (2017). arxiv:1711.11439

24.

Jacobs, S., Bloem, R., Brenguier, R., Khalimov, A., Klein, F., Könighofer, R., Kreber, J., Legg, A., Narodytska, N., Pérez, G.A., Raskin, J., Ryzhyk, L., Sankur, O., Seidl, M., Tentrup, L., Walker, A.: The 3rd reactive synthesis competition (SYNTCOMP 2016): Benchmarks, participants & results (2016). arxiv:1609.00507

25.

Jacobs, S., Bloem, R., Colange, M., Faymonville, P., Finkbeiner, B., Khalimov, A., Klein, F., Luttenberger, M., Meyer, P.J., Michaud, T., Sakr, M., Sickert, S., Tentrup, L., Walker, A.: The 5th reactive synthesis competition (SYNTCOMP 2018): Benchmarks, participants & results (2019). arxiv:1904.07736

26.

Jobstmann, B.: Applications and optimizations for LTL synthesis. Ph.D. thesis, Graz University of Technology (2007)

27.

Khalimov, A., Jacobs, S., Bloem, R.: PARTY parameterized synthesis of token rings. In: Computer Aided Verification—25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13–19, 2013. Proceedings, pp. 928–933 (2013). https://doi.org/10.1007/978-3-642-39799-8_66 CrossRef

28.

Kretínský, J., Meggendorfer, T., Sickert, S.: Owl: A library for \(\omega \)-words, automata, and LTL. In: Automated Technology for Verification and Analysis—16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7–10, 2018, Proceedings, pp. 543–550 (2018). https://doi.org/10.1007/978-3-030-01090-4_34 CrossRef

29.

Kupferman, O.: Recent challenges and ideas in temporal synthesis. In: SOFSEM 2012: Theory and Practice of Computer Science - 38th Conference on Current Trends in Theory and Practice of Computer Science, Špindlerův Mlýn, Czech Republic, January 21–27, 2012. Proceedings, pp. 88–98 (2012). https://doi.org/10.1007/978-3-642-27660-6_8 CrossRef

30.

Kupferman, O., Piterman, N., Vardi, M.Y.: Safraless compositional synthesis. In: Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17–20, 2006, Proceedings, pp. 31–44 (2006). https://doi.org/10.1007/11817963_6 CrossRef

31.

Luttenberger, M.: Strategy iteration using non-deterministic strategies for solving parity games (2008). arxiv:0806.2923

32.

Meyer, P.J., Luttenberger, M.: Solving mean-payoff games on the GPU. In: Automated Technology for Verification and Analysis—14th International Symposium, ATVA 2016, Chiba, Japan, October 17–20, 2016, Proceedings, pp. 262–267 (2016). https://doi.org/10.1007/978-3-319-46520-3_17 CrossRef

33.

Meyer, P.J., Sickert, S., Luttenberger, M.: Strix: Explicit reactive synthesis strikes back! In: Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14–17, 2018, Proceedings, Part I, pp. 578–586 (2018). https://doi.org/10.1007/978-3-319-96145-3_31 CrossRef

34.

Morgenstern, A., Schneider, K.: Exploiting the temporal logic hierarchy and the non-confluence property for efficient LTL synthesis. In: Proceedings First Symposium on Games, Automata, Logic, and Formal Verification, GANDALF 2010, Minori (Amalfi Coast), Italy, 17–18th June 2010., pp. 89–102 (2010). https://doi.org/10.4204/EPTCS.25.11 CrossRef

35.

Müller, D., Sickert, S.: LTL to deterministic Emerson-Lei automata. In: Proceedings Eighth International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2017, Roma, Italy, 20–22 September 2017., pp. 180–194 (2017). https://doi.org/10.4204/EPTCS.256.13 MathSciNetCrossRef

36.

Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October–1 November 1977, pp. 46–57 (1977). https://doi.org/10.1109/SFCS.1977.32

37.

Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’89, pp. 179–190. ACM, New York, NY, USA (1989). https://doi.org/10.1145/75277.75293

38.

Sickert, S., Esparza, J., Jaax, S., Kretínský, J.: Limit-deterministic Büchi automata for linear temporal logic. In: Computer Aided Verification—28th International Conference, CAV 2016, Toronto, ON, Canada, July 17–23, 2016, Proceedings, Part II, pp. 312–332 (2016). https://doi.org/10.1007/978-3-319-41540-6_17 CrossRef

39.

Sohail, S., Somenzi, F.: Safety first: a two-stage algorithm for the synthesis of reactive systems. STTT (Int. J. Softw. Tools Technol. Trans.) 15(5–6), 433–454 (2013). https://doi.org/10.1007/s10009-012-0224-3 CrossRef

40.

Somenzi, F.: CUDD: CU decision diagram package release 3.0.0 (2015)

Titel: Practical synthesis of reactive systems from LTL specifications via parity games
You can teach an old dog new tricks: making a classic approach structured, forward-explorative, and incremental
verfasst von: Michael Luttenberger
Philipp J. Meyer
Salomon Sickert
Publikationsdatum: 21.11.2019
Verlag: Springer Berlin Heidelberg
Erschienen in: Acta Informatica / Ausgabe 1-2/2020
Print ISSN: 0001-5903
Elektronische ISSN: 1432-0525
DOI: https://doi.org/10.1007/s00236-019-00349-3

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 1-2/2020

Parameterized synthesis of self-stabilizing protocols in symmetric networks

Reactive synthesis with maximum realizability of linear temporal logic specifications

Synthesis from hyperproperties

Preface for the SYNT

A symbolic algorithm for lazy synthesis of eager strategies

Performance heuristics for GR(1) synthesis and related algorithms