Quantitative model checking of knowledge

Wei Wan, Jamal Bentahar, Abdessamad Ben Hamza

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

6 Scopus citations


Model checking, a formal and automatic verification method, has been widely used to check specifications expressed not only as qualitative properties (e.g safety and liveliness), but also as quantitative properties (e.g. degree of reliability and reachability). In this paper, we present a method for probabilistic model checking of multi-agent systems specified by a probabilistic-epistemic logic PCTLK. We define transformations from probabilistic interpreted systems into Discrete-time Markov chains (DTMC) and from PCTLK formulae to PCTL formulae so that we are able to convert the problem of model checking PCTLK to the one of PCTL. The algorithm is implemented in the probabilistic model checker PRISM. Some properties, including agents' probabilistic knowledge, are verified and simulations are shown.

Original languageBritish English
Title of host publicationNew Trends in Software Methodologies, Tools and Techniques
Number of pages17
StatePublished - 2012

Publication series

NameFrontiers in Artificial Intelligence and Applications
ISSN (Print)0922-6389


  • Interpreted Systems
  • Markov Chains
  • Model Checking
  • Probabilistic and Epistemic Logic


Dive into the research topics of 'Quantitative model checking of knowledge'. Together they form a unique fingerprint.

Cite this