Efficient approach of translating LTL formulae into Büchi automata

Abstract

In explicit-state model checking, system properties are typically expressed in linear temporal logic (LTL), and translated into a Büchi automaton (BA) to be checked. In order to improve performance of the conversion algorithm, some model checkers involve the intermediate automata, such as a generalized Büchi automaton (GBA). The de-generalization is a translation from a GBA to a BA. In this paper, we present a conversion algorithm to translate an LTL formula to a BA directly. A labeling, acceptance degree, is presented to record acceptance conditions satisfied in each state and transition. Acceptance degree is a set of U-subformulae or F-subformulae of the given LTL formula. According to the acceptance degree, on-the-fly degeneralization algorithm, which is different from the standard de-generalization algorithm, is conceived and implemented. On-the-fly de-generalization algorithm is carried out during the expansion of the given LTL formula. It is performed in the case of the given LTL formula contains U-subformulae and F-subformulae, that is, the on-the-fly de-generalization algorithm is performed as required. In order to get a more deterministic BA, the shannon expansion is used recursively during expanding LTL formulae. Ordered binary decision diagrams are used to represent the BA and simplify LTL formulae.We compare the conversion algorithm presented in this paper to previousworks, and show that it is more efficient for five families LTL formulae in common use and four sets of random formulae generated by LBTT (an LTL-to-Büchi translator testbench).

Keywords

model checking / Büchi automata / acceptance degree / on-the-fly de-generalization

References

[1] Katoen J P. Concepts, Algorithms, and Tools for Model Checking. Erlangen: IMMD, 1999

[2] Babiak T, Křetínský M, Řehák V, Strejček J. LTL to Büchi automata translation: Fast and more deterministic. Lecture Notes in Computer Science, 2012, 7214: 95―109

[3] Gastin P, Oddoux D. Fast LTL to Büchi automata translation. Computer Aided Verification, 2001, 2102: 53―65

[4] Boker U, Kupferman O, Rosenberg A. Alternation removal in Büchi automata. Automata, Languages and Programming, 2010, 6199: 76―87

[5] Duret-Lutz A. Ltl translation improvements in spot. In: Proceedings of the 5th International Conference on Verification and Evaluation of Computer and Communication Systems. British Computer Society, 2011, 72―83

[6] Couvreur J M. On-the-fly verification of linear temporal logic. Lecture Notes in Computer Science, 1999, 1708: 253―271

[7] Gerth R, Peled D, Vardi M Y, Wolper P. Simple on-the-fly automatic verification of linear temporal logic. In: Proceedings of the 15th IFIP WG6. 1 International Symposium on Protocol Specification, Testing and Verification. 1995

[8] Holzmann G J. The model checker spin. IEEE Transactions on Software Engineering, 1997, 23(5): 279―295

[9] Clarke E M, Grumberg O, Peled D A. Model Checking. The United States: MIT Press, 1999

[10] Giannakopoulou D, Lerda F. From states to transitions: improving translation of LTL formulae to Büchi automata. In: Proceedings of Joint Conterece on Formal Techniques for Networked and Distributed Sytems (FORTE 2002). 2002, LNCS, 2529: 308―326

[11] Babiak T, Badie T, Duret-Lutz A, Křetínský M, Strejček J. Compositional approach to suspension and other improvements to LTL translation. Model Checking Software, 2013, 7976: 81―98

[12] Chatterjee K, Gaiser A, Křetínský J. Automata with generalized rabin pairs for probabilistic model checking and LTL synthesis. Lecture Notes in Computer Science, 2013, 8044: 559―575

[13] Shan L, Qin Z, Li S, Zhang R, Yang X. Conversion algorithm of lineartime temporal logic to Büchi automata. Journal of Software, 2014, 9(4): 970―976

[14] Renault E, Duret-Lutz A, Kordon F, Poitrenaud D. Three scc-based emptiness checks for generalized Büchi automata. Lecture Notes in Computer Science, 2013, 8312: 668―682

[15] Duret-Lutz A, Poitrenaud D. Spot: an extensible model checking library using transition-based generalized büchi automata. In: Proceedings of the IEEE Computer Society’s 12th Annual International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems. 2004, 76―83

[16] Bryant R E. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 1986, C-35(8): 677―691

[17] Somenzi F. Cudd: Cu decision diagram package-release 2.4. 0. University of Colorado at Boulder. 2009

[18] Lind-Nielsen J. Buddy: a binary decision diagram package. Technical report. 1999

[19] Somenzi F. Cudd: Cu decision diagram package, release 2.5. 0. 2012.

[20] Cichon J, Czubak A, Jasinski A. Minimal Büchi automata for certain classes of LTL formulas. In: Proceedings. of the 4th International Conference on Dependability of Computer Systems. 2009, 17―24

[21] Duret-Lutz A. Manipulating LTL formulas using spot 1.0. Lecture Notes in Computer Science, 2013, 8172: 442―445

[22] Tauriainen H, Heljanko K. Testing LTL formula translation into Büchi automata. International Journal on Software Tools for Technology Transfer, 2002, 4(1): 57―70

RIGHTS & PERMISSIONS

Higher Education Press and Springer-Verlag Berlin Heidelberg