Abstract
Vacuity detection is a common practice accompanying model checking of hardware designs. Roughly speaking, a system satisfies a specification vacuously if it can satisfy a stronger specification obtained by replacing some of its subformulas with stronger expressions. If this happens then part of the specification is immaterial, which typically indicates that there is a problem in the model or the specification itself.
We propose to apply the concept of vacuity to the synthesis problem. In synthesis, there is often a problem that the specifications are incomplete, hence under-specifying the desired behaviour, which may lead to a situation in which the synthesised system is different than the one intended by the designer. To address this problem we suggest an algorithm and a tool for non-vacuous bounded synthesis. It combines synthesis for universal and existential properties; the latter stems from the requirement to have at least one interesting witness for each strengthening of the specification. Even when the system satisfies the specification non-vacuously, our tool is capable of improving it by synthesizing a system that has additional interesting witnesses. The user decides when the system reflects their intent.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
This means that we swap \(\psi \) with false if \(\psi \) is in positive polarity, and with true otherwise. Hence, e.g., if \(\varphi \equiv \psi _1 \Rightarrow \varPsi _2\), then \(\varphi [\psi _1 \leftarrow \bot ] \equiv \psi _2\).
- 2.
- 3.
Note the unusual semantics of LTL on this figure: In the trace \(\{g_2, r_1\}, \{g_1,r_1,r_2\},\{g_2\}^{\omega }\), the request \(r_1\) on the outgoing edge of \(s_1\) is granted by the label \(g_1\) on the state \(s_1\) itself.
- 4.
Since \(\mathcal {G}\) is only used for checking emptiness, the labels are immaterial, and it is customary to use a one-letter automaton (i. e., \(\vert \varSigma \vert = \vert \varUpsilon \vert = 1\)).
References
Armoni, R., Fix, L., Flaisher, A., Grumberg, O., Piterman, N., Tiemeyer, A., Vardi, M.Y.: Enhanced vacuity detection in linear temporal logic. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 368–380. Springer, Heidelberg (2003). doi:10.1007/978-3-540-45069-6_35
Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in ACTL formulas. Formal Methods Syst. Des. 18(2), 141–163 (2001)
Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T.A., Hofferek, G., Jobstmann, B., Könighofer, B., Könighofer, R.: Synthesizing robust systems. Acta Inf. 51, 193–220 (2014)
Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 140–156. Springer, Berlin (2009). doi:10.1007/978-3-642-02658-4_14
Bustan, D., Flaisher, A., Grumberg, O., Kupferman, O., Vardi, M.Y.: Regular vacuity. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 191–206. Springer, Heidelberg (2005). doi:10.1007/11560548_16
Gurfinkel, A., Chechik, M.: Extending extended vacuity. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 306–321. Springer, Heidelberg (2004). doi:10.1007/978-3-540-30494-4_22
Chockler, H., Gurfinkel, A., Strichman, O.: Beyond vacuity: towards the strongest passing formula. Formal Methods Syst. Des. 43(3), 552–571 (2013)
Church, A.: Logic, arithmetics, and automata. In: ICM (1963)
Finkbeiner, B., Schewe, S.: Bounded synthesis. Int. J. Softw. Tools Technol. Transfer 15(5), 519–539 (2012)
Jacobs, S., Bloem, R., Brenguier, R., Könighofer, R., Pérez, G.A., Raskin, J., Ryzhyk, L., Sankur, O., Seidl, M., Tentrup, L., Walker, A.: The second reactive synthesis competition. In: SYNT (2015)
Jobstmann, B., Staber, S., Griesmayer, A., Bloem, R.: Finding and fixing faults. J. Comput. Syst. Sci. 78(2), 441–460 (2012)
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
Kupferman, O., Vardi, M.: Vacuity detection in temporal model checking. J. Softw. Tools Technol. Transfer 4(2), 224–233 (2003)
Namjoshi, K.S.: An efficiently checkable, proof-based formulation of vacuity in model checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 57–69. Springer, Heidelberg (2004). doi:10.1007/978-3-540-27813-9_5
Pnueli, A.: The temporal logic of programs. In: FOCS (1977)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL (1989)
Samanta, R., Deshmukh, J.V., Chaudhuri, S.: Robustness analysis of networked systems. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 229–247. Springer, Heidelberg (2013). doi:10.1007/978-3-642-35873-9_15
Vardi, M., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1–37 (1994)
Acknowledgments
This work was supported by the TU Graz LEAD project “Dependable Internet of Things in Adverse Environments” and the Austrian Science Fund (FWF) under the RiSE National Research Network (S11406). We would like to thank Nir Piterman for his insights on infinite chains of ever less vacuous systems and Ayrat Khalimov for his comments on existential bounded synthesis and his valuable assistance with the implementation.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Bloem, R., Chockler, H., Ebrahimi, M., Strichman, O. (2017). Synthesizing Non-Vacuous Systems. In: Bouajjani, A., Monniaux, D. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2017. Lecture Notes in Computer Science(), vol 10145. Springer, Cham. https://doi.org/10.1007/978-3-319-52234-0_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-52234-0_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-52233-3
Online ISBN: 978-3-319-52234-0
eBook Packages: Computer ScienceComputer Science (R0)