Fu, Chen, Hahn, Ernst-Moritz, Li, Yong
ORCID: 0000-0002-7301-9234, Schewe, Sven
ORCID: 0000-0002-9093-9518, Sun, Meng, Turrini, Andreas and Zhang, Lijun
(2022)
EPMC Gets Knowledge in Multi-Agent Systems
In: International Conference on Verification, Model Checking, and Abstract Interpretation.
|
Text
paper_30.pdf - Author Accepted Manuscript Download (841kB) | Preview |
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.
| Item Type: | Conference Item (Unspecified) |
|---|---|
| Uncontrolled Keywords: | 4605 Data Management and Data Science, 46 Information and Computing Sciences, 4602 Artificial Intelligence |
| Divisions: | Faculty of Science & Engineering > School of Electrical Engineering, Electronics and Computer Science |
| Depositing User: | Symplectic Admin |
| Date Deposited: | 18 Nov 2021 08:47 |
| Last Modified: | 01 Mar 2026 04:30 |
| DOI: | 10.1007/978-3-030-94583-1_5 |
| Related Websites: | |
| URI: | https://livrepository.liverpool.ac.uk/id/eprint/3143384 |
| Disclaimer: | The University of Liverpool is not responsible for content contained on other websites from links within repository metadata. Please contact us if you notice anything that appears incorrect or inappropriate. |
Altmetric
Altmetric