Abstract

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 analysed in the literature. However, systems also have 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 dissertation, we analyse 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 multiagent systems distributed knowledge bases using probabilistic interpreted systems. We also 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. We address the problem of verifying probabilistic properties
and epistemic properties in concurrent probabilistic systems as well. We then prove that model checking a formula of PCTLK in concurrent probabilistic systems is
PSPACE-complete. Furthermore, we represent models associated with PCTLK logic symbolically with Multi-Terminal Binary Decision Diagrams (MTBDDs).

Finally, we make use of PRISM, the model checker of PCTL without adding new computation cost. Dining cryptographers protocol is implemented to show the
applicability of the proposed technique along with performance analysis and comparison in terms of execution time and state space scalability with MCK, an existing
epistemic-probabilistic model checker, and MCMAS, a model checker for multi-agent systems. Another example, NetBill protocol, is also implemented with PRISM to verify probabilistic epistemic properties and to evaluate the complexity of this verification.