Maurice Laveaux: Abstracting real-valued parameters in parameterised Boolean equation systems


Event Details


The mCRL2 tool-set utilizes parameterised boolean equation systems to verify formulas from modal mu-calculus on models written in the minimal common representation language (mCRL2). For models of real-timed systems this introduces real-valued parameters in these equation systems. Solving parameterised boolean equation systems with real-valued parameters is not possible in most cases.

We will show that a region abstraction, derived from a similar notion defined for timed automata, can also be applied to parameterised boolean equation systems. An alternative abstraction where regions are combined into so-called zones will be defined as well. In some cases this approach works better in practice. However, it is also more restricted in the type of model checking questions that it can answer. Finally, we will define suitable representations for regions and zones that have also been implemented using the mCRL2 language.