\[ \renewcommand{\implies}{\mathop{\Rightarrow}}\]

This section gives an overview of the classes and algorithms on parameterised
boolean equation systems (PBESs). All classes and algorithms of the PBES Library reside
in the namespace `pbes_system`

.

A Parameterised Boolean Equation System \(\cal{E}\) is a sequence of fixpoint equations, where each equation has the following form:

\[\sigma X(d:D)=\varphi,\]

with \(\sigma \in \{\mu, \nu\}\) *a fixpoint symbol*, \(X(d:D)\) a *predicate variable*,
and \(\varphi\) a *predicate formula*.

The following C++ classes are defined for PBESs:

Expression | C++ class |
---|---|

\(\cal{E}\) | `pbes` |

\(\sigma X(d:D)=\varphi\) | `pbes_equation` |

\(\sigma\) | `fixpoint_symbol` |

\(X(d:D)\) | `propositional_variable` |

\(\varphi\) | `pbes_expression` |

\(d:D\) | `data::variable_list` |

\(e\) | `data::data_expression_list` |

PBES expressions (or predicate formulae) are defined using the following grammar

\[\begin{split}\begin{array}{lrl}
\varphi & ::= & c
\: \mid \: \neg \varphi
\: \mid \: \varphi \wedge \varphi
\: \mid \: \varphi \vee \varphi
\: \mid \: \varphi \implies \varphi
\: \mid \: \forall d{:}D .\:\varphi
\: \mid \: \exists d{:}D .\:\varphi
\: \mid \: X(e),
\end{array}\end{split}\]

where \(c\) is a data term of sort Bool, \(X(e)\) is a parameterised propositional variable, \(d\) is a variable of sort \(D\) and \(e\) is a data expression.

Note

Both \(d{:}D\) and \(e\) can be multivariate, meaning they are shorthand for \(d_1:D_1, \cdots, d_n:D_n\) and \(e_1, \cdots, e_n\) respectively.

Note

The operators \(\neg\) and \(\implies\) are usually not defined in the theory about PBESs. For practical reasons they are supported in the implementation.

The following C++ classes are defined for PBES expressions:

Expression | C++ class |
---|---|

\(c\) | `data::data_expression` |

\(\neg \varphi\) | `not_` |

\(\varphi \wedge \psi\) | `and_` |

\(\varphi \vee \psi\) | `or_` |

\(\varphi \implies \psi\) | `imp` |

\(\forall d{:}D .\:\varphi\) | `forall` |

\(\exists d{:}D .\:\varphi\) | `exists` |

\(X(e)\) | `propositional_variable_instantiation` |

Note

PBES expressions must be *monotonous*: every occurrence of a propositional
variable should be in a scope such that the number of \(\neg\) operators plus the
number of left-hand sides of the \(\implies\) operator is even.

Note

Some of the class names of the operations have a trailing underscore character.
This is only the case when the name itself (like `and`

or `not`

) is a reserved
C++ keyword.

This section gives an overview of the algorithms that are available for PBESs.

algorithm | description |
---|---|

`txt2pbes` |
Parses a textual description of a PBES |

`lps2pbes` |
Generates a PBES from a linear process specification and a state formula |

`constelm` |
Removes constant parameters from a PBES |

`parelm` |
Removes unused parameters from a PBES |

`pbesrewr` |
Rewrites the predicate formulae of a PBES |

`pbesinst` |
Transforms a PBES to a BES by instantiating predicate variables |

`gauss_elimination` |
Solves a PBES using Gauss elimination |

`remove_parameters` |
Removes propositional variable parameters |

`remove_unreachable_variables` |
Removes equations that are not (syntactically) reachable from the initial state of a PBES |

`is_bes` |
Returns true if a PBES data type is in BES form |

`complement` |
Pushes negations as far as possible inwards towards data expressions |

`normalize` |
Brings a PBES expression into positive normal form, i.e. without occurrences of \(\neg\) and \(\implies\) |

algorithm | description |
---|---|

`find_identifiers` |
Finds all identifiers occurring in a PBES data type |

`find_sort_expressions` |
Finds all sort expressions occurring in a PBES data type |

`find_function_symbols` |
Finds all function symbols occurring in a PBES data type |

`find_all_variables` |
Finds all variables occurring in a PBES data type |

`find_free_variables` |
Finds all free variables occurring in a PBES data type |

`find_propositional_variable_instantiations` |
Finds all propositional variable instantiations occurring in a PBES data type |

`replace_sort_expressions` |
Replaces sort expressions in a PBES data type |

`replace_data_expressions` |
Replaces data expressions in a PBES data type |

`replace_variables` |
Replaces variables in a PBES data |

`replace_variables_capture_avoiding` |
Replaces variables in a PBES data type, and avoids unwanted capturing |

`replace_free_variables` |
Replaces free variables in a PBES data type |

`replace_all_variables` |
Replaces all variables in a PBES data type, even in declarations |

`replace_propositional_variables` |
Replaces propositional variables in a PBES data type |

The following rewriters are available

name | description |
---|---|

`bqnf_rewriter` |
BQNF rewriter |

`data2pbes_rewriter` |
Replaces data library operators to equivalent PBES library operators |

`data_rewriter` |
Rewrites data expressions that appear as a subterm of the PBES expression |

`enumerate_quantifiers_rewriter` |
Eliminates quantifiers by enumerating quantifier variables |

`one_point_rule_rewriter` |
Applies one point rule to simplify quantifier expressions |

`pfnf_rewriter` |
Brings PBES expressions into PFNF normal form |

`quantifiers_inside_rewriter` |
Pushes quantifiers inside |

`simplify_quantifiers_rewriter` |
Simplifies quantifier expressions |

`simplify_rewriter` |
Simplifies logical boolean operators |