lpssymbolicbisim

This tool is aimed at generating the reachable part of the bisimulation quotient of systems with an infinite state space. Classical state-space enumeration, such as implemented in lps2lts, relies on enumeration and stores each state explicitly. To avoid this, lpssymbolicbisim applies symbolic techniques to represent infinite sets.

The tool can run in one of four modes: the default mode refine only performs partition refinement with intermediate exploration steps to determine which parts of the state space are unreachable. In explore mode, the tool tries to generate an invariant with forward exploration. When running in explorerefine mode, the tool first generates an invariant and then uses that invariant to initialise the refinement procedure. Finally, it’s possible to simplify an LPS by using the simplify mode.

Instead of generating an invariant, one can also supply an invariant via the option -i/--invariant.

To run this tool, the Z3 SMT-solver should be installed and its bin-directory has to be added to the PATH variable.

Limitations

The tool can only deal with specifications of limited complexity. Furthermore, there are several other restrictions:

  • The tool cannot deal very well with actions that have data parameters. Actions

with Boolean parameters will not lead to a large slowdown, but for larger domains, scalability will be an issue.

In any case, pbessymbolicbisim is probably more powerful, since its abstractions can also rely on the information of the property being checked and it does not have to deal with actions and their parameters.

Manual page for lpssymbolicbisim

Usage

lpssymbolicbisim   [OPTION]... [INFILE [OUTFILE]]

Description

Performs partition refinement on INFILE and outputs the resulting LTS. This tool is highly experimental.

Command line options

-QNUM , --qlimitNUM

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

-rNAME , --rewriterNAME

use rewrite strategy NAME:

jitty

jitty rewriting

jittyc

compiled jitty rewriting

jittyp

jitty rewriting with prover

-sMODE , --simplifierMODE

set the simplifying strategy for expressions

fm

Use functions from the mCRL2 data library to eliminate redundant inequalities

finite

Only simplify expressions over finite discrete data

identity

Do not simplify expressions

auto

Automatically select the best simplifier

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

Thomas Neele