Model checking probabilistic epistemic logic for probabilistic multiagent systems

Fu, C; Turrini, A; Huang, X; Song, L; Feng, Y; Zhang, L

Model checking probabilistic epistemic logic for probabilistic multiagent systems

Fu, C Turrini, A Huang, X Song, L Feng, Y

Zhang, L

Permalink

Publication Type:: Conference Proceeding
Citation:: IJCAI International Joint Conference on Artificial Intelligence, 2018, 2018-July pp. 4757 - 4763
Issue Date:: 2018-01-01

Open Access

Copyright Clearance Process

Recently Added
In Progress
Open Access

This item is open access.

Adobe PDF

Download Published versionAdobe PDF (162.87 kB)

View statistics

Full metadata record

Field	Value	Language
dc.contributor.author	Fu, C	en_US
dc.contributor.author	Turrini, A	en_US
dc.contributor.author	Huang, X	en_US
dc.contributor.author	Song, L	en_US
dc.contributor.author	Feng, Y https://orcid.org/0000-0002-3097-3896	en_US
dc.contributor.author	Zhang, L	en_US
dc.date.issued	2018-01-01	en_US
dc.identifier.citation	IJCAI International Joint Conference on Artificial Intelligence, 2018, 2018-July pp. 4757 - 4763	en_US
dc.identifier.isbn	9780999241127	en_US
dc.identifier.issn	1045-0823	en_US
dc.identifier.uri	http://hdl.handle.net/10453/134188
dc.description.abstract	© 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.	en_US
dc.relation	http://purl.org/au-research/grants/arc/DP130102764
dc.relation	http://purl.org/au-research/grants/arc/DP160101652
dc.relation.ispartof	IJCAI International Joint Conference on Artificial Intelligence	en_US
dc.title	Model checking probabilistic epistemic logic for probabilistic multiagent systems	en_US
dc.type	Conference Proceeding
utslib.citation.volume	2018-July	en_US
utslib.for	0801 Artificial Intelligence and Image Processing	en_US
pubs.embargo.period	Not known	en_US
pubs.organisational-group	/University of Technology Sydney
pubs.organisational-group	/University of Technology Sydney/Faculty of Engineering and Information Technology
pubs.organisational-group	/University of Technology Sydney/Strength - QSI - Centre for Quantum Software and Information
utslib.copyright.status	open_access
pubs.publication-status	Published	en_US
pubs.volume	2018-July	en_US

Abstract:

© 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:

http://hdl.handle.net/10453/134188