\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