Modeling and verifying probabilistic Multi-Agent Systems using knowledge and social commitments

Khalid Sultan, Jamal Bentahar, Wei Wan, Faisal Al-Saqqar

Research output: Contribution to journalArticlepeer-review

11 Scopus citations


Multi-Agent Systems (MASs) have long been modeled through knowledge and social commitments independently. In this paper, we present a new method that merges the two concepts to model and verify MASs in the presence of uncertainty. To express knowledge and social commitments simultaneously in uncertain settings, we define a new multi-modal logic called Probabilistic Computation Tree Logic of Knowledge and Commitments (PCTLkc in short) which combines two existing probabilistic logics namely, probabilistic logic of knowledge PCTLK and probabilistic logic of commitments PCTLC. To model stochastic MASs, we present a new version of interpreted systems that captures the probabilistic behavior and accounts for the communication between interacting components. Then, we introduce a new probabilistic model checking procedure to check the compliance of target systems against some desirable properties written in PCTLkc and report the obtained verification results. Our proposed model checking technique is reduction-based and consists in transforming the problem of model checking PCTLkc into the problem of model checking a well established logic, namely PCTL. So doing provides us with the privilege of re-using the PRISM model checker to implement the proposed model checking approach. Finally, we demonstrate the effectiveness of our approach by presenting a real case study. This framework can be considered as a step forward towards closing the gap of capturing interactions between knowledge and social commitments in stochastic agent-based systems.

Original languageBritish English
Pages (from-to)6291-6304
Number of pages14
JournalExpert Systems with Applications
Issue number14
StatePublished - 15 Oct 2014


  • Interpreted systems
  • Knowledge
  • Modal logic
  • Multi-Agent Systems
  • Probabilistic model checking
  • Social commitments
  • Verification


Dive into the research topics of 'Modeling and verifying probabilistic Multi-Agent Systems using knowledge and social commitments'. Together they form a unique fingerprint.

Cite this