On-the-fly translation algorithm from linear temporal logic to Büchi automata

Abstract
Figures/Tables
References
Related Articles
Metrics

Download: PDF(1206 KB) HTML
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks Supporting Info

Guide

Abstract

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.

Keywords linear temporal logic transition-based Büchi automata on-the-fly

ZTFLH:

Fund:

Issue Date: 15 February 2014

	Service

	E-mail this article
	E-mail Alert
	RSS
	Articles by authors

	Laixiang SHAN
	Zheng QIN
	Xinye LU
	Zhengcai LU

Cite this article:

Laixiang SHAN,Zheng QIN,Xinye LU, et al. On-the-fly translation algorithm from linear temporal logic to Büchi automata[J]. Journal of Tsinghua University(Science and Technology), 2014, 54(2): 281-288.

URL:

http://jst.tsinghuajournals.com/EN/ OR http://jst.tsinghuajournals.com/EN/Y2014/V54/I2/281

[1]	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.
[2]	Holzmann G J. The model checker SPIN[J]. IEEE Transactions on Software Engineering, 1997, 23(5): 279-295. url: http://dx.doi.org/10.1109/32.588521
[3]	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.
[4]	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.
[5]	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.
[6]	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.
[7]	Gastin P, Oddoux D. Fast LTL to Büchi automata translation [C]//Computer Aided Verification. Berlin, Heidelberg, Germany: Springer, 2001: 53-65.
[8]	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.
[9]	Fritz C. Concepts of automata construction from LTL [C]//Logic for Programming, Artificial Intelligence, and Reasoning. Berlin, Heidelberg, Germany: Springer, 2005: 728-742.
[10]	Boker U, Kupferman O, Rosenberg A. Alternation removal in Büchi automata [C]//Automata, Languages and Programming. Berlin, Heidelberg, Germany: Springer, 2010: 76-87.
[11]	Juvekar S, Piterman N. Minimizing generalized Büchi automata [C]//Computer Aided Verification. Berlin, Heidelberg, Germany: Springer, 2006: 45-58.
[12]	Somenzi F, Bloem R. Efficient Büchi automata from LTL formulae [C]//Computer Aided Verification. Berlin, Heidelberg, Germany: Springer, 2000: 248-263.
[13]	Etessami K, Holzmann G J. Optimizing Büchi automata [C]//CONCUR 2000: Concurrency Theory. Berlin, Heidelberg, Germany: Springer, 2000: 153-168.
[14]	Yin C, Luo G. Efficient translation of LTL to Büchi automata[J].Tsinghua Science & Technology, 2009, 14(1): 75-82.
[15]	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.
[16]	Ehlers R, Finkbeiner B. On the virtue of patience: Minimizing Büchi automata [C]//Model Checking Software. Berlin, Heidelberg, Germany: Springer, 2010: 129-145.
[17]	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.

[1]	Kexin DENG. Retinal image registration based on hyper-edge graph matching[J]. Journal of Tsinghua University(Science and Technology), 2014, 54(5): 568-574.
[2]	Chen HAO, Fu LI, Jiong GUO. Simulations of mixing in the pebble flow of a pebble bed HTR[J]. Journal of Tsinghua University(Science and Technology), 2014, 54(5): 624-628.
[3]	Pengfei LIN, Xiaojian ZHANG, Chao CHEN, Jun WANG. Treatment of molybdenum-containing wastewater and drinking water[J]. Journal of Tsinghua University(Science and Technology), 2014, 54(5): 613-618.
[4]	Qi MIN, Yuanyuan DUAN, Xiaodong WANG. Lattice Boltzmann method for the fluid saturation density based on the volume translated Peng-Robinson equation of state[J]. Journal of Tsinghua University(Science and Technology), 2014, 54(5): 619-623.
[5]	Zhenbo WANG, Jun ZHANG, Yiming LUOSUN. Flexural performance of textile reinforced cementitious composite with sprinkling water hardening technique[J]. Journal of Tsinghua University(Science and Technology), 2014, 54(5): 551-555.
[6]	Feng JIANG, Ziwei ZHUANG, Zhenzhong ZHANG, Jiying WEI. Evaporation-condensation technology for testing the efficiency of HEPA filter media[J]. Journal of Tsinghua University(Science and Technology), 2014, 54(5): 629-632.
[7]	Xinrong CAO, Lei LIU, Dongyang CAI, Peng GUO, Jintian TANG. Statistical analyses of ballistocardiogram features for cardiac disease diagnosis[J]. Journal of Tsinghua University(Science and Technology), 2014, 54(5): 633-637.
[8]	Wu XU, Qing YU, Guohuang YAO. Effect of preload on the axial capacity of CFST reinforced concrete columns[J]. Journal of Tsinghua University(Science and Technology), 2014, 54(5): 556-562.
[9]	Ya WEI, Xiangjie YAO. Tensile creep model for concrete subject to constant restraints[J]. Journal of Tsinghua University(Science and Technology), 2014, 54(5): 563-567.
[10]	Ronghua LIU, Jiahua WEI, Yanzhang WENG, Guangqian WANG, Shuang TANG. HydroMP: A cloud computing based platform for hydraulic modeling and simulation service[J]. Journal of Tsinghua University(Science and Technology), 2014, 54(5): 575-583.
[11]	Na ZHAO, Zhaoyin WANG, Baozhu PAN, Zhiwei LI, Xuehua DUAN. Ecological functions of riverbed structures with different strengths in the Xiaojiang River basin[J]. Journal of Tsinghua University(Science and Technology), 2014, 54(5): 584-589.
[12]	Hanbo YANG, Huafang LV, Qingfang HU, Huimin LEI, Dawen YANG. Comparison of parametrization methods for calculating the downward long-wave radiation over the North China Plain[J]. Journal of Tsinghua University(Science and Technology), 2014, 54(5): 590-595.
[13]	Fenjie LONG, Zhenxing LONG, Xiaomeng WANG. Effect of equity constraints on housing prices in rising markets[J]. Journal of Tsinghua University(Science and Technology), 2014, 54(5): 596-601.
[14]	Hong ZHANG, Yang ZHANG, Xuanbing CHEN. Experimental evaluation of Beijing resale housing information diffusion during information transmission[J]. Journal of Tsinghua University(Science and Technology), 2014, 54(5): 602-606.
[15]	Hongwei YANG, Haoyu WANG, Yunxia LIU, Wenjun LIU, Shaoxia YANG. Ozone-biological activated carbon treatment of DBP in high-bromide water[J]. Journal of Tsinghua University(Science and Technology), 2014, 54(5): 607-612.

Viewed

Full text

Abstract

Cited

Shared

Discussed