Abstract
In model checking, properties are typically defined in linear temporal logic (LTL) and are translated into non-deterministic Büchi automata (NBA). In this paper, we propose a new, efficient translation method that is different from those used in LTL2BA, Spot and LTL3BA. Our method produces non-transition-based generalised Büchi automata (GBA) as an intermediate object, whereas LTL2BA, Spot, and LTL3BA use transition-based generalised Büchi automata (TGBA). Our method enables fast conversion because the data structure representing the object is simpler than that used in conversions via TGBA. Furthermore, we have developed techniques to reduce the number of states, similar to techniques that have heretofore only been available for conversions via TGBA. We also propose a technique to suppress the increase in the number of states that normally occurs while GBA is converted into NBA, using characteristics of strongly connected components of the GBA. We implemented our method with these techniques and experimentally compared our method with LTL2BA, Spot, and LTL3BA, which are the fastest translators to date. Our conversion method was much faster than LTL2BA and Spot, and was competitive with LTL3BA. In addition, the number of states in the NBA resulting from our method was comparable to that produced by LTL2BA, Spot, and LTL3BA.
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
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M., Lamport, L., Wolper, P.: Realizable and unrealizable specifications of reactive systems. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol. 372, pp. 1–17. Springer, Heidelberg (1989)
Aoshima, T., Sakuma, K., Yonezaki, N.: An efficient verification procedure supporting evolution of reactive system specifications. In: Proc. of the 4th International Workshop on Principles of Software Evolution, pp. 182–185. ACM (2001)
Aoshima, T., Yonezaki, N.: Verification of reactive system specification with outer event conditional formula. In: International Symposium on Principles of Software Evolution (ISPSE2000), pp. 195–199 (2000)
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)
Duret-Lutz, A.: LTL translation improvements in Spot. In: Proc. of the Fifth international conference on Verification and Evaluation of Computer and Communication Systems, VECoS 2011, pp. 72–83. British Computer Society (2011)
Duret-Lutz, A., Poitrenaud, D.: Spot: An extensible model checking library using transition-based generalized Büchi automata. In: Proc. of MASCOTS 2004, pp. 76–83. IEEE Computer Society (2004)
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)
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)
Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Protocol Specification Testing and Verification, pp. 3–18. Chapman & Hall (1995)
Giannakopoulou, D., Lerda, F.: From states to transitions: Improving translation of LTL formulae to Büchi automata. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 308–326. Springer, Heidelberg (2002)
Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997), http://dx.doi.org/10.1109/32.588521
Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: Formal Methods in Computer Aided Design, FMCAD 2006, pp. 117–124 (2006)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL 1989, pp. 179–190 (1989)
Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 149–167. Springer, Heidelberg (2007)
Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 248–263. Springer, Heidelberg (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Mochizuki, S., Shimakawa, M., Hagihara, S., Yonezaki, N. (2014). Fast Translation from LTL to Büchi Automata via Non-transition-based Automata. In: Merz, S., Pang, J. (eds) Formal Methods and Software Engineering. ICFEM 2014. Lecture Notes in Computer Science, vol 8829. Springer, Cham. https://doi.org/10.1007/978-3-319-11737-9_24
Download citation
DOI: https://doi.org/10.1007/978-3-319-11737-9_24
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-11736-2
Online ISBN: 978-3-319-11737-9
eBook Packages: Computer ScienceComputer Science (R0)