Home
Introduction to mCRL2
Philosophy
History
Toolset overview
mCRL2 specification and linearisation
LPS tools
LTS tools
Model checking using PBESs
Integration with other tools
Download mCRL2
Latest release
Nightly build
Previous releases
Support
Publications
General
Research
Applications
Course material
Presentations
Showcases
AIA ITP load-balancer
Technical details
Publications
Atacama Large Millimeter Array
Technical details
Publications
Automated parking garage
Technical details
Publications
Automatic Document Feeder
Technical details
Publications
Links
Control Software of the CMS Experiment at CERN’s Large Hadron Collider
Formalisation
Bugs Detected
Future
Technical details
Publications
DAF Trucks Vehicle Function Architecture
Technical Details
Distributed system for lifting trucks
Technical details
Publications
Links
Dogfooding the structural operational semantics of mCRL2
Technical details
Publications
FlexRay communication protocol
Technical details
Publications
Generic Driving Actuator
Technical details
Publications
IEEE 1394 link layer
Technical details
Publications
LedSync communication protocol
Technical details
PCB Printer
Technical details
Publications
Pacemaker
Approach
Technical details
Publications
Patient support platform
System description
Context
Purpose
System architecture
Requirements
Validation
Technical details
Stella Solar Car
Technical details
Using mCRL2
mCRL2 tutorial
A Vending Machine
First variation
Second variation
Third variation
Water cans
Towers of Hanoi
Optimal strategy
The Rope Bridge
A Telephone Book
Gossips
Probabilistic processes
Using mcrl2-gui
Obtaining a linear process specification
Generating a labelled transition system
ltsgraph
and
ltsconvert
ltsview
and
diagraphica
Simulating a linear process specification
Setting an external editor in mcrl2-gui
Concluding remarks
References
mCRL2 language reference
mCRL2 specification
Lexical elements
Comments
Data specifications
Specifying sorts
Data expressions
Specifying mappings
Predefined mappings
Predefined sorts
Constructed sorts
Global variables
Process syntax
Process specifications
Actions
Process algebra
Adding data
Parallel composition
Communication and allow
Rename and hide
Time
Specification syntax
Linear Process Specifications
µ-Calculus
Multi-actions
Action formulas
Regular formulas
State formulas
Relations between symbols
Examples
Boolean Equation Systems
BES expression
BES equation
BES specification
References
Parameterised Boolean Equation Systems
PBES expression
PBES equation
PBES specification
Transforming PBESs
Solving PBESs
Symbolic approximation + Gauß elimination
Enumerative
References
Parsing changes in the 202507.0 Release
Tool documentation
List of the common tools
besinfo
Usage
Description
Command line options
Author
bespp
Usage
Description
Command line options
Author
bessolve
Usage
Description
Command line options
Author
diagraphica
References
lps2lts
Usage
Description
Command line options
Author
lps2pbes
Usage
Description
Command line options
Author
lpsactionrename
Structure of rename files
Rename rule conditions
Example
Regular Expressions
Examples
lpsbinary
Usage
Description
Command line options
Author
lpsbisim2pbes
Usage
Description
Command line options
Author
lpsconfcheck
Usage
Description
Command line options
Author
lpsconstelm
Usage
Description
Command line options
Author
lpsfununfold
An example with function arguments
An example with finite sets
The rewrite rules that are added
lpsinfo
Usage
Description
Command line options
Author
lpsinvelm
Example of use
lpsparelm
Usage
Description
Command line options
Author
lpsparunfold
Options
Background
lpspp
Usage
Description
Command line options
Author
lpsreach
Symbolic Exploration
Symbolic Representation
Limitations
References
lpsrewr
Usage
Description
Command line options
Author
lpssim
Usage
Description
Command line options
Author
lpsstategraph
Usage
Description
Command line options
Author
lpssumelm
Known issues
lpssuminst
Example
lpsuntime
Usage
Description
Command line options
Author
lpsxsim
Usage
Description
Command line options
Author
lts2lps
Usage
Description
Command line options
Author
lts2pbes
Usage
Description
Command line options
Author
ltscompare
Usage
Description
Command line options
Author
ltsconvert
Usage
Description
Command line options
Author
ltsgraph
Usage
Description
Command line options
Author
ltsinfo
Usage
Description
Command line options
Author
ltspbisim
Usage
Description
Command line options
Author
ltspcompare
Usage
Description
Command line options
Author
ltsview
References
mcrl2-gui
Usage
Description
Command line options
Author
mcrl22lps
Linearisation methods
mcrl2i
Usage
Description
Command line options
Author
mcrl2ide
Projects
Simulation and state space generation
Properties
Running tools
Known issues
mcrl2xi
Usage
Description
Command line options
Author
pbes2bes
Generation of a BES
Strategies
pbes2bool
Usage
Description
Command line options
Author
pbes2booldeprecated
Generation of a BES
Solving a BES
Generation of counter examples
Known issues
pbesconstelm
Usage
Description
Command line options
Author
pbesinfo
Usage
Description
Command line options
Author
pbesinst
Usage
Description
Command line options
Author
pbesparelm
Usage
Description
Command line options
Author
pbespgsolve
Usage
Description
Command line options
Author
pbespp
Usage
Description
Command line options
Author
pbesrewr
Usage
Description
Command line options
Author
pbessolve
Usage
Description
Command line options
Author
pbessolvesymbolic
Limitations
pbesstategraph
Usage
Description
Command line options
Author
tracepp
Usage
Description
Command line options
Author
txt2bes
Usage
Description
Command line options
Author
txt2lps
Usage
Description
Command line options
Author
txt2pbes
Usage
Description
Command line options
Author
List of the experimental tools
besconvert
Usage
Description
Command line options
Author
lpscleave
Compositional Minimisation
References
lpscombine
Usage
Description
Command line options
Author
lpsrealelm
Example
lpssymbolicbisim
Limitations
pbesabsinthe
Usage
Description
Command line options
Author
pbesabstract
Example
pbeschain
Usage
Description
Command line options
Author
pbesfixpointsolve
Iteration
Alternating equations
In practice
pbespareqelm
Usage
Description
Command line options
Author
pbespor
Usage
Description
Command line options
Author
pbessymbolicbisim
Usage
Description
Command line options
Author
symbolic_exploration
Usage
Description
Command line options
Author
File formats
Formats for Labelled Transition Systems
mCRL2 LTS format
The aut format
The FSM file format
External tools
mCRL2 fundamentals
Basic modelling with mCRL2
Behaviour and transition systems
Sequences and choices
Specifying systems
Comparing systems
A dash of infinity
Recursion
Regular HML
The modal µ-calculus
Using the µ-calculus
Data
The first-order µ-calculus
Compositionality
Operators
Communicating systems
Labelled transition systems
Internal actions
State values
Equivalences
Trace equivalence
Weak trace equivalence
Strong bisimilarity
Branching bisimilarity
Isomorphism
Determinism
Development
Contributing
Build instructions
Windows instructions
MacOS instructions
Ubuntu instructions
Python dependencies
Documentation
CMake configuration flags
Development guidelines
File hierarchy
Libraries
Tools
Programming
Preamble
Naming conventions
Header policy
Exception handling
Standards compliance
Regression tests
Usability
Platform independence
Feature macros
Formatting
Clang-tidy
Committing changes
Documentation guidelines
Tools
User manual
Libraries
User manual
Reference manual
General
Acknowledgements
mCRL2 library documentation
ATermpp
Introduction to the atermpp library
What is an aterm?
ATermpp types
ATerm properties
Programming with aterms
ATerm creation
ATerm manipulation
ATerms and the C++ Standard Library
ATerm algorithms
mCRL2 Term Library
Preliminaries
Term Library
Function Symbol Pool
Term Pool
Binary Input/Output
Data Structures
Optimizations
Core
Introduction
Concepts
Structure
References
Common functionality
Traversal functions
Generic programming techniques
Static polymorphism
Concepts
mCRL2 Syntax Definition
Lexical Syntax
Data Specifications
Process Specifications
Mu-calculus Formulae
PBES’s
Table of Symbols
Data
Data library
Sort aliases and sort normalisation
Data rewriters
Rewriter implementation notes
Capture-avoiding substitutions
Data enumerator
Data specifications
Expressions
Formal foundations
Historical notes
GUI
The GUI library
Architecture of mcrl2ide
The qt_tool class
The CodeEditor class
LPS
Linear process specifications
Definitions
Specification
Linear processes
Classes in the LPS library
Correctness checks
LPS Implementation Notes
The LPS-library
Algorithms
Confluence Detection
Confluence
State Space Exploration
Graph Exploration
Applications
Search strategies
Cycle detection
Untimed state space exploration
Timed state space exploration
Stochastic state space exploration
Caching
Confluence Reduction
References
Calculation of Communication with Open Terms
Notation
The χ Function
The Communication Function γ
Extension to Open Terms
Simplification
The ϕ Helper Function
Algorithms
Complexity and Optimisation
Extended Algorithms with Accumulator
The ψ Functions
Non-recursive Implementations
Correctness
References
LTS
Notes on the bisimulation partitioner
Introduction
A partitioner for branching bisimulation
References
Implementation of LTSGraph3D
Introduction
Utils namespace
State
Transition
LTSGraph3D
GLCanvas
Visualizer
Springlayout
Introduction
Structure
Creating and accessing an LTS
The standard labelled transition systems
Reducing and comparing labelled transition systems
Some utility functions
Traces
Modal formula
Modal formulas
PBES
Parameterised Boolean Equation Systems
PBES equation systems
PBES expressions
Algorithms
Algorithms on PBESs
Search and Replace functions
Rewriters for PBES expressions
Standard recursive form
PBES Instantiation in
pbesinst
Finite algorithm
Lazy algorithm
Generic lazy algorithms
Parameterised Boolean Equation Systems Instantiation and Solving
Preliminaries to PBES instantiation to structure graph
PBES instantiation algorithm
Solving strategies for PBES instantiation
Additional optimizations to PBES instantiation
Recursive procedure for solving structure graphs
References
PBES Rewriters
Simplifying rewriter
PFNF rewriter
OnePointRule quantifier elimination rewriter
Quantifier inside rewriter
Quantifier expansion rewriter
PBES Abstraction
Absinthe
PBES abstraction
PBES Generation
Transforming an LPS and a property to a PBES
Transforming an LTS and a property to a PBES
Bisimulation
PBES Greybox Implementation Notes
Instantiation from PBES to Parity Game
PBES Implementation Notes
Definitions
Parity game generator
Constant parameter detection and elimination
Gauß elimination
Small progress measures
Stategraph
ReachableVariables
Appendix
Process
Introduction
Process expressions
Algorithms on processes
Search and Replace functions
On free variables in process specifications, LPSs and PBESs
Process Library Implementation Notes
Processes
Guarded process expressions
Alphabet reduction
Optimization for
SMT
SMT Interface library
Utilities
Introduction
Structure
CLI Library
Introduction
Concepts
Library interface
Tutorial
Tool classes
Tool interface guidelines
Available tool classes
Example
Logging Library
Introduction
Concepts
Library interface
Tutorial
Symbolic
Symbolic library
List Decision Diagrams
Symbolic Reachability
Source code reference
Code generation
Testing
Regression tests
Random Testing
Performance measurements
Benchmarks
Setup
Maintainers
Git workflow
Regression testing with TeamCity
Code coverage
Setup
TeamCity project configuration
Build steps
Configure
Build
Test
CPack
Setup VS Env
ltsmin
Release and packaging procedure
Versioning scheme
Creating an official release
Creating release branch
Testing
Updating release number and copyright information
Tagging
Source release
Debian/Ubuntu packages
Fedora packages
Windows release
Mac OS-X installer for 10.5+
Checking the installers
mCRL2
mCRL2 language reference
View page source
mCRL2 language reference
mCRL2 specification
Lexical elements
Comments
Data specifications
Specifying sorts
Data expressions
Specifying mappings
Predefined mappings
Predefined sorts
Mappings on predefined sorts
Constructed sorts
Mapping sorts
Lists, sets and bags
Lists
(Finite) Sets
(Finite) Bags
Structured sorts
Global variables
Process syntax
Process specifications
Actions
Process algebra
Adding data
Conditions
Summation
Parallel composition
Communication and allow
Rename and hide
Time
Specification syntax
Linear Process Specifications
µ-Calculus
Multi-actions
Action formulas
Regular formulas
State formulas
Relations between symbols
Examples
Boolean Equation Systems
BES expression
BES equation
BES specification
References
Parameterised Boolean Equation Systems
PBES expression
PBES equation
PBES specification
Transforming PBESs
Solving PBESs
Symbolic approximation + Gauß elimination
Enumerative
References
Parsing changes in the 202507.0 Release