Quantitative Verification of Knowledge Precondition for Open System  

作　　者：XU Weifeng LIU Shufen WANG Xiaoyan 

机构地区：[1]College of Computer Science and Technology,Jilin University

出　　处：《Chinese Journal of Electronics》2016年第2期227-233,共7页电子学报（英文版）

基　　金：supported by the National Natural Science Foundation of China(No.60973041)

摘　　要：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 φ, EA sφ and CA sφ as atomic propositions. We study a train controller using PRISM-games to demonstrate the applicability of above quantitative verification method.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 φ, EA sφ and CA sφ 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 

分 类 号：O225[理学—运筹学与控制论]