Login | Register

Probabilistic and Epistemic Model Checking for Multi-Agent Systems


Probabilistic and Epistemic Model Checking for Multi-Agent Systems

Wan, Wei (2014) Probabilistic and Epistemic Model Checking for Multi-Agent Systems. PhD thesis, Concordia University.

[thumbnail of Wan_PhD_S2015.pdf]
Text (application/pdf)
Wan_PhD_S2015.pdf - Accepted Version


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.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (PhD)
Authors:Wan, Wei
Institution:Concordia University
Degree Name:Ph. D.
Program:Electrical and Computer Engineering
Date:19 December 2014
Thesis Supervisor(s):Bentahar, Jamal and Ben Hamza, Abdessamad
ID Code:980081
Deposited By: WEI WAN
Deposited On:16 Jul 2015 12:58
Last Modified:18 Jan 2018 17:50
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top