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:
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
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 |