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 |
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.
|