Introduction

This tool is for model checking probabilistic multiagent systems with respect to the probabilistic epistemic logic PETL, which can specify both temporal and epistemic properties. We consider memoryless uniform schedulers in this problem, and the basic idea is to reduce the model checking problem into a mixed integer non-linear programming problem, which can then be solved by using an SMT solver. For more information, please check this IJCAI paper.

How to install and use

This tool is implemented as a plugin in ePMC. The source code can be found on GitHub. All the implementation details related to PETL model checking are under epmc-petl/plugins/propertysolver-petl. And you can find the experiment files used in the paper under experiment_files. For building, running and other information about ePMC, please visit its GitHub page.

To perform PETL model checking, please set the following options:

--property-solver propositional-explicit,operator-explicit,pctl-explicit-next,petl-explicit-knowledge,pctl-explicit-until-uniform
--prism-flatten false
--model-input-type mas
--property-input-type petl
--smtlib-command-line z3 -smt2 {0} 
--smtlib-version v25 
--constraintsolver-solver smt-lib 
--model-input-files /path/to/your-model /path/to/your-equivalence-relation 
--property-input-files /path/to/your-property

You need to prepare 3 files: one for the model, one for equivalence relations, and one for properties.

The models should be in the PRISM format. Note that we redefine the composition of the modules to make the agents all take one local action in each transition, so the transitions from different modules will not synchronize according to the parallel composition operator.

The equivalence relations are described in this format:

equiv agent1
-- formula1;
-- formula2;
......
equiv end
equiv agent2
-- formula1;
-- formula2;
......
equiv end
......
......

Each agent in the model has a “equiv (agent name) … equiv end” block, and each block contains a set of formulas. You can use the variables used in the model. All the states satisfying the same formula are regarded as equivalent by the agent. So you can not write formulas such that one state satisfies two or more formulas. If one state can not satisfy any formula, it’s not equivalent to any other states.

The knowledge properties are described like this:

K {agent}  (state_formula)
E/C/D {agent1,..., agentn}  (state_formula)

Other properties can be described by the PRISM language.

Contact

Comments and feedback about any this project are very welcome. Please contact: Chen Fu