XU Weifeng, LIU Shufen, WANG Xiaoyan. Quantitative Verification of Knowledge Precondition for Open System[J]. Chinese Journal of Electronics, 2016, 25(2): 227-233. doi: 10.1049/cje.2016.03.006
Citation: XU Weifeng, LIU Shufen, WANG Xiaoyan. Quantitative Verification of Knowledge Precondition for Open System[J]. Chinese Journal of Electronics, 2016, 25(2): 227-233. doi: 10.1049/cje.2016.03.006

Quantitative Verification of Knowledge Precondition for Open System

doi: 10.1049/cje.2016.03.006
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
  • 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 Kaφ, EAsφ and CAsφ as atomic propositions. We study a train controller using PRISM-games to demonstrate the applicability of above quantitative verification method.
  • loading
  • 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.
  • 加载中


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

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

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

    Article Metrics

    Article views (212) PDF downloads(524) Cited by()
    Proportional views


    DownLoad:  Full-Size Img  PowerPoint