WEI Xiujuan, LI Yongming. An Automata-Theoretic Approach to L-valued Computation Tree Logic Model Checking[J]. Chinese Journal of Electronics, 2019, 28(2): 309-315. doi: 10.1049/cje.2019.01.014
Citation: WEI Xiujuan, LI Yongming. An Automata-Theoretic Approach to L-valued Computation Tree Logic Model Checking[J]. Chinese Journal of Electronics, 2019, 28(2): 309-315. doi: 10.1049/cje.2019.01.014

An Automata-Theoretic Approach to L-valued Computation Tree Logic Model Checking

doi: 10.1049/cje.2019.01.014
Funds:  This work is supported by the National Natural Science Foundation of China (No.11271237, No.11671244) and Ph.D. Programs Foundation of Ministry of Education of China (No.20130202110001).
More Information
  • Corresponding author: LI Yongming (corresponding author) was born in 1966. He received the Ph.D. degree from Sichuan University. He is a professor of Shaanxi Normal University. His research interests include computational intelligence, non-classical computation theory, quantum computing and quantum information, and topology over lattices. (Email:liyongm@snnu.edu.cn)
  • Received Date: 2016-11-28
  • Rev Recd Date: 2018-05-11
  • Publish Date: 2019-03-10
  • Translating computation tree logic formulas into Büchi tree automata has been proven to be an effective approach for implementing branching-time model checking. For a more generalized class of lattice-valued (L-valued, for short) computation tree logic formulas, the revelent study has not proceeded yet. We introduce the notion of L-valued alternating Büchi tree automata and achieve the goal of associating each L-valued computation tree logic formula with an L-valued Büchi tree automaton. We show that a satisfiability problem for an L-valued computation tree logic formula can be reduced to one for the language accepted by an L-valued Büchi tree automaton. L-valued alternating Büchi tree automata are the key to the automata-theoretic approach to L-valued computation tree logics, and we also study their expressive power and closure properties.
  • loading
  • C. Baier and J.P. Katoen, Principles of Model Checking, The MIT Press Cambridge, London, 2008.
    L.X. Shan and Z. Qin, “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.
    M.Y. Vardi, “An automata-theoretic approach to linear temporal logic”, Lecture Notes in Computer Science, Vol.1043, pp.238-266, 2005.
    M.Y. Vardi, P. Wolper, “An automata-theoretic approach to automatic program verification”, Proceedings of LICS, pp.322-331, 1986.
    O. Bernholtz, M.Y. Vardi and P. Wolper, “An automatatheoretic approach to branching-time model checking (Extended abstract)”, Lecture Notes in Computer Science, Vol.818, pp.142-155, 2005.
    O. Kupferman, M.Y. Vardi and P. Wolper, “An automatatheoretic approach to branching-time model checking”, Journal of the ACM, Vol.47, No.2, pp.312-360, 2000.
    A.K. Chandra, D.C. Kozen and L.J. Stockmeyer, “Alternation”, Journal of the ACM, Vol.28, No.1, pp.114-133, 1981.
    S. Miyano and T. Hayashiiyano, “Alternating finite automata on !-words”, Theoretical Computer Science, Vol.32, pp.321-330, 1984.
    H. Comon, M. Dauchet, R. Gilleron et al., “Tree Automata: Techniques and Applications”, available at http://tata.gforge.inria.fr, 2007.
    D.E. Muller and P.E. Schupp, “Alternating automata on infinite trees”, Theoretical Computer Science, Vol.54, pp.267-276, 1987.
    D.E. Muller and P.E. Schupp, “Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra”, Theoretical Computer Science, Vol.141, pp.69-107, 1995.
    M. Chechik, B. Devereux, A. Gurfinkel et al., “Multi-valued symbolic model-checking”, ACM Transactions on Software Engineering and Methodology, Vol.12, No. 4, pp.371-408, 2003.
    M. Chechik, S. Easterbrook and V. Petrovykh, “Modelchecking over multi-valued logics”, Lecture Notes in Computer Science, Vol.2021, pp.72-98, 2001.
    Y.H Fan, Y.M. Li and H.Y. Pan, “Computation tree logic model checking for nondeterministic fuzzy Kripke structure”, Acta Electronica Sinica, Vol.46, No.1, pp.152-159, 2018. (in Chinese)
    Y.M. Li, Y.L. Li and Z.Y. Ma, “Computation tree logic model checking based on possibility measures”, Fuzzy Sets and Systems, Vol.261, pp.44-59, 2015.
    Y.M. Li and Z.Y. Ma, “Quantitative computation tree logic model checking based on generalized possibility measures”, IEEE Transactions on Fuzzy Systems, Vol.23, No.6, pp.2034-2047, 2015.
    C.J. Liang and Y.M. Li, “The model checking problem of computing tree logic based on generalized possibility measure”, Acta Electronica Sinica, Vol.45, No.11, pp. 2641-2648, 2017. (in Chinese)
    C.J. Liang and Y.M. Li, “Model checking of fuzzy linear temporal logic based on generalized possibility measure”, Acta Electronica Sinica, Vol.45, No.12, pp.2971-2977, 2017. (in Chinese)
    Z.Y. Ma and Y.M. Li, “Model checking generalized possibilistic computation tree logic based on decision processes”, Science China Information Sciences, Vol.46, No.11, pp.1591-1607, 2016. (in Chinese)
    H.Y. Pan, Y.M. Li, Y.Z. Cao et al., “Model checking fuzzy computation tree logic”, Fuzzy Sets and Systems, Vol.262, pp.60-77, 2015.
    H.Y. Pan, Y.M. Li, Y.Z. Cao et al., “Model checking computation tree logic over finite lattices”, Theoretical Computer Science, Vol.612, pp.45-62, 2016.
    H.Y. Pan, M. Zhang, H.Y. Wu et al., “Quantitative analysis of lattice-valued Kripke structures”, Fundamenta Informaticae, Vol.135, No.3, pp.269-293, 2014.
    Y.G. Lin, H.X. Lei and Y.M. Li, “Model checking of safety property over quantum Markov chain”, Acta Electronica Sinica, Vol.42, No.11, pp.2091-2097, 2014.
    M. Droste, W. Kuich and H. Vogler(eds.), Handbook of Weighted Automata, Monographs in Theoretical Computer Science, Berlin Heidelberg, Springer-Verlag, 2009.
    X.J. Wei and Y.M. Li, “Fuzzy alternating Büchi automata over distributive lattices”, International Journal of Approximate Reasoning, Vol.90, pp.144-162, 2017.
    X.J. Wei and Y.M. Li, “Fuzzy alternating automata over distributive lattices”, Information Sciences, Vol.425, pp.34-47, 2018.
    B.A. Davey and H.A. Priestley, Introduction to Lattices and Order, Cambridge University Press, 1990.
  • 加载中

Catalog

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

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

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

    Article Metrics

    Article views (118) PDF downloads(154) Cited by()
    Proportional views
    Related

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return