Model checking epistemic-probabilistic logic using probabilistic interpreted systems

Model checking is a formal technique widely used to verify security and communication protocols in epistemic multi-agent systems against given properties. Qualitative properties such as safety and liveliness have been widely analyzed in the literature. However, systems have also quantitative and uncertain (i.e., probabilistic) properties such as degree of reliability and reachability, which still need further attention from the model checking perspective. In this paper, we analyze such properties and present a new method for probabilistic model checking of epistemic multi-agent systems specified by a new probabilistic-epistemic logic PCTLK. We model multi-agent systems as distributed knowledge bases using probabilistic interpreted systems and define transformations from those interpreted systems into discrete-time Markov chains and from PCTLK formulae to PCTL formulae, an existing extension of CTL with probabilities. By so doing, we are able to convert the PCTLK model checking problem into the PCTL one. Thus, we make use of PRISM, the model checker of PCTL without adding new computation cost. A concrete case study has been implemented to show the applicability of the proposed technique along with performance analysis and comparison with MCK, an epistemic-probabilistic model checker, and MCMAS, a model checker for multi-agent systems, in terms of execution time and state space scalability.