PRISM Connect bundle
PRISM
is a probabilistic model checker, a tool for formal modelling and analysis of systems which exhibit random or probabilistic behaviour. In this bundle, we implemented two new model checking techniques on top of PRISM for the CONNECT project:
- A multi-objective model checking framework, which is the underlying technique used by the assume-guarantee reasoning methods presented in our TACAS'10 paper and TACAS'11 paper. In this framework, an objective can be a probabilistic LTL formula or a total reward formula. A property with multiple objectives holds in a Markov Decision Process (MDP) if an adversary satisfying all objectives can be found.
- SCC-based quantitative verification, which speeds up probabilistic model checking and provides a basis for quantitative incremental verification presented in the deliverable D5.2. Currently, this technique can be used to compute maximum/minimum probability/expected reward of reaching a set of target states.
Installation
- Linux x86_64 platform: run the command "make" to compile and install the bundle.
- Other platform: download the corresponding version of lp_solve (http://lpsolve.sourceforge.net/5.5/)
and copy the header files to the directory "include" and copy liblpsolve55.so to the directory "lib"; then run the command "make" as above.
Usage
- Multi-objective verification: multi-objective properties are in the format of "multi[p1, ..., pn]", where each objective p in {p1, ..., pn} can be either an LTL property or a total reward property.
- SCC-based verification: specify option "-m" in the command line.
Examples are located in the directoties examples/multi-objectives and
examples/incremental in the package. The general usage of PRISM can be found here.
Download
