Quantitative model checking of knowledge

Wei Wan; Jamal Bentahar; Abdessamad Ben Hamza

doi:10.3233/978-1-61499-125-0-91

Quantitative model checking of knowledge

Wei Wan, Jamal Bentahar, Abdessamad Ben Hamza

Electrical Engineering

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

6 Scopus citations

Abstract

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 language	British English
Title of host publication	New Trends in Software Methodologies, Tools and Techniques
Pages	91-107
Number of pages	17
DOIs	https://doi.org/10.3233/978-1-61499-125-0-91
State	Published - 2012

Publication series

Name	Frontiers in Artificial Intelligence and Applications
Volume	246
ISSN (Print)	0922-6389

Keywords

Interpreted Systems
Markov Chains
Model Checking
Probabilistic and Epistemic Logic

Access to Document

10.3233/978-1-61499-125-0-91

Cite this

@inproceedings{3b56975dd2a64a02ad80317114acc32d,

title = "Quantitative model checking of knowledge",

abstract = "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.",

keywords = "Interpreted Systems, Markov Chains, Model Checking, Probabilistic and Epistemic Logic",

author = "Wei Wan and Jamal Bentahar and {Ben Hamza}, Abdessamad",

year = "2012",

doi = "10.3233/978-1-61499-125-0-91",

language = "British English",

isbn = "9781614991243",

series = "Frontiers in Artificial Intelligence and Applications",

pages = "91--107",

booktitle = "New Trends in Software Methodologies, Tools and Techniques",

}

TY - GEN

T1 - Quantitative model checking of knowledge

AU - Wan, Wei

AU - Bentahar, Jamal

AU - Ben Hamza, Abdessamad

PY - 2012

Y1 - 2012

N2 - 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.

AB - 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.

KW - Interpreted Systems

KW - Markov Chains

KW - Model Checking

KW - Probabilistic and Epistemic Logic

UR - http://www.scopus.com/inward/record.url?scp=84873125009&partnerID=8YFLogxK

U2 - 10.3233/978-1-61499-125-0-91

DO - 10.3233/978-1-61499-125-0-91

M3 - Conference contribution

AN - SCOPUS:84873125009

SN - 9781614991243

T3 - Frontiers in Artificial Intelligence and Applications

SP - 91

EP - 107

BT - New Trends in Software Methodologies, Tools and Techniques

ER -

Quantitative model checking of knowledge

Abstract

Publication series

Keywords

Access to Document

Other files and links

Fingerprint

Cite this