ProbDiVinE
A Parallel Qualitative and Quantitative LTL Model Checker
ProbDiVinE-MC is an extensible open source system for parallel and/or distributed formal verification of concurrent probabilistic systems. ProbDiVinE-MC is an integral part of the distributed verification tool DiVinE and as such can be viewed both as an analyser and prototyping environment.
ProbDiVinE-MC supports both qualitative and quantitative LTL model checking of Markov Decision Processes (MDPs) -- models supporting both probability and non-determinism expressed in PROBDVE language (see section "Usage"). Current version works in shared memory environment.
The main difference in comparison to previous version (see section download) is that ProbDiVinE-MC supports also quantitative verification and does not require distributed memory environment.
ProbDiVinE-MC uses the automata-theoretic approach where qualitative LTL model checking of MDPs is reduced to the question whether the product automaton for a given MDP with a Buchi acceptance condition contains an accepting end component (AEC). The problem of quantitative LTL model checking is to determine minimal or maximal probability the formula is satisfied, i.e. we try to find minimal or maximal probability an AEC is reachable from initial state, which is done via building and solving linear programming problem.
The tool implements a parallel adaptations of the algorithm of de Alfaro [dA95]. It computes the set of states, from which probability of reaching accepting end component is 1. In particular, the algorithm maintains approximation set of states that may belong to an AEC or probability of reaching AEC from them is 1. The algorithm repeatedly refines the approximation set by locating and removing states from which AEC cannot be reached with probability 1, we call this a pruning step. The core of the algorithm are conditions determining the states to prune.
After determinig states with probability 1, linear programming problem is built and solved. Size of LP problem is crucial, thus several parallel optimization techniques to reduce number of inequations were developed and implemented. The techniques:
- prune the graph, from which inequations are generated
- allow to divide LP problem to a sequence of LP subproblems via parallel decomposition into strongly connected component (SCC) graph
- allow to solve some LP subproblems corresponding to SCCs, independently or at least iteratively (in parallel)
ProbDiVinE-MC is built on the top of the DiVinE library that offers common functions needed to develop a parallel or distributed enumerative model checker. The only extension to the library that was necessary, was the extension of the state generator to a probabilistic state generator, hence, it can handle probabilistic transitions of PROBDVE as introduced in section "Usage".
ProbDiVinE-MC is currently operated in command-line mode. The input is the model given as a .probdve file and the LTL formula given as an .ltl file. Further parameters include type of verification, number of threads involved in the computation etc. See section "Usage" .
Using the tool
- Before using the tool, make sure your PATH environment
variable contains paths to both DiVinE and ProbDiVinE
binaries.
export PATH=:path_to_probdivine:path_to_divine
- Write your model in a PROBDVE language and store it in a file with extension .probdve.
PROBDVE is a slightly modified DVE specification language as used in DiVinE. A system is modeled as a composition of processes, which can change their states via probabilistic (=>) or non-probabilistic (->) transitions and can synchronize using channels. A non-probabilistic transition may have a guard (a condition which has to be satisfied for the transition to be enabled), an effect (assignment to a variable), and a sync expression (for synchronization with another transition via channel). A probabilistic transition just determines probability of resulting state, which is given by weights assigned to states. For example, s=>{s:3, t:2, u:2} means that from the state s the system evolves in the state s with probability 3/7, in the state t with probability 2/7, as well as in the state u.
- Express the properties you want to verify and store them in a file with extension .ltl.
Rules for writing .ltl files are as follows.- Only lines starting with # are processed, the rest is ignored.
- Atomic propositions are specified using the standard keyword #define, e.g.:
#define hungry (hungry==1)
- Individual properties are specified using keyword #property , e.g.:
#property GF(hungry)
- More LTL properties can be specified in a single file.
- Syntax of an LTL formula is given by the following rule. All temporal operators follow the standard semantics.
f ::= !f | Xf | Ff | Gf | fUf | fVf | f&&f | f||f | f->f | a | true | false
- Important! Combine your model file with the ltl file using
divine.combine script to produce models with LTL specification and use -d to obtain a product with semi-deterministic Buchi automaton. Only these can be used as input files to the probabilistic model
checker. Tools(algorithms) will not work on models that contain no LTL
specification or property process.
divine.combine -d model.probdve specification.ltl
This will produce as many files as there are properties in specification.ltl. Newly created files will be named
model.prop1.probdve
model.prop2.probdve
model.prop3.probdve
...
- Run the algorithm to verify the model. NNN
stands for the number of threads required to perform the
computation. In case of quantitative verification, we
obtain minimal probability the formula holds:
divine-mc.probabilistic -n NNN -t model.prop1.probdve
If you run qualitative verification only, the algorithm outputs whether the LTL formula is satisfied with probability one or not.divine-mc.probabilistic -n NNN -l model.prop1.probdve
ProbDiVinE-MC:
ProbDiVinE-1.0:
- Run any of the algortihms to detect the presence of AEC. If
an AEC is present in the state space graph, the verifed
property does not hold true with probability one. The presence
of AEC is reported by the algorithms to the standard output.
Algorithm probdivine.AECdetection is an MPI application and must be executed with appropriate way. The particular ways differ according to individual implementations of MPI standard. The following sequences of commands relate to the two most used MPI implementations: mpich and LAM/MPI. Note that NNN stands for the number of network nodes required to perform the computation.mpich:
mpirun -np NNN probdivine.AECdetection model.prop1.probdveLAM/MPI:
Algorithms probdivine.CY and probdivine.CY_eliminate are standard serial algorithms that are executed outside MPI environment.
lamboot
mpirun -np NNN probdivine.AECdetection model.prop1.probdve
lamhalt
probdivine.CY model.prop1.probdve
Download
The latest release of ProbDiVinE and install instructions can be found at DiVinE download page.