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.

# 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).
• 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)
• 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.
•  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

/
{"extraction_info": {"found_math": false, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "math_score": 0.8629839420318604, "perplexity": 15089.181887578448}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 5, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "plain"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "warc_path": "s3://commoncrawl/crawl-data/CC-MAIN-2022-27/segments/1656103355949.26/warc/CC-MAIN-20220628050721-20220628080721-00506.warc.gz"}