|
|
Efficient approach of translating LTL formulae into Büchi automata |
Laixiang SHAN1,*(),Xiaomin DU2,Zheng QIN3 |
1. Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China 2. School of Education Science, East China Normal University, Shanghai 200241, China 3. School of Software, Tsinghua University, Beijing 100084, China |
|
|
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
|
Corresponding Author(s):
Laixiang SHAN
|
Just Accepted Date: 30 December 2014
Issue Date: 07 September 2015
|
|
1 |
Katoen J P. Concepts, Algorithms, and Tools for Model Checking. Erlangen: IMMD, 1999
|
2 |
Babiak T, K?etínsky 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
https://doi.org/10.1007/978-3-642-28756-5_8
|
3 |
Gastin P, Oddoux D. Fast LTL to Büchi automata translation. Computer Aided Verification, 2001, 2102: 53―65
https://doi.org/10.1007/3-540-44585-4_6
|
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
https://doi.org/10.1007/3-540-48119-2_16
|
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
https://doi.org/10.1109/32.588521
|
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
https://doi.org/10.1007/3-540-36135-9_20
|
11 |
Babiak T, Badie T, Duret-Lutz A, K?etínsky M, Strej?ek J. Compositional approach to suspension and other improvements to LTL translation. Model Checking Software, 2013, 7976: 81―98
https://doi.org/10.1007/978-3-642-39176-7_6
|
12 |
Chatterjee K, Gaiser A, K?etínsky J. Automata with generalized rabin pairs for probabilistic model checking and LTL synthesis. Lecture Notes in Computer Science, 2013, 8044: 559―575
https://doi.org/10.1007/978-3-642-39799-8_37
|
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
https://doi.org/10.1007/978-3-642-45221-5_44
|
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
https://doi.org/10.1109/mascot.2004.1348184
|
16 |
Bryant R E. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 1986, C-35(8): 677―691
https://doi.org/10.1109/TC.1986.1676819
|
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
https://doi.org/10.1007/978-3-319-02444-8_31
|
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
https://doi.org/10.1007/s100090200070
|
[1] |
Supplementary Material-Highlights in 3-page ppt
|
Download
|
|
Viewed |
|
|
|
Full text
|
|
|
|
|
Abstract
|
|
|
|
|
Cited |
|
|
|
|
|
Shared |
|
|
|
|
|
Discussed |
|
|
|
|