Skip to main content.

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:

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

ProbDiVinE-1.0:

Download

The latest release of ProbDiVinE and install instructions can be found at DiVinE download page.