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
        • Sets
        • 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
• Labelled Transition Systems
  • mCRL2 LTS format
  • FSM file format
    • Parameters section
    • States section
    • Transitions section
    • Example
  • Aldebaran format
    • Syntax
    • Example
    • Acknowledgements
• µ-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
• File formats