# pbesparelm¶

The purpose of this tool is to find those parameters in parameterised Boolean equation sytems that do not affect the solution, and remove those in a similar fashion as lpsparelm.

Example:

$\begin{split}\begin{array}{l} \nu V(n{:}\mathbb{N}, b{:}\mathbb{B}) = (b \Rightarrow V(n + 1, b)) \land W(n, b)\\ \mu W(n{:}\mathbb{N}, b{:}\mathbb{B}) = b \lor (b \land W(n+1, b))\\ ~\\ \mathbf{init}\ V(0,\mathit{true}) \end{array}\end{split}$

Instantiation of this PBES using tools such as pbes2bool or pbessolve does not terminate. However, in this PBES, parameter $$n$$ of both equations is redundant (it does not appear positively in any equation), and can be removed. The resulting PBES will be:

$\begin{split}\begin{array}{l} \nu V(b{:}\mathbb{B}) = (b \Rightarrow V(b)) \land W(b)\\ \mu W(b{:}\mathbb{B}) = b \lor (b \land W(b))\\ ~\\ \mathbf{init}\ V(0,\mathit{true}) \end{array}\end{split}$

The algorithm underlying the tool is described in detail in [OWW09].

## Manual page for pbesparelm¶

### Usage¶

pbesparelm   [OPTION]... [INFILE [OUTFILE]]


### Description¶

Reads a file containing a PBES, and applies parameter elimination to it. If OUTFILE is not present, standard output is used. If INFILE is not present, standard input is used.

### Command line options¶

-iFORMAT , --in=FORMAT

use input format FORMAT:

bes

BES in internal format

pbes

PBES in internal format

pgsolver

BES in PGSolver format

text

PBES in textual (mCRL2) format

-oFORMAT , --out=FORMAT

use output format FORMAT:

bes

BES in internal format

pbes

PBES in internal format

pgsolver

BES in PGSolver format

text

PBES in textual (mCRL2) format

--timings[=FILE]

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

#### Standard options¶

-q , --quiet

do not display warning messages

-v , --verbose

display short intermediate messages

-d , --debug

display detailed intermediate messages

--log-level=LEVEL

display intermediate messages up to and including level

-h , --help

display help information

--version

display version information

### Author¶

Wieger Wesselink; Simon Janssen and Tim Willemse