Practical synthesis of reactive systems from LTL specifications via parity games. (English) Zbl 1435.68200
Summary: 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.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B44 | Temporal logic |
| 68Q45 | Formal languages and automata |
| 91A43 | Games involving graphs |
| 91A80 | Applications of game theory |
References:
| [1] | 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). 10.1109/ICCAD.2015.7372555 |
| [2] | Babiak, Tomáš; Blahoudek, František; Duret-Lutz, Alexandre; Klein, Joachim; Křetínský, Jan; Müller, David; Parker, David; Strejček, Jan, The Hanoi Omega-Automata Format, Computer Aided Verification, 479-486 (2015), Cham: Springer International Publishing, Cham |
| [3] | Bloem, R.; Chatterjee, K.; Jobstmann, B.; Clarke, Em; Henzinger, Ta; Veith, H.; Bloem, R., Graph games and reactive synthesis, Handbook of Model Checking, 921-962 (2018), Berlin: Springer, Berlin · Zbl 1392.68233 |
| [4] | Bloem, Roderick; Jacobs, Swen; Khalimov, Ayrat, Parameterized Synthesis Case Study: AMBA AHB, Electronic Proceedings in Theoretical Computer Science, 157, 68-83 (2014) · doi:10.4204/EPTCS.157.9 |
| [5] | Bohy, Aaron; Bruyère, Véronique; Filiot, Emmanuel; Jin, Naiyong; Raskin, Jean-François, Acacia+, a Tool for LTL Synthesis, Computer Aided Verification, 652-657 (2012), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg |
| [6] | Brayton, Robert; Mishchenko, Alan, ABC: An Academic Industrial-Strength Verification Tool, Computer Aided Verification, 24-40 (2010), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg |
| [7] | Cavada, Roberto; Cimatti, Alessandro; Dorigatti, Michele; Griggio, Alberto; Mariotti, Alessandro; Micheli, Andrea; Mover, Sergio; Roveri, Marco; Tonetta, Stefano, The nuXmv Symbolic Model Checker, Computer Aided Verification, 334-342 (2014), Cham: Springer International Publishing, Cham |
| [8] | Duret-Lutz, Alexandre; Lewkowicz, Alexandre; Fauchille, Amaury; Michaud, Thibaud; Renault, Étienne; Xu, Laurent, Spot 2.0 — A Framework for LTL and \[\omega \] -Automata Manipulation, Automated Technology for Verification and Analysis, 122-129 (2016), Cham: Springer International Publishing, Cham |
| [9] | Ehlers, Rüdiger, Unbeast: Symbolic Bounded Synthesis, Tools and Algorithms for the Construction and Analysis of Systems, 272-275 (2011), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1316.68073 |
| [10] | Ehlers, R., Symbolic bounded synthesis, Form. Methods Syst. Des., 40, 2, 232-262 (2012) · Zbl 1247.68163 · doi:10.1007/s10703-011-0137-x |
| [11] | Ehlers, Rüdiger; Adabala, Keerthi, Reactive Synthesis of Graphical User Interface Glue Code, Automated Technology for Verification and Analysis, 387-403 (2019), Cham: Springer International Publishing, Cham |
| [12] | Esparza, Javier; Křetínský, Jan; Raskin, Jean-François; Sickert, Salomon, From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata, Tools and Algorithms for the Construction and Analysis of Systems, 426-442 (2017), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1452.68105 |
| [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). 10.1145/3209108.3209161 · Zbl 1497.68259 |
| [14] | Faymonville, Peter; Finkbeiner, Bernd; Tentrup, Leander, BoSy: An Experimentation Framework for Bounded Synthesis, Computer Aided Verification, 325-332 (2017), Cham: Springer International Publishing, Cham |
| [15] | Filiot, E.; Jin, N.; Raskin, J., Antichains and compositional algorithms for LTL synthesis, Form. Methods Syst. Des., 39, 3, 261-296 (2011) · Zbl 1258.03046 · doi:10.1007/s10703-011-0115-3 |
| [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). 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) · Zbl 1246.91025 · doi:10.1142/S0129054112400333 |
| [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, Carsten; Klein, Felix; Finkbeiner, Bernd, Bounded Synthesis of Reactive Programs, Automated Technology for Verification and Analysis, 441-457 (2018), Cham: Springer International Publishing, Cham · Zbl 1517.68236 |
| [20] | Giannakopoulou, Dimitra; Lerda, Flavio, From States to Transitions: Improving Translation of LTL Formulae to Büchi Automata, Formal Techniques for Networked and Distributed Sytems — FORTE 2002, 308-326 (2002), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1037.68553 |
| [21] | Godhal, Y.; Chatterjee, K.; Henzinger, Ta, Synthesis of AMBA AHB from formal specification: a case study, STTT (Int. J. Softw. Tools. Technol. Trans.), 15, 5-6, 585-601 (2013) · doi:10.1007/s10009-011-0207-9 |
| [22] | Grädel, Erich; Thomas, Wolfgang; Wilke, Thomas, Automata Logics, and Infinite Games (2002), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1011.00037 |
| [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, Ayrat; Jacobs, Swen; Bloem, Roderick, PARTY Parameterized Synthesis of Token Rings, Computer Aided Verification, 928-933 (2013), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1426.68051 |
| [28] | Křetínský, Jan; Meggendorfer, Tobias; Sickert, Salomon, Owl: A Library for \[\omega \]-Words, Automata, and LTL, Automated Technology for Verification and Analysis, 543-550 (2018), Cham: Springer International Publishing, Cham · Zbl 1517.68203 |
| [29] | Kupferman, Orna, Recent Challenges and Ideas in Temporal Synthesis, SOFSEM 2012: Theory and Practice of Computer Science, 88-98 (2012), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg |
| [30] | Kupferman, Orna; Piterman, Nir; Vardi, Moshe Y., Safraless Compositional Synthesis, Computer Aided Verification, 31-44 (2006), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1188.68193 |
| [31] | Luttenberger, M.: Strategy iteration using non-deterministic strategies for solving parity games (2008). arxiv:0806.2923 |
| [32] | Meyer, Philipp J.; Luttenberger, Michael, Solving Mean-Payoff Games on the GPU, Automated Technology for Verification and Analysis, 262-267 (2016), Cham: Springer International Publishing, Cham |
| [33] | Meyer, Philipp J.; Sickert, Salomon; Luttenberger, Michael, Strix: Explicit Reactive Synthesis Strikes Back!, Computer Aided Verification, 578-586 (2018), Cham: Springer International Publishing, Cham |
| [34] | Morgenstern, Andreas; Schneider, Klaus, Exploiting the Temporal Logic Hierarchy and the Non-Confluence Property for Efficient LTL Synthesis, Electronic Proceedings in Theoretical Computer Science, 25, 89-102 (2010) · Zbl 1456.68099 · doi:10.4204/EPTCS.25.11 |
| [35] | Müller, David; Sickert, Salomon, LTL to Deterministic Emerson-Lei Automata, Electronic Proceedings in Theoretical Computer Science, 256, 180-194 (2017) · Zbl 1483.68177 · doi:10.4204/EPTCS.256.13 |
| [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). 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). 10.1145/75277.75293 · Zbl 0686.68015 |
| [38] | Sickert, Salomon; Esparza, Javier; Jaax, Stefan; Křetínský, Jan, Limit-Deterministic Büchi Automata for Linear Temporal Logic, Computer Aided Verification, 312-332 (2016), Cham: Springer International Publishing, Cham · Zbl 1411.68054 |
| [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) · doi:10.1007/s10009-012-0224-3 |
| [40] | Somenzi, F.: CUDD: CU decision diagram package release 3.0.0 (2015) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
