×

zbMATH — the first resource for mathematics

Encodings of bounded synthesis. (English) Zbl 1452.68118
Legay, Axel (ed.) et al., 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. Berlin: Springer. Lect. Notes Comput. Sci. 10205, 354-370 (2017).
Summary: The reactive synthesis problem is to compute a system satisfying a given specification in temporal logic. Bounded synthesis is the approach to bound the maximum size of the system that we accept as a solution to the reactive synthesis problem. As a result, bounded synthesis is decidable whenever the corresponding verification problem is decidable, and can be applied in settings where classic synthesis fails, such as in the synthesis of distributed systems. In this paper, we study the constraint solving problem behind bounded synthesis. We consider different reductions of the bounded synthesis problem of linear-time temporal logic (LTL) to constraint systems given as Boolean formulas (SAT), quantified Boolean formulas (QBF), and dependency quantified Boolean formulas (DQBF). The reductions represent different trade-offs between conciseness and algorithmic efficiency. In the SAT encoding, both inputs and states of the system are represented explicitly; in QBF, inputs are symbolic and states are explicit; in DQBF, both inputs and states are symbolic. We evaluate the encodings systematically using benchmarks from the reactive synthesis competition (SYNTCOMP) and state-of-the-art solvers. Our key, and perhaps surprising, empirical finding is that QBF clearly dominates both SAT and DQBF.
For the entire collection see [Zbl 1360.68015].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic
Software:
ABC; Acacia+; Bloqqer; CAQE
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Babiak, T., Křetínský, M., Řehák, V., Strejček, J.: LTL to Büchi automata translation: fast and more deterministic. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 95-109. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28756-5_8 · Zbl 1352.68142
[2] Biere, A., Lonsing, F., Seidl, M.: Blocked clause elimination for QBF. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 101-115. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22438-6_10 · Zbl 1341.68181
[3] Bloem, R., Galler, S.J., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Interactive presentation: automatic hardware synthesis from specifications: a case study. In: Proceedings of DATE, pp. 1188-1193. EDA Consortium, San Jose, CA, USA (2007)
[4] Bloem, R., Könighofer, R., Seidl, M.: SAT-based synthesis methods for safety specs. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 1-20. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54013-4_1 · Zbl 1428.68040
[5] Bohy, A., Bruyère, V., Filiot, E., Jin, N., Raskin, J.-F.: Acacia+, a tool for LTL synthesis. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 652-657. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31424-7_45
[6] Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24-40. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14295-6_5
[7] Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Santuari, A., Sebastiani, R.: To ackermann-ize or not to ackermann-ize? on efficiently handling uninterpreted function symbols in \(\mathit{SMT}(\cal{EUF} \cup \cal{T})\). In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 557-571. Springer, Heidelberg (2006). doi:10.1007/11916277_38 · Zbl 1165.68482
[8] Büchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Trans. Am. Math. Soc. 138, 295-311 (1969). http://www.jstor.org/stable/1994916 · Zbl 0182.02302
[9] Ehlers, R.: Unbeast: symbolic bounded synthesis. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 272-275. Springer, Heidelberg (2011). doi:10.1007/978-3-642-19835-9_25 · Zbl 1316.68073
[10] Finkbeiner, B.: Bounded synthesis for petri games. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Correct System Design. LNCS, vol. 9360, pp. 223-237. Springer, Heidelberg (2015). doi:10.1007/978-3-319-23506-6_15 · Zbl 1443.68110
[11] Finkbeiner, B., Jacobs, S.: Lazy synthesis. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 219-234. Springer, Heidelberg (2012). doi:10.1007/978-3-642-27940-9_15 · Zbl 1326.68183
[12] Finkbeiner, B., Klein, F.: Bounded cycle synthesis. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 118-135. Springer, Heidelberg (2016). doi:10.1007/978-3-319-41528-4_7 · Zbl 1411.68066
[13] Finkbeiner, B., Schewe, S.: SMT-based synthesis of distributed systems. In: Proceedings of AFM (2007) · Zbl 1196.68142
[14] Finkbeiner, B., Schewe, S.: Bounded synthesis. STTT 15(5-6), 519-539 (2013) · Zbl 1141.68491
[15] Finkbeiner, B., Tentrup, L.: Detecting unrealizable specifications of distributed systems. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 78-92. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54862-8_6
[16] Fröhlich, A., Kovásznai, G., Biere, A., Veith, H.: iDQ: Instantiation-based DQBF solving. In: Proceedings of POS@SAT. EPiC Series in Computing, vol. 27, pp. 103-116. EasyChair (2014)
[17] 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 and results. In: Proceedings Fifth Workshop on Synthesis, SYNT@CAV 2016, Toronto, Canada, 17-18 July, 2016. EPTCS, vol. 229, pp. 149-177 (2016)
[18] Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.M.: Solving QBF with counterexample guided refinement. Artif. Intell. 234, 1-25 (2016) · Zbl 1351.68254
[19] Jobstmann, B., Galler, S., Weiglhofer, M., Bloem, R.: Anzu: a tool for property synthesis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 258-262. Springer, Heidelberg (2007). doi:10.1007/978-3-540-73368-3_29
[20] Khalimov, A., Jacobs, S., Bloem, R.: PARTY parameterized synthesis of token rings. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 928-933. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_66 · Zbl 1426.68051
[21] Khalimov, A., Jacobs, S., Bloem, R.: Towards efficient parameterized synthesis. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 108-127. Springer, Heidelberg (2013). doi:10.1007/978-3-642-35873-9_9 · Zbl 1426.68051
[22] Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Proceedings of FOCS, pp. 531-542. IEEE Computer Society (2005)
[23] Rabe, M.N., Seshia, S.A.: Incremental determinization. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 375-392. Springer, Heidelberg (2016). doi:10.1007/978-3-319-40970-2_23 · Zbl 06623523
[24] Rabe, M.N., Tentrup, L.: CAQE: a certifying QBF solver. In: Proceedings of FMCAD, pp. 136-143. IEEE (2015)
[25] Schewe, S., Finkbeiner, B.: Bounded synthesis. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 474-488. Springer, Heidelberg (2007). doi:10.1007/978-3-540-75596-8_33 · Zbl 1141.68491
[26] Seidl, M., Könighofer, R.: Partial witnesses from preprocessed quantified boolean formulas. In: Proceedings of DATE, pp. 1-6. European Design and Automation Association (2014)
[27] Shimakawa, M., Hagihara, S., Yonezaki, N.: Reducing bounded realizability analysis to reachability checking. In: Bojańczyk, M., Lasota, S., Potapov, I. (eds.) RP 2015. LNCS, vol. 9328, pp. 140-152. Springer, Heidelberg (2015). doi:10.1007/978-3-319-24537-9_13 · Zbl 06798773
[28] Tentrup, L.
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.