Quantitative Verification of Knowledge Precondition for Open System

XU Weifeng; LIU Shufen; WANG Xiaoyan

doi:10.1049/cje.2016.03.006

Volume 25 Issue 2

Turn off MathJax

Article Contents

Article Navigation > Chinese Journal of Electronics > 2016 > 25(2): 227-233

XU Weifeng, LIU Shufen, WANG Xiaoyan, “Quantitative Verification of Knowledge Precondition for Open System,” Chinese Journal of Electronics, vol. 25, no. 2, pp. 227-233, 2016, doi: 10.1049/cje.2016.03.006

Citation:

XU Weifeng, LIU Shufen, WANG Xiaoyan, “Quantitative Verification of Knowledge Precondition for Open System,” Chinese Journal of Electronics, vol. 25, no. 2, pp. 227-233, 2016, doi: 10.1049/cje.2016.03.006

Citation:

PDF( 430 KB)

Quantitative Verification of Knowledge Precondition for Open System

doi: 10.1049/cje.2016.03.006

College of Computer Science and Technology, Jilin University, Changchun 130012, China

Funds: This work is supported by the National Natural Science Foundation of China (No.60973041).

More Information

Corresponding author: WANG Xiaoyan (corresponding author) was born in Jilin Province, China, in 1977. She received her Ph.D. degree from Jilin University in 2008 in computer science and technology. Currently she is a lecturer of college of computer science and technology in Jilin University. Her research interests include MDA technology, network management technology and cloud computing (Email:wangxy@jlu.edu.cn)
Received Date: 2014-04-01
Rev Recd Date: 2014-05-27
Publish Date: 2016-03-10

Abstract

Abstract

A quantitative verification method is proposed to quantitatively verify knowledge precondition of actions and plans. Probability epistemic game structure (PEGS) is proposed to model knowledge preconditions in open systems, an extension of concurrent game structure with probabilistic transition. We introduce a probability operator P_-λ into Alternating temporal epistemic logic (ATEL) and define a Probability alternating-time temporal epistemic logic (PATEL) for quantitatively model checking the properties of PEGS. We designed an algorithm to compute the probability aiming at model checking verification problems of PATEL based on DTMC and CTMC. We convert a portion of the PATEL verification problems into PATL problems by defining the knowledge formulas K_aφ, E_Asφ and C_Asφ as atomic propositions. We study a train controller using PRISM-games to demonstrate the applicability of above quantitative verification method.
- Quantitative verification,
- Knowledge precondition,
- Alternating-time temporal logic (ATL),
- Open system

FullText(HTML)

References(19)

References

Kwiatkowska Marta, "From software verification to ‘everyware’ verification", Computer Science-Research and Development, Springer, Vol.28, No.4, pp.295-310, 2013.

Michael Huth and Mark Ryan, Logic in Computer Science: Modelling and Reasoning about Systems, China Machine Press, Beijing, China, 2005.

E.M. Clarke, O. Grumberg and D.A. Peled, Model Checking, MIT press, Cambridge, MA, USA, 1999.

TIAN Cong, LIU Shaoying, et al., "Test case generation from conjunctions of predicates with model checking", Chinese Journal of Electronics, Vol.23, No.2, pp.271-277, 2014.

XIAO Meihua, JIANG Yun and LIU Qiaowei, "On formal analysis of cryptographic protocolsand supporting tool", Chinese Journal of Electronics, Vol.19, No.2, pp.223-228, 2010.

H. Hansson and B. Jonsson, "A logic for reasoning about time and reliability", Formal Aspects of Computing, Vol.6, No.5, pp.512-535, 1994.

T.A. Henzinger, X. Nicollin and J. Sifakis, "Symbolic model checking for real-time systems", Proc. of the 7th Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, CA, USA, pp.394-406, 1992.

T. Chen and Kwiatkowska Marta, "Synthesis for multi-objective stochastic games: an application to autonomous urban driving", Proc. of the 10th International Conference on Quantitative Evaluation of SysTems (QEST 2013), Buenos Aires, Argentina, LNCS, Vol.8054, pp.322-337, 2013.

T. Chen, et al., "On stochastic games with multiple objectives", Proc. of the 38th International Symposium on Mathematical Foundations of Computer Science (MFCS'13), Klosterneuburg, Austria, LNCS, Vol.8087, pp.266-277, 2013.

Frits Dannenberg, Marta Kwiatkowska, et al., "DNA walker circuits: Computational potential, design, and verification", Proc. of the 19th International Conference on DNA Computing and Molecular Programming (DNA 2013), Tempe, AZ, USA, LNCS, Vol.8141, pp.31-45, 2013.

James F. Allen, "Planning as temporal reasoning", Proc. of the Second International Conf. on Principles of Knowledge Representation and Reasoning, Cambridge, MA, USA, pp.3-14, 1991.

W. Wan, J. Bentahar and Hamza A. Ben, "Model checking epistemic-probabilistic logic using probabilistic interpreted systems", Knowledge-Based Systems, Vol.50, pp.279-295, 2013.

R. Alur, et al., "Alternating-time temporal logic", Journal of the ACM (JACM), Vol.49, No.5, pp.672-713, 2002.

Van der Hoek W and M. Wooldridge, "Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications", Studia Logica, Vol.75, No.1, pp.125-157, 2003.

M. Kwiatkowska, G. Norman and J. Sproston, "Symbolic model checking for probabilistic timed automata", Information and Computation, Vol.205, No.7, pp.1027-1077, 2007.

C. Delgado and M. Benevides, "Verification of epistemic properties in probabilistic multi-agent systems", Proc. of the 7th German Conference on Multiagent System Technologies (MATES 2009), Hamburg, Germany, LNCS, Vol.5774, pp.16-28, 2009.

T. Brázdil, V. Forejt, J. Kr?ál, J. K?etínský and A. Ku?era, "Continuous-time stochastic games with time-bounded reachability", Information & Computation, Vol.224, pp.46-70, 2013.

T. Chen, V. Forejt and M. Kwiatkowska, "PRISM-games: A model checker for stochastic multi-player games", Proc. of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013), Rome, Italy, LNCS, Vol.7795, pp.185-191, 2013.

T. Chen and Kwiatkowska Marta, "Automatic verification of competitive stochastic systems", Formal Methods in System Design, Vol.43, No.1, pp.61-92, 2013.

Relative Articles

Supplements(0)

Cited By

Proportional views