×

A symbolic algorithm for lazy synthesis of eager strategies. (English) Zbl 1435.68198

Summary: We present an algorithm for solving two-player safety games that combines a mixed forward/backward search strategy with a symbolic representation of the state space. By combining forward and backward exploration, our algorithm can synthesize strategies that are eager in the sense that they try to prevent progress towards the error states as soon as possible, whereas standard backwards algorithms often produce permissive solutions that only react when absolutely necessary. We provide experimental results for two classes of crafted benchmarks, the benchmark set of the Reactive Synthesis Competition (SYNTCOMP) 2017, as well as a set of randomly generated benchmarks. The results show that our algorithm in many cases produces more eager strategies than a standard backwards algorithm, and solves a number of benchmarks that are intractable for existing tools. Finally, we observe a connection between our algorithm and a recently proposed algorithm for the synthesis of controllers that are robust against disturbances, pointing to possible future applications.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
91A80 Applications of game theory
94C11 Switching theory, applications of Boolean algebras to circuits and networks

Software:

CUDD
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Beyene, T.A., Chaudhuri, S., Popeea, C., Rybalchenko, A.: A constraint-based approach to solving games on infinite graphs. In: Jagannathan, S., Sewell, P. (eds.) POPL, pp. 221-234. ACM (2014). 10.1145/2535838.2535860 · Zbl 1284.91009
[2] Bloem, R., Könighofer, R., Seidl, M.: SAT-based synthesis methods for safety specs. In: VMCAI, LNCS, vol. 8318, pp. 1-20. Springer, Berlin (2014) · Zbl 1428.68040
[3] Brenguier, R.; Pérez, Ga; Raskin, J.; Sankur, O., AbsSynthe: abstract synthesis from succinct safety specifications, SYNT, EPTCS, 157, 100-116 (2014) · doi:10.4204/EPTCS.157.11
[4] Büchi, J.; Landweber, L., Solving sequential conditions by finite-state strategies, Trans. Am. Math. Soc., 138, 295-311 (1969) · Zbl 0182.02302 · doi:10.2307/1994916
[5] Cassez, Franck; David, Alexandre; Fleury, Emmanuel; Larsen, Kim G.; Lime, Didier, Efficient On-the-Fly Algorithms for the Analysis of Timed Games, Lecture Notes in Computer Science, 66-80 (2005), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1134.68382
[6] Church, A.: Applications of recursive arithmetic to the problem of circuit synthesis. Summaries of the Summer Institute of Symbolic Logic I, pp. 3-50 (1957) · Zbl 0206.47902
[7] Clarke, J.B.E., Long, D.: Representing circuits more efficiently in symbolic model checking. In: 28th ACM/IEEE Design Automation Conference, pp. 403-407 (1991)
[8] Coudert, Olivier; Berthet, Christian; Madre, Jean Christophe, Verification of synchronous sequential machines based on symbolic execution, Automatic Verification Methods for Finite State Systems, 365-373 (1990), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg
[9] Dallal, E., Neider, D., Tabuada, P.: Synthesis of safety controllers robust to unmodeled intermittent disturbances. In: CDC, pp. 7425-7430. IEEE (2016). 10.1109/CDC.2016.7799416
[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., Topcu, U.: Resilience to intermittent assumption violations in reactive synthesis. In: HSCC, pp. 203-212. ACM (2014). 10.1145/2562059.2562128 · Zbl 1361.68146
[12] Filiot, E.; Jin, N.; Raskin, Jf, 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
[13] Finkbeiner, Bernd; Jacobs, Swen, Lazy Synthesis, Lecture Notes in Computer Science, 219-234 (2012), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1326.68183
[14] Finkbeiner, B.; Schewe, S., Bounded synthesis, STTT, 15, 5-6, 519-539 (2013) · doi:10.1007/s10009-012-0228-z
[15] Huang, C.; Peled, Da; Schewe, S.; Wang, F., A game-theoretic foundation for the maximum software resilience against dense errors, IEEE Trans. Softw. Eng., 42, 7, 605-622 (2016) · doi:10.1109/TSE.2015.2510001
[16] Jacobs, Swen; Basset, Nicolas; Bloem, Roderick; Brenguier, Romain; Colange, Maximilien; Faymonville, Peter; Finkbeiner, Bernd; Khalimov, Ayrat; Klein, Felix; Michaud, Thibaud; Pérez, Guillermo A.; Raskin, Jean-François; Sankur, Ocan; Tentrup, Leander, The 4th Reactive Synthesis Competition (SYNTCOMP 2017): Benchmarks, Participants & Results, Electronic Proceedings in Theoretical Computer Science, 260, 116-143 (2017) · doi:10.4204/EPTCS.260.10
[17] Jacobs, S.; Bloem, R.; Brenguier, R.; Ehlers, R.; Hell, T.; Könighofer, R.; Pérez, Ga; Raskin, J.; Ryzhyk, L.; Sankur, O.; Seidl, M.; Tentrup, L.; Walker, A., The first reactive synthesis competition (SYNTCOMP 2014), STTT, 19, 3, 367-390 (2017) · doi:10.1007/s10009-016-0416-3
[18] Jacobs, Swen; Sakr, Mouhammad, A Symbolic Algorithm for Lazy Synthesis of Eager Strategies, Automated Technology for Verification and Analysis, 211-227 (2018), Cham: Springer International Publishing, Cham · Zbl 1435.68198
[19] Kropf, T., Introduction to Formal Hardware Verification (2013), Berlin: Springer, Berlin · Zbl 0931.68018
[20] Legg, Alexander; Narodytska, Nina; Ryzhyk, Leonid, A SAT-Based Counterexample Guided Method for Unbounded Synthesis, Computer Aided Verification, 364-382 (2016), Cham: Springer International Publishing, Cham
[21] Liu, Xinxin; Smolka, Scott A., Simple linear-time algorithms for minimal fixed points, Automata, Languages and Programming, 53-66 (1998), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg
[22] Neider, Daniel; Topcu, Ufuk, An Automaton Learning Approach to Solving Safety Games over Infinite Graphs, Tools and Algorithms for the Construction and Analysis of Systems, 204-221 (2016), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1420.68109
[23] Neider, D., Weinert, A., Zimmermann, M.: Synthesizing optimally resilient controllers. In: CSL, LIPIcs, vol. 119, pp. 34:1-34:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2018). 10.4230/LIPIcs.CSL.2018.34 · Zbl 1528.68085
[24] Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179-190. ACM Press (1989). 10.1145/75277.75293 · Zbl 0686.68015
[25] Raman, V., Donzé, A., Sadigh, D., Murray, R.M., Seshia, S.A.: Reactive synthesis from signal temporal logic specifications. In: HSCC, pp. 239-248. ACM (2015). 10.1145/2728606.2728628 · Zbl 1366.68180
[26] Sohail, S.; Somenzi, F., Safety first: a two-stage algorithm for the synthesis of reactive systems, STTT, 15, 5-6, 433-454 (2013) · doi:10.1007/s10009-012-0224-3
[27] Somenzi, F.: CUDD: CU decision diagram package, release 2.4.0. University of Colorado at Boulder (2009)
[28] Touati, H.J., Savoj, H., Lin, B., Brayton, R.K., Sangiovanni-Vincentelli, A.: Implicit state enumeration of finite state machines using bdd’s. In: Computer-Aided Design, 1990. ICCAD-90. 1990 IEEE International Conference on Digest of Technical Papers, pp. 130-133. IEEE (1990)
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.