An Automata-Theoretic Approach to <i>L</i>-valued Computation Tree Logic Model Checking

WEI Xiujuan; LI Yongming

doi:10.1049/cje.2019.01.014

Volume 28 Issue 2

Turn off MathJax

Article Contents

Article Navigation > Chinese Journal of Electronics > 2019 > 28(2): 309-315

WEI Xiujuan and LI Yongming, “An Automata-Theoretic Approach to L-valued Computation Tree Logic Model Checking,” Chinese Journal of Electronics, vol. 28, no. 2, pp. 309-315, 2019, doi: 10.1049/cje.2019.01.014

Citation:

WEI Xiujuan and LI Yongming, “An Automata-Theoretic Approach to L-valued Computation Tree Logic Model Checking,” Chinese Journal of Electronics, vol. 28, no. 2, pp. 309-315, 2019, doi: 10.1049/cje.2019.01.014

Citation:

PDF( 698 KB)

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

doi: 10.1049/cje.2019.01.014

WEI Xiujuan¹,
LI Yongming^{1,2
,}

1.
College of Mathematic and Information Science, Shaanxi Normal University, Xi'an 710119, China;
2.
College of Computer Science, Shaanxi Normal University, Xi'an 710119, China

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

Abstract

Abstract

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.
- L-valued computation tree logics,
- L-valued alternating Büchi tree automata,
- L-valued positive Boolean formulas,
- Dual operation

FullText(HTML)

References(27)

References

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.

Relative Articles

Supplements(0)

Cited By

Proportional views