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

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:

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

PBES classes
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

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

PBES expression classes
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

Selected algorithms on PBES data types
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

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

PBES expression rewriters
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