This tool is can be used to apply one of several rewriters on a parameterised Boolean equation system.

The simplifying rewriter simplifies pbes expressions by applying the rewrite rules for the data types, and by simplifying boolean expressions. It pushes quantifiers inside as much as possible, removes quantifiers over variables that are not used, and applies straightforward boolean simplifications.

The quantifier-all rewriter expands all quantifiers. The pbes:

map  f: Nat -> Bool;
pbes nu Y = forall x: Nat. val(x < 3 => f(x));
init Y;

is rewriten to:

map  f: Nat -> Bool;
pbes nu Y = val(f(0)) && val(f(1)) && val(f(2));
init Y;

In case the rewriter is requested to expand a quantifier over an unbounded domain it will not terminate. The quantifier-finite rewriter only expands variables over data types that are guaranteed to be finite. If applied to the example above where the quantifier ranges over natural numbers, it does not touch it there are an infinite number of natural numbers.

The quantifier one point rewriter tries to eliminate quantifiers if it can determine that they range over only one element. This works independently of the domain. Contrary to the quantifier-all and quantifier-finite rewriters, the bound variable can be equal to a symbolic value:

map  f:Nat->Bool;
pbes nu Y = forall x:Nat.(val(x==N => f(x)));
init Y;

rewrites to:

map  f: Nat -> Bool;
     N: Nat;
pbes nu Y = val(f(N));
init Y;

The quantifier-one-point rewriter works on both universal and existential quantifiers. It uses equalities (==) and inequallities (!=) to determine to which the bound variable is equal.

The quantifiers-inside rewriter tries to push quantifiers as deeply as possible inside a formula. This is sometimes useful before applying the quantifier-one-point rewriter. It is also useful before applying a quantifier-all or quantifier-finite as it can avoid many copies of the same expression the the expanded pbesses.

The pfnf rewriter transforms the pbes to Predicate Formula Normal Form. In this form all quantifiers are moved to the front of each pbes equation. The right hand side is transformed into a big conjunction over disjunctions of pbes variables.

Specifications of the rewriters can be found in the developers documenation in the document about PBES rewriters.

Manual page for pbesrewr


pbesrewr   [OPTION]... [INFILE [OUTFILE]]


Rewrite the PBES in INFILE, remove quantified variables and write the resulting PBES to OUTFILE. If INFILE is not present, stdin is used. If OUTFILE is not present, stdout is used.

Command line options


use input format FORMAT:


BES in internal format


PBES in internal format


BES in PGSolver format


PBES in textual (mCRL2) format


use output format FORMAT:


BES in internal format


PBES in internal format


BES in PGSolver format


PBES in textual (mCRL2) format

-pNAME , --pbes-rewriter=NAME

use pbes rewrite strategy NAME:


for simplification


for eliminating all quantifiers


for eliminating finite quantifier variables


for pushing quantifiers inside


for one point rule quantifier elimination


for rewriting into PFNF normal form


for rewriting into Parameterised Parity Game form


for rewriting quantifiers over conjuncts to conjuncts of quantifiers (experimental)

-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

Standard options

-q , --quiet

do not display warning messages

-v , --verbose

display short intermediate messages

-d , --debug

display detailed intermediate messages


display intermediate messages up to and including level

-h , --help

display help information


display version information


Jan Friso Groote and Wieger Wesselink