LTL Formulae to Büchi Automata Translation Using on-the-Fly De-generalization

SHAN Laixiang; QIN Zheng

doi:10.1049/cje.2015.10.002

Volume 24 Issue 4

Turn off MathJax

Article Contents

Article Navigation > Chinese Journal of Electronics > 2015 > 24(4): 674-678

SHAN Laixiang and QIN Zheng, “LTL Formulae to Büchi Automata Translation Using on-the-Fly De-generalization,” Chinese Journal of Electronics, vol. 24, no. 4, pp. 674-678, 2015, doi: 10.1049/cje.2015.10.002

Citation:

SHAN Laixiang and QIN Zheng, “LTL Formulae to Büchi Automata Translation Using on-the-Fly De-generalization,” Chinese Journal of Electronics, vol. 24, no. 4, pp. 674-678, 2015, doi: 10.1049/cje.2015.10.002

Citation:

PDF( 411 KB)

LTL Formulae to Büchi Automata Translation Using on-the-Fly De-generalization

doi: 10.1049/cje.2015.10.002

SHAN Laixiang¹,
QIN Zheng^2
,

1.
Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China;
2.
School of Software, Tsinghua University, Beijing 100084, China

Funds: This work is supported by the Specialized Research Fund for the Doctoral Program of Higher Education (No.20120002130007) and the National Basic Research Program of China (No.9140A1550212JW01047).

More Information

Corresponding author: QIN Zheng (corresponding author)was born in Hunan Province, China, in1956. He is a professor in the School ofSoftware, Tsinghua University. His majorresearch interest includes software architecture,data fusion and artificial intelligence.(Email: qingzh@mail.tsinghua.edu.cn)
Received Date: 2014-07-07
Rev Recd Date: 2014-08-28
Publish Date: 2015-10-10

Abstract

Abstract

In this paper, we present a conversion algorithm to translate a Linear temporal logic (LTL) formula to a Büchi automaton (BA) directly. Acceptance degree (AD) is presented to record acceptance conditions satisfied in each state and transition of the BA. According to AD, on-the-fly de-generalization algorithm, which is different from the standard de-generalization algorithm, is conceived and implemented. On-the-fly de-generalization algorithm is performed in the case of the given LTL formula containing U-subformulae or F-subformulae, that is, it is performed as required during the expansion of the given LTL formula. We compare the conversion algorithm presented in this paper to previous works, and show that it is more efficient for a series of LTL formulae in common use.
- Formal method,
- Model checking,
- Linear temporal logic,
- On-the-fly de-generalization

FullText(HTML)

References(11)

References

E.M. Clarke, O. Grumberg and D.A. Peled, Model Checking, MIT Press, The United States, 1999.

Babiak Tomáš, M. K?etínský, V. ?ehák, et al., "LTL to Büchi automata translation: Fast and more deterministic", Tools and Algorithms for the Construction and Analysis of Systems, Springer Berlin Heidelberg, pp.95-109, 2012.

A. Duret-Lutz, "LTL translation improvements in spot", The Fifth International Conference on Verification and Evaluation of Computer and Communication Systems, British Computer Society, pp.72-83, 2011.

Z. LU, Z. QIN, Q. JIN, et al., "Constructing rough set based unbalanced binary tree for feature selection", Chinese Journal of Electronics, Vol.23, No.3, pp.474-479, 2014.

R. Gerth, D. Peled, M.Y. Vardi, et al., "Simple on-the-fly automatic verification of linear temporal logic", Proc. of the 15th Workshop on Protocol Specification, Testing and Verification (PSTV‘95), Warsaw, Poland, pp.3-18, 1995.

L. Shan, Z. Qin, S. Li, et al., "Conversion algorithm of linear time temporal logic to Büchi automata", Journal of Software, Vol.9, No.4, pp.970-976, 2014.

F. Somenzi, "Cudd: Cu decision diagram package, release 2.5.0, 2012", http://vlsi.colorado.edu, 2012-5-23.

J. Lind-Nielsen, "Buddy: A binary decision diagram package: version 2.2, 2003", http://vlsicad.eecs.umich.edu/BK/Slots/ca che/www.itu.dk/research/buddy/, 2003-1-7.

Cichon Jacek, Adam Czubak and Andrzej Jasinski, "Minimal büchi automata for certain classes of LTL formulas", Fourth International Conference on Dependability of Computer Systems (DepCos-RELCOMEX09), IEEE, pp.17-24, 2009.

A. Duret-Lutz, "Manipulating LTL formulas using spot 1.0", Automated Technology for Verification and Analysis, Springer, pp.442-445, 2013.

Laixiang Shan, Jun Qin, Mingshi Chen, et al., "De-generalization algorithm for generation büchi automata based on contented situation", Journal of Applied Mathematics, Vol.2015, Article ID 516104, 10 pages, 2015, doi: 10.1155/2015/516104.

Relative Articles

Supplements(0)

Cited By

Proportional views