Please wait a minute...
Frontiers of Computer Science

ISSN 2095-2228

ISSN 2095-2236(Online)

CN 10-1014/TP

Postal Subscription Code 80-970

2018 Impact Factor: 1.129

Front. Comput. Sci.    2015, Vol. 9 Issue (4) : 511-523    https://doi.org/10.1007/s11704-015-4302-z
RESEARCH ARTICLE
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
 Download: PDF(524 KB)  
 Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks
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
 Cite this article:   
Laixiang SHAN,Xiaomin DU,Zheng QIN. Efficient approach of translating LTL formulae into Büchi automata[J]. Front. Comput. Sci., 2015, 9(4): 511-523.
 URL:  
https://academic.hep.com.cn/fcs/EN/10.1007/s11704-015-4302-z
https://academic.hep.com.cn/fcs/EN/Y2015/V9/I4/511
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
[1] Yuanrui ZHANG, Frédéric MALLET, Yixiang CHEN. A verification framework for spatio-temporal consistency language with CCSL as a specification language[J]. Front. Comput. Sci., 2020, 14(1): 105-129.
[2] Kazuhiro OGATA. A divide & conquer approach to liveness model checking under fairness & anti-fairness assumptions[J]. Front. Comput. Sci., 2019, 13(1): 51-72.
[3] Anil Kumar KARNA, Yuting CHEN, Haibo YU, Hao ZHONG, Jianjun ZHAO. The role of model checking in software engineering[J]. Front. Comput. Sci., 2018, 12(4): 642-668.
[4] Yu ZHOU, Nvqi ZHOU, Tingting HAN, Jiayi GU, Weigang WU. Probabilistic verification of hierarchical leader election protocol in dynamic systems[J]. Front. Comput. Sci., 2018, 12(4): 763-776.
[5] Fei HE, Yuan GAO, Liangze YIN. Efficient software product-line model checking using induction and a SAT solver[J]. Front. Comput. Sci., 2018, 12(2): 264-279.
[6] Luxi CHEN,Linpeng HUANG,Chen LI,Tao ZAN. Integrating behavior analysis into architectural modeling[J]. Front. Comput. Sci., 2015, 9(1): 15-33.
[7] Yuanjie SI, Jun SUN, Yang LIU, Jin Song DONG, Jun PANG, Shao Jie ZHANG, Xiaohu YANG. Model checking with fairness assumptions using PAT[J]. Front. Comput. Sci., 2014, 8(1): 1-16.
[8] Savas KONUR. A survey on temporal logics for specifying and verifying real-time systems[J]. Front. Comput. Sci., 2013, 7(3): 370-403.
[9] Anh Tuan LUU, Jun SUN, Yang LIU, Jin Song DONG, Xiaohong LI, Thanh Tho QUAN. SeVe: automatic tool for verification of security protocols[J]. Front Comput Sci, 2012, 6(1): 57-75.
[10] Conghua ZHOU, Bo SUN, Zhifeng LIU. Abstraction for model checking multi-agent systems[J]. Front Comput Sci Chin, 2011, 5(1): 14-25.
[11] Jiaqi ZHU, Hanpin WANG, Zhongyuan XU, Chunxiang XU, . A new model for model checking: cycle-weighted Kripke structure[J]. Front. Comput. Sci., 2010, 4(1): 78-88.
[12] Wanwei LIU, Ji WANG, Huowang CHEN, Xiaodong MA, Zhaofei WANG. symbolic model checking APSL[J]. Front Comput Sci Chin, 2009, 3(1): 130-141.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed