$\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{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}$

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