Model checking probabilistic epistemic logic for probabilistic multiagent systems

Publication Type:
Conference Proceeding
IJCAI International Joint Conference on Artificial Intelligence, 2018, 2018-July pp. 4757 - 4763
Issue Date:
Full metadata record
© 2018 International Joint Conferences on Artificial Intelligence.All right reserved. 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.
Please use this identifier to cite or link to this item: