1. Tsinghua National Laboratory for Information Science and Technology, Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China
2. School of Software, Tsinghua University, Beijing 100084, China
3. Institute of Software Chinese Academy of Sciences, Beijing 100190, China
Translations of linear temporal logic to Büchi automata are key to explicit model checking, with the Tableau-based algorithm commonly used for the translation. This paper describes an improved Tableau-based algorithm which converts linear temporal logic to transition-based Büchi automata. The satisfaction information of the U-formula for the states and transitions is used to judge whether the automata is acceptable using only one acceptance condition set, rather than multiple sets. Thus, the algorithm gives an on-the-fly degeneralization mechanism that can expand the state nodes while detecting their validity and removing invalid nodes. The algorithm combines equivalent states and transitions and avoids simplifications after forming the final automata. Comparisons with other conversion tools show that this algorithm runs faster with less states and transitions in the automaton.
Gerth R, Peled D, Vardi M Y, et al.Simple on-the-fly automatic verification of linear temporal logic [C]//Proceedings of the 15th IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification. Seneca, USA: IFIP, 1995.
Holzmann G J. The model checker SPIN[J]. IEEE Transactions on Software Engineering, 1997, 23(5): 279-295.
Daniele M, Giunchiglia F, Vardi M Y. Improved automata generation for linear temporal logic [C]//Computer Aided Verification. Berlin, Heidelberg, Germany: Springer 1999: 249-260.
Giannakopoulou D, Lerda F. From states to transitions: Improving translation of LTL formulae to Büchi automata [C]//Formal Techniques for Networked and Distributed Sytems, FORTE 2002. Berlin, Heidelberg, Germany: Springer, 2002: 308-326.
Duret-Lutz A. LTL translation improvements in spot [C]//Proceedings of the 5th International Conference on Verification and Evaluation of Computer and Communication Systems. Swinton, UK: British Computer Society, 2011: 72-83.
Shoshmina I V, Belyaev A B. Symbolic algorithm for generation Büchi automata from LTL formulas [C]//Parallel Computing Technologies. Berlin, Heidelberg, Germany: Springer, 2011: 98-109.
Gastin P, Oddoux D. Fast LTL to Büchi automata translation [C]//Computer Aided Verification. Berlin, Heidelberg, Germany: Springer, 2001: 53-65.
Babiak T, Kretínsky M, Rehák V, et al.LTL to Büchi automata translation: Fast and more deterministic [C]//Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg, Germany: Springer, 2012: 95-109.
Fritz C. Concepts of automata construction from LTL [C]//Logic for Programming, Artificial Intelligence, and Reasoning. Berlin, Heidelberg, Germany: Springer, 2005: 728-742.
Boker U, Kupferman O, Rosenberg A. Alternation removal in Büchi automata [C]//Automata, Languages and Programming. Berlin, Heidelberg, Germany: Springer, 2010: 76-87.
Somenzi F, Bloem R. Efficient Büchi automata from LTL formulae [C]//Computer Aided Verification. Berlin, Heidelberg, Germany: Springer, 2000: 248-263.
Etessami K, Holzmann G J. Optimizing Büchi automata [C]//CONCUR 2000: Concurrency Theory. Berlin, Heidelberg, Germany: Springer, 2000: 153-168.
Yin C, Luo G. Efficient translation of LTL to Büchi automata[J].Tsinghua Science & Technology, 2009, 14(1): 75-82.
Sebastiani R, Tonetta S. “More deterministic” vs.“smaller” Büchi automata for efficient LTL model checking [C]//Correct Hardware Design and Verification Methods. Berlin, Heidelberg, Germany: Springer, 2003: 126-140.
Ehlers R, Finkbeiner B. On the virtue of patience: Minimizing Büchi automata [C]//Model Checking Software. Berlin, Heidelberg, Germany: Springer, 2010: 129-145.
Lu X, Luo G. Direct translation of LTL formulas to Büchi automata [C]//2012 IEEE 11th International Conference on Cognitive Informatics & Cognitive Computing (ICCI*CC). Bratislava, Slovak: IEEE Press, 2012: 323-328.