{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,7]],"date-time":"2024-08-07T07:38:13Z","timestamp":1723016293692},"publisher-location":"California","reference-count":0,"publisher":"International Joint Conferences on Artificial Intelligence Organization","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,7]]},"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>","DOI":"10.24963\/ijcai.2018\/661","type":"proceedings-article","created":{"date-parts":[[2018,7,5]],"date-time":"2018-07-05T01:49:10Z","timestamp":1530755350000},"page":"4757-4763","source":"Crossref","is-referenced-by-count":6,"title":["Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems"],"prefix":"10.24963","author":[{"given":"Chen","family":"Fu","sequence":"first","affiliation":[{"name":"State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences"},{"name":"University of Chinese Academy of Sciences"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Turrini","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaowei","family":"Huang","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Liverpool"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lei","family":"Song","sequence":"additional","affiliation":[{"name":"JD.com"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuan","family":"Feng","sequence":"additional","affiliation":[{"name":"Centre for Quantum Software and Information, University of Technology Sydney"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lijun","family":"Zhang","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences"},{"name":"University of Chinese Academy of Sciences"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"10584","event":{"number":"27","sponsor":["International Joint Conferences on Artificial Intelligence Organization (IJCAI)"],"acronym":"IJCAI-2018","name":"Twenty-Seventh International Joint Conference on Artificial Intelligence {IJCAI-18}","start":{"date-parts":[[2018,7,13]]},"theme":"Artificial Intelligence","location":"Stockholm, Sweden","end":{"date-parts":[[2018,7,19]]}},"container-title":["Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence"],"original-title":[],"deposited":{"date-parts":[[2018,7,5]],"date-time":"2018-07-05T01:55:02Z","timestamp":1530755702000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.ijcai.org\/proceedings\/2018\/661"}},"subtitle":[],"proceedings-subject":"Artificial Intelligence Research Articles","short-title":[],"issued":{"date-parts":[[2018,7]]},"references-count":0,"URL":"https:\/\/doi.org\/10.24963\/ijcai.2018\/661","relation":{},"subject":[],"published":{"date-parts":[[2018,7]]}}}