Verifying concurrent probabilistic systems using probabilistic-epistemic logic specifications

Wei Wan, Jamal Bentahar, Hamdi Yahyaoui, Abdessamad Ben Hamza

Research output: Contribution to journalArticlepeer-review

2 Scopus citations

Abstract

In this paper, we address the problem of verifying probabilistic and epistemic properties in concurrent probabilistic systems expressed in PCTLK. PCTLK is an extension of the Probabilistic Computation Tree Logic (PCTL) augmented with Knowledge (K). In fact, PCTLK enjoys two epistemic modalities Ki for knowledge and Pr bKi for probabilistic knowledge. The approach presented for verifying PCTLK specifications in such concurrent systems is based on a transformation technique. More precisely, we convert PCTLK model checking into the problem of model checking Probabilistic Branching Time Logic (PBTL), which enjoys path quantifiers in the range of adversaries. We then prove that model checking a formula of PCTLK in concurrent probabilistic programs is PSPACE-complete. Furthermore, we represent models associated with PCTLK logic symbolically with Multi-Terminal Binary Decision Diagrams (MTBDDs), which are supported by the probabilistic model checker PRISM. Finally, an application, namely the NetBill online shopping payment protocol, and an example about synchronization illustrated through the dining philosophers problem are implemented with the MTBDD engine of this model checker to verify probabilistic epistemic properties and evaluate the practical complexity of this verification.

Original languageBritish English
Pages (from-to)747-776
Number of pages30
JournalApplied Intelligence
Volume45
Issue number3
DOIs
StatePublished - 1 Oct 2016

Keywords

  • Concurrent probabilistic systems
  • Model checking
  • Multi-agent systems
  • Verification

Fingerprint

Dive into the research topics of 'Verifying concurrent probabilistic systems using probabilistic-epistemic logic specifications'. Together they form a unique fingerprint.

Cite this