×

zbMATH — the first resource for mathematics

Unbeast: symbolic bounded synthesis. (English) Zbl 1316.68073
Abdulla, Parosh Aziz (ed.) et al., 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. Berlin: Springer (ISBN 978-3-642-19834-2/pbk). Lecture Notes in Computer Science 6605, 272-275 (2011).
Summary: We present Unbeast v.0.6, a tool for synthesising finite-state systems from specifications written in linear-time temporal logic (LTL). We combine bounded synthesis, specification splitting and symbolic game solving with binary decision diagrams (BDDs), which allows tackling specifications that previous tools were typically unable to handle. In case of realizability of a given specification, our tool computes a prototype implementation in a fully symbolic way, which is especially beneficial for settings with many input and output bits.
For the entire collection see [Zbl 1213.68016].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68W30 Symbolic computation and algebraic computation
Software:
CUDD; LTL2BA; NuSMV
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Specify, compile, run: Hardware from PSL. ENTCS 190(4), 3–16 (2007)
[2] Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002) · Zbl 1010.68766 · doi:10.1007/3-540-45657-0_29
[3] Ehlers, R.: Symbolic bounded synthesis. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 365–379. Springer, Heidelberg (2010) · Zbl 05772646 · doi:10.1007/978-3-642-14295-6_33
[4] Filiot, E., Jin, N., Raskin, J.F.: An antichain algorithm for LTL realizability. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 263–277. Springer, Heidelberg (2009) · Zbl 1242.68158 · doi:10.1007/978-3-642-02658-4_22
[5] Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001) · Zbl 0991.68044 · doi:10.1007/3-540-44585-4_6
[6] Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods in System Design 19(3), 291–314 (2001) · Zbl 0995.68061 · doi:10.1023/A:1011254632723
[7] 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) · Zbl 1141.68491 · doi:10.1007/978-3-540-75596-8_33
[8] Somenzi, F.: CUDD: CU Decision Diagram package release 2.4.2 (2009)
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.