This tool performs a dead variable analysis on parameterised Boolean equation systems. Dead variables are reset to a constant. The analysis performed in this tool is generally more powerful than the one performed by pbesparelm, but it is also more resource intensive.


\[\begin{split}\begin{array}{l} \nu X(i,j,k,l{:}\mathbb{N}) = (i \neq 1 \lor j \neq 1 \lor X(2,j,k,l+1)) \land \forall m{:}\mathbb{N} . Z(i,2,m+k,k)\\ \mu Y(i,j,k,l{:}\mathbb{N}) = k = 1 \lor (i = 2 \land X(1,j,k,l))\\ \nu Z(i,j,k,l{:}\mathbb{N}) = (k < 10 \lor j = 2) \land (j \neq 2 \lor Y(1,1,l,1)) \land Y(2,2,1,l)\\ ~\\ \mathbf{init}\ X(1,1,1,1) \end{array}\end{split}\]

Instantiation of this PBES using tools such as pbes2bool or pbessolve does not terminate. Also, pbesparelm is only able to remove parameter \(l\) from equations \(X\) and \(Y\), and parameter \(i\) from \(Z\). The presence of the predicate variable instantiations \(X(2,j,k,l+1)\) and \(Z(i,2,m+k,k)\) in \(X\)’s equation means the solution to \(X(1,1,1,1)\) depends on the solutions to \(X(2,1,1,2)\) and \(X(1,2,v+1,1)\) for all values \(v\), so instantiation will not terminate (not even after applying pbesparelm, since parameter \(k\) in the equation for \(Z\) was not removed).

The dead variable analysis will (among others) observe that the third parameter of \(Z\) does not affect the solution when \(j = 2\). The method will observe this, and replace \(Z(i,2,m+k,k)\) by, for example, \(Z(i,2,1,k)\).

The resulting PBES will be:

\[\begin{split}\begin{array}{l} \nu X(i,j,k,l{:}\mathbb{N}) = (i \neq 1 \lor j \neq 1 \lor X(2,j,k,1)) \land \forall m{:}\mathbb{N} . Z(0,2,0,k)\\ \mu Y(i,j,k,l{:}\mathbb{N}) = k = 1 \lor (i = 2 \land X(1,j,k,1))\\ \nu Z(i,j,k,l{:}\mathbb{N}) = (k < 10 \lor j = 2) \land (j \neq 2 \lor Y(1,1,l,0)) \land Y(2,2,1,0)\\ ~\\ \mathbf{init}\ X(1,1,1,1) \end{array}\end{split}\]

To perform the dead variable analysis, the algorithm computes a set of control flow variables. By default, local control flow graphs are constructed in order to avoid a combinatorial explosion of the control flow graph. The option -g/–use-global-variant uses a global control flow graph instead. The latter option may be able to detect more dead variables, but may use (much) more memory.

The algorithm underlying the tool, including the detection of control flow variables and the construction of local and global control flow graphs, is described in detail in [KWW14].



pbesstategraph   [OPTION]... [INFILE [OUTFILE]]


Reads a file containing a PBES, and reduces it based on an analysis of control flow parameters.If OUTFILE is not present, standard output is used. If INFILE is not present, standard input is used.

Command line options


use input format FORMAT:


PBES in internal format


BES in PGSolver format


PBES in textual (mCRL2) format

-m[NAME] , --marking-algorithm[=NAME]

specifies the algorithm that is used for the marking computation 0 (default), 1 or 2. In certain cases this choice can have a significant impact on the performance.


use output format FORMAT:


BES in internal format


PBES in internal format


BES in PGSolver format


PBES in textual (mCRL2) format

-QNUM , --qlimit=NUM

limit enumeration of quantifiers to NUM iterations. (Default NUM=1000, NUM=0 for unlimited).

-rNAME , --rewriter=NAME

use rewrite strategy NAME:


jitty rewriting


compiled jitty rewriting


jitty rewriting with prover


append timing measurements to FILE. Measurements are written to standard error if no FILE is provided

-g , --use-global-variant

use the global variant of the algorithm

Standard options

-q , --quiet

do not display warning messages

-v , --verbose

display short log messages

-d , --debug

display detailed log messages


display log messages up to and including level; either warn, verbose, debug or trace

-h , --help

display help information


display version information


display help information, including hidden and experimental options


Wieger Wesselink; Jeroen Keiren