EPMC Gets Knowledge in Multi-Agent Systems

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 or Workshop Item (Unspecified)
Divisions:	Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science
Depositing User:	Symplectic Admin
Date Deposited:	18 Nov 2021 08:47
Last Modified:	11 Oct 2023 17:30
DOI:	10.1007/978-3-030-94583-1_5
Related URLs:	Author Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3143384