Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems



Fu, Chen, Turrini, Andrea, Huang, Xiaowei ORCID: 0000-0001-6267-0366, Song, Lei, Feng, Yuan and Zhang, Lijun
(2018) Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems. In: Twenty-Seventh International Joint Conference on Artificial Intelligence {IJCAI-18}, 2018-7-13 - 2018-7-19, Stockholm, Sweden.

[img] Text
0661.pdf - Published version

Download (209kB)

Abstract

<jats:p>In this work we study the model checking problem for probabilistic multiagent systems with respect to the probabilistic epistemic logic PETL, which can specify both temporal and epistemic properties. We show that under the realistic assumption of uniform schedulers, i.e., the choice of every agent depends only on its observation history, PETL model checking is undecidable. By restricting the class of schedulers to be memoryless schedulers, we show that the problem becomes decidable. More importantly, we design a novel algorithm which reduces the model checking problem into a mixed integer non-linear programming problem, which can then be solved by using an SMT solver. The algorithm has been implemented in an existing model checker and experiments are conducted on examples from the IPPC competitions.</jats:p>

Item Type: Conference or Workshop Item (Unspecified)
Depositing User: Symplectic Admin
Date Deposited: 09 Jan 2019 10:13
Last Modified: 19 Jan 2023 01:07
DOI: 10.24963/ijcai.2018/661
Related URLs:
URI: https://livrepository.liverpool.ac.uk/id/eprint/3031029