EPMC Gets Knowledge in Multi-agent Systems

Chen Fu; Ernst Moritz Hahn; Yong Li; Sven Schewe; Meng Sun; Andrea Turrini; Lijun Zhang

doi:10.1007/978-3-030-94583-1_5

EPMC Gets Knowledge in Multi-agent Systems

Chen Fu^*
, Ernst Moritz Hahn
, Yong Li
, Sven Schewe
, Meng Sun
, Andrea Turrini
, Lijun Zhang

^*Corresponding author for this work

Formal Methods and Tools

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

6 Citations (Scopus)

298 Downloads (Pure)

Abstract

In this paper, we present EPMC, an extendible probabilistic model checker. EPMC has a small kernel, and is designed modularly. It supports discrete probabilistic models such as Markov chains and Markov decision processes. Like PRISM, it supports properties specified in PCTL*. Two central advantages of EPMC are its modularity and extendibility. We demonstrate these features by extending EPMC to EPMC-PETL, a model checker for probabilistic epistemic properties on multi-agent systems. EPMC-PETL takes advantage of EPMC to provide two model checking algorithms for multi-agent systems with respect to probabilistic epistemic logic: an exact algorithm based on SMT techniques and an approximated one based on UCT. Multi-agent systems and epistemic properties are given in an extension of the modelling language of PRISM, making it easy to model this kind of scenarios.

Original language	English
Title of host publication	Verification, Model Checking, and Abstract Interpretation
Subtitle of host publication	23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16-18, 2022, Proceedings
Editors	Bernd Finkbeiner, Thomas Wies
Publisher	Springer
Pages	93-107
Number of pages	15
ISBN (Electronic)	978-3-030-94583-1
ISBN (Print)	978-3-030-94582-4
DOIs	https://doi.org/10.1007/978-3-030-94583-1_5
Publication status	Published - 2022
Event	23rd International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2022 - Virtual, Philadelphia, United States Duration: 16 Jan 2022 → 18 Jan 2022 Conference number: 23

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	13182

Conference

Conference	23rd International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2022
Abbreviated title	VMCAI 2022
Country/Territory	United States
City	Philadelphia
Period	16/01/22 → 18/01/22

Keywords

2023 OA procedure

Access to Document

10.1007/978-3-030-94583-1_5

ArticleFinal published version, 594 KBLicence: Taverne

EPMC: VMCAI 2022 Artifact
Fu, C. (Creator), Hahn, E. M. (Creator), Li, Y. (Creator), Schewe, S. (Creator), Sun, M. (Creator), Turrini, A. (Creator) & Zhang, L. (Creator), Zenodo, 16 Sept 2021
DOI: 10.5281/zenodo.5512722, https://zenodo.org/record/5512722 and 4 more links, https://doi.org/10.5281/zenodo.5512723, https://zenodo.org/record/5512723, https://doi.org/10.5281/zenodo.5529691, https://zenodo.org/record/5529691 (show fewer)
Dataset

Cite this

Fu, C., Hahn, E. M., Li, Y., Schewe, S., Sun, M., Turrini, A., & Zhang, L. (2022). EPMC Gets Knowledge in Multi-agent Systems. In B. Finkbeiner, & T. Wies (Eds.), Verification, Model Checking, and Abstract Interpretation: 23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16-18, 2022, Proceedings (pp. 93-107). (Lecture Notes in Computer Science; Vol. 13182). Springer. https://doi.org/10.1007/978-3-030-94583-1_5

@inproceedings{830473c7f2bd4820a300a279e50886ea,

title = "EPMC Gets Knowledge in Multi-agent Systems",

abstract = "In this paper, we present EPMC, an extendible probabilistic model checker. EPMC has a small kernel, and is designed modularly. It supports discrete probabilistic models such as Markov chains and Markov decision processes. Like PRISM, it supports properties specified in PCTL*. Two central advantages of EPMC are its modularity and extendibility. We demonstrate these features by extending EPMC to EPMC-PETL, a model checker for probabilistic epistemic properties on multi-agent systems. EPMC-PETL takes advantage of EPMC to provide two model checking algorithms for multi-agent systems with respect to probabilistic epistemic logic: an exact algorithm based on SMT techniques and an approximated one based on UCT. Multi-agent systems and epistemic properties are given in an extension of the modelling language of PRISM, making it easy to model this kind of scenarios.",

keywords = "2023 OA procedure",

author = "Chen Fu and Hahn, \{Ernst Moritz\} and Yong Li and Sven Schewe and Meng Sun and Andrea Turrini and Lijun Zhang",

year = "2022",

doi = "10.1007/978-3-030-94583-1\_5",

language = "English",

isbn = "978-3-030-94582-4",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "93--107",

editor = "Bernd Finkbeiner and Thomas Wies",

booktitle = "Verification, Model Checking, and Abstract Interpretation",

address = "Germany",

note = "23rd International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2022, VMCAI 2022 ; Conference date: 16-01-2022 Through 18-01-2022",

}

