SHAN Laixiang, QIN Zheng. LTL Formulae to Büchi Automata Translation Using on-the-Fly De-generalization[J]. Chinese Journal of Electronics, 2015, 24(4): 674-678. doi: 10.1049/cje.2015.10.002
Citation: SHAN Laixiang, QIN Zheng. LTL Formulae to Büchi Automata Translation Using on-the-Fly De-generalization[J]. Chinese Journal of Electronics, 2015, 24(4): 674-678. doi: 10.1049/cje.2015.10.002

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

doi: 10.1049/cje.2015.10.002
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
  • 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.
  • loading
  • 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.
  • 加载中

Catalog

    通讯作者: 陈斌, bchen63@163.com
    • 1. 

      沈阳化工大学材料科学与工程学院 沈阳 110142

    1. 本站搜索
    2. 百度学术搜索
    3. 万方数据库搜索
    4. CNKI搜索

    Article Metrics

    Article views (255) PDF downloads(860) Cited by()
    Proportional views
    Related

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return