Logo

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
  • 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
      • pbesiteration
        • 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
    • 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
    • Core
      • Introduction
      • Concepts
      • Structure
      • Tutorial
        • Dependencies
        • The specification
        • The program
        • Manipulating the specification
        • Alphabet reduction
        • References
      • Common functionality
        • Traversal functions
        • Generic programming techniques
        • Static polymorphism
        • Concepts
    • Data
      • Introduction
      • Data specifications
      • Expressions
        • Sort expressions
        • Data expressions
        • Predefined sorts
        • Operations on data expressions
        • Creating data expressions
      • Sort aliases and sort normalisation
      • Data rewriters
        • Rewriter Concept
        • Algorithms using a rewriter
      • Data enumerator
    • GUI
      • The GUI library
        • The qt_tool class
    • LPS
      • Linear process specifications
        • Definitions
        • Specification
        • Linear processes
      • Classes in the LPS library
        • Correctness checks
    • LTS
      • 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
    • Process
      • Introduction
        • Process expressions
        • Algorithms on processes
        • Search and Replace functions
    • 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
        • Zielonka
    • 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
  • 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
      • Windows release
      • Mac OS-X installer for 10.5+
      • Checking the installers
mCRL2
  • mCRL2 library documentation
  • Modal formulas
  • View page source

Modal formulas

The modal formulas library contains classes and algorithms to represent and manipulate modal formulas using the modal mu-calculus with data and time. The code in this library is contained in the namespaces action_formulas, state_formulas and regular formulas.

Previous Next

© Copyright 2011-2025, Technische Universiteit Eindhoven.

Built with Sphinx using a theme provided by Read the Docs.