Fu, C, Hahn, EM, Li, Y, Schewe, S, Sun, M, Turrini, A & Zhang, L 2022, EPMC Gets Knowledge in Multi-agent Systems. in B Finkbeiner & T Wies (eds), Verification, Model Checking, and Abstract Interpretation: 23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16-18, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13182, Springer, pp. 93-107, 23rd International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2022, Philadelphia, Pennsylvania, United States, 16/01/22. https://doi.org/10.1007/978-3-030-94583-1_5

EPMC Gets Knowledge in Multi-agent Systems. / Fu, Chen; Hahn, Ernst Moritz; Li, Yong et al.
Verification, Model Checking, and Abstract Interpretation: 23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16-18, 2022, Proceedings. ed. / Bernd Finkbeiner; Thomas Wies. Springer, 2022. p. 93-107 (Lecture Notes in Computer Science; Vol. 13182).

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

TY - GEN

T1 - EPMC Gets Knowledge in Multi-agent Systems

AU - Fu, Chen

AU - Hahn, Ernst Moritz

AU - Li, Yong

AU - Schewe, Sven

AU - Sun, Meng

AU - Turrini, Andrea

AU - Zhang, Lijun

N1 - Conference code: 23

PY - 2022

Y1 - 2022

N2 - In this paper, we present EPMC, an extendible probabilistic model checker. EPMC has a small kernel, and is designed modularly. It supports discrete probabilistic models such as Markov chains and Markov decision processes. Like PRISM, it supports properties specified in PCTL*. Two central advantages of EPMC are its modularity and extendibility. We demonstrate these features by extending EPMC to EPMC-PETL, a model checker for probabilistic epistemic properties on multi-agent systems. EPMC-PETL takes advantage of EPMC to provide two model checking algorithms for multi-agent systems with respect to probabilistic epistemic logic: an exact algorithm based on SMT techniques and an approximated one based on UCT. Multi-agent systems and epistemic properties are given in an extension of the modelling language of PRISM, making it easy to model this kind of scenarios.

AB - In this paper, we present EPMC, an extendible probabilistic model checker. EPMC has a small kernel, and is designed modularly. It supports discrete probabilistic models such as Markov chains and Markov decision processes. Like PRISM, it supports properties specified in PCTL*. Two central advantages of EPMC are its modularity and extendibility. We demonstrate these features by extending EPMC to EPMC-PETL, a model checker for probabilistic epistemic properties on multi-agent systems. EPMC-PETL takes advantage of EPMC to provide two model checking algorithms for multi-agent systems with respect to probabilistic epistemic logic: an exact algorithm based on SMT techniques and an approximated one based on UCT. Multi-agent systems and epistemic properties are given in an extension of the modelling language of PRISM, making it easy to model this kind of scenarios.

KW - 2023 OA procedure

U2 - 10.1007/978-3-030-94583-1_5

DO - 10.1007/978-3-030-94583-1_5

M3 - Conference contribution

SN - 978-3-030-94582-4

T3 - Lecture Notes in Computer Science

SP - 93

EP - 107

BT - Verification, Model Checking, and Abstract Interpretation

A2 - Finkbeiner, Bernd

A2 - Wies, Thomas

PB - Springer

T2 - 23rd International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2022

Y2 - 16 January 2022 through 18 January 2022

ER -

Fu C, Hahn EM, Li Y, Schewe S, Sun M, Turrini A et al. EPMC Gets Knowledge in Multi-agent Systems. In Finkbeiner B, Wies T, editors, Verification, Model Checking, and Abstract Interpretation: 23rd International Conference, VMCAI 2022, Philadelphia, PA, USA, January 16-18, 2022, Proceedings. Springer. 2022. p. 93-107. (Lecture Notes in Computer Science). Epub 2022 Jan 14. doi: 10.1007/978-3-030-94583-1_5

EPMC Gets Knowledge in Multi-agent Systems

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Datasets

EPMC: VMCAI 2022 Artifact

Cite this