PBES Implementation Notes

Wieger Wesselink

This document contains details about data structures and algorithms of the PBES Library of the mCRL2 toolset.

• Definitions
  • Well typedness constraints
  • Monotonicity
  • Normalization
• Parity game generator
• Constant parameter detection and elimination
• Gauß elimination
  • Gauß elimination algorithm
  • Solving a BES
• Small progress measures
• Stategraph
  • Definitions
  • Control flow parameters
  • Global algorithm
  • Compute values
  • Local algorithm
• ReachableVariables
• Appendix
  • ATerm format
  • Naming conventions