lpsbisim2pbes

Construct a PBES that expresses whether the two LPSs given as input are equal modulo some behavioural equivalence relation specified with option -b/--bisimulation. The two LPSs used to construct the PBES are equivalent if and only if the solution to the PBES is true.

A precise definition of the construction of the PBES can be found in [CBPW07].

[CBPW07]T. Chen, B. Ploeger, J. van de Pol, and T. A. C. Willemse: Equivalence Checking for Infinite Systems using Parameterized Boolean Equation Systems, in CONCUR 2007, vol. 4703 of LNCS, pp. 120–135.

Manual page for lpsbisim2pbes

Usage

lpsbisim2pbes   [OPTION]... INFILE1 [INFILE2 [OUTFILE]]

Description

Reads two files containing an LPS, and computes a PBES that expresses bisimulation between the two. If OUTFILE is not present, standard output is used.

Command line options

-bNAME , --bisimulationNAME

generate a PBES for the bisimulation type NAME:

strong-bisim

strong bisimulation

weak-bisim

weak bisimulation

branching-bisim

branching bisimulation

branching-sim

branching simulation equivalence

-n , --normalize

normalize the result

-oFORMAT , --outFORMAT

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-levelLEVEL

display intermediate messages up to and including level

-h , --help

display help information

--version

display version information

Author

Wieger Wesselink; Tim Willemse and Bas Ploeger