\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