Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems
Authors: Chen Fu, Andrea Turrini, Xiaowei Huang, Lei Song, Yuan Feng, Lijun Zhang
IJCAI 2018 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | The algorithm has been implemented in an existing model checker and experiments are conducted on examples from the IPPC competitions. The experimental results show the scalability of our symbolic algorithm in handling interesting problems. |
| Researcher Affiliation | Collaboration | 1 State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences 2 University of Chinese Academy of Sciences 3 Department of Computer Science, University of Liverpool 4 JD.com 5 Centre for Quantum Software and Information, University of Technology Sydney |
| Pseudocode | Yes | Algorithm 1 Procedure to compute the set of states satisfying a PETL formula ϕ |
| Open Source Code | Yes | The source code of our implementation is available at https://github.com/fuchen1991/epmc-petl. |
| Open Datasets | Yes | The models we use for our experiments are taken from the IPPC competitions held in 2011 and 2014, and the original IPPC domain decription of these models can be found at https://github.com/ssanner/rddlsim. |
| Dataset Splits | No | The paper uses models from IPPC competitions but does not explicitly provide details about training, validation, or test dataset splits. |
| Hardware Specification | Yes | All experiments were conducted on a 3.40GHz Intel Core i7-2600 CPU with 8GB of memory. |
| Software Dependencies | Yes | In our implementation, we use the SMT solver Z3 [de Moura and Bjørner, 2008] (version 4.6.0) to solve the MINLP problem. |
| Experiment Setup | Yes | The models we use for our experiments are taken from the IPPC competitions held in 2011 and 2014... In our implementation, we use the SMT solver Z3 [de Moura and Bjørner, 2008] (version 4.6.0) to solve the MINLP problem. In this model, there are several robots moving in a grid... We have 2 robots; we varied the size of the grid by changing the number of rows and columns... consider Φ3 = Pr max[G(rw x = rc x rw y = rc y)] and Φ4 = Pr max[GErw,rc(rw x = rc x rw y = rc y)] which ask for the maximal probability of the two robots always (knowing of) being on different cells, respectively. |