µCRL toolset

Quick summary


Linear process equations (LPEs)

The whole idea of the architecture of the toolset is centered around the notion of a Linear Process Equation (LPE). This is a simply structured process, where the state consists of an assigment to a sequence of typed data variables. Its behaviour is specified by condition, action and effect functions. This format is very similar to I/O automata or the core of Unity processes.

Restriction of functionality

A major other idea is that the toolset must only provide functionality that cannot be easily obtained via the use of other tools. Therefore, the toolset is currently restricted to a state space generator, a simulator and a few tools to manipulate LPEs. The generated state spaces can be manipulated and visualised by for instance the toolset Eucalyptus/Ceasar/Aldebaran .

Groups of tools

The core of the toolset contains four groups of tools.
  1. Linearizing tools. This group contains one tool, called mcrl . The tool mcrl transforms µCRL process definitions to linear process operators (LPEs). All the other tools of the toolset work on LPEs. Thus, before doing any analysis, mcrl must be invoked with a µCRL specification as input.
  2. State space explorators. This group contains two tools. The instantiator which generates from an LPE a concrete transition system and the simulator, msim, which can single-step a process. The instantiator is highly optimized by using a very fast compiling rewriter. The output of the instantiator can be read, manipulated and, visualized by the CADP (Caesar/Aldebaran) toolset. It is possible to store the state space in an extremely compact file format for storing labeled transition systems called SVC format [1] .
  3. Reduction tools. This group contains four reduction tools (each of them reads an LPE and writes an LPE). These reduction tools are
    1. constelm, constant elimination,
    2. parelm, parameter elimination,
    3. sumelm, sum elimination, and
    4. structelm, structure elimination.
    These reduction tools are the implementations of the reduction methods described in [2] .
  4. Rewrite tools. This group contains the tool rewr, rewrite, which normalizes the LPE, with respect to the rewrite rules in the ADT. If a condition belonging to a summand is equal to false then that summand will be removed.
In addition there are two groups of tools.
  1. Tools for manipulation of labeled transition systems (LTSs). A reduction algorithm based on confluence and minimisation algorithms modulo equivalences such as bisimulation and branching bisimulation have been implemented, collapsing equivalent states.
  2. Tools which lean on a theorem prover based on an extension of BDDs with equality. The main functionality of this prover is to transform a formula into an equivalent binary decision diagram (BDD ) [3] Here follows a list of these tools.
    1. formcheck, which computes the result of a boolean formula ,
    2. invcheck, checks if a boolean formula is an invariant of a LPE,
    3. invelm , uses an invariant to eliminate unreachable summands,
    4. confcheck, checks which tau-summands are confluent and marks them on request,
    5. reachelm, tries to predict which summands will be never used during state space generation. These summands will be deleted from the LPE.
Back to µCRL home page