Parameterised Boolean Equation Systems¶
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.
PBES equation systems¶
A Parameterised Boolean Equation System \(\cal{E}\) is a sequence of fixpoint equations, where each equation has the following form:
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¶
PBES expressions (or predicate formulae) are defined using the following grammar
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.
Algorithms¶
This section gives an overview of the algorithms that are available for PBESs.
Algorithms on 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\) |
Search and Replace functions¶
| 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 |
Rewriters for PBES expressions¶
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 |
