Quantitative Verification of Knowledge Precondition for Open System

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.