Parameterised Boolean Equation Systems Instantiation and Solving

This section describes instantiation and solving algorithms for PBESs that are used in the tool pbessolve.

Preliminaries to PBES instantiation to structure graph

The PBES instantiation algorithm, defined in Algorithm PbesInstStructureGraph builds a structure graph given a PBES. The graph is constructed by instantiation of the PBES equations.

Structure graph

A structure graph, see [KRW12], is a graph structure that captures BESs in their full generality. Structure graphs capture information regarding (the order of) fixed points, as well as the structure of the right hand sides of the equations.

Definition (Structure graph)

A structure graph is a tuple with a set of nodes containing proposition variables, a set of edges, a partial function that assigns a rank to each node, and a partial function that assigns a decoration to each node. A structure graph is formally defined using the following SOS rules, where is the BES and its bound proposition variables, is proposition variable, are proposition formulae and is the fixpoint:

where the rank of a proposition variable , denoted as is defined as follows:

where is defined as:

In the implementation, each proposition variable (BES variables) is replaced by a propositional variable instantiation (PVI). A PVI is a predicate variable instantiation, i.e., given a predicate formula , an occurrence in is a PVI. In the implementation, the nodes of the structure graphs are PVIs.

Attractor sets

Let be a subset of vertices of a structure graph . We define Algorithm AttrDefault to compute the attractor set of A. The value corresponds with disjunction () and corresponds with conjunction (), i.e. the decoration of is if .

where, and . The algorithm returns, for player , the attractor set . As a side effect a mapping is produced that corresponds to a winning strategy.

The algorithm is extended in Algorithm AttrDefaultWithTau such that in addition it sets a local strategy in the mapping .

Finally Algorithm AttrDefaultNoStrategy does not set any strategy.

Preprocessing rewriters

Two rewriters are used to preprocess PBES equations before instantiation: the simplify rewriter and the one-point-rule quantifier elimination rewriter.

In Algorithm PbesInstStructureGraph the application of first simplify rewriter and then one-point-rule quantifier elimination rewriter is combined in rewriter .

Simplify rewriter

The simplify rewriter for PBESs takes a PBES expression and simplifies it. We define the simplify rewriter inductively as follows. For the cases in which quantifiers are used, we consider them ranging over a set of typed variables, and indicate with the free variables appearing in PBES expression .

where is a Boolean data variable, is a data expression and and are PBES expressions.

One-point-rule quantifier elimination rewriter

Before presenting the rewriter itself, we need to define the function . Function computes a set of equalities and inequalities for a data expression , such that the following holds:

for some data expression , data variables and data expressions .

The function is inductively defined as follows:

where is a Boolean data variable, is a data variable, and are data expressions, is the set of all equalities and inequalities, and:

Function is extended to PBES expressions, consider , as follows:

for some data expression . The inductive defition of is extended with the following:

We define the one-point-rule rewriter inductively as follows:

Rewriter

Disclaimer on rewriter

This rewriter is effective only if we are solving a PBES with evidence information after having effectively solved the corresponding PBES without evidence information; otherwise the rewriter does nothing.

Rewriter aims to remove irrelevant PVIs while instantiating a PBES with information about evidence, by exploiting information obtained after having solved the same PBES but without evidence information.

The rewriter relies on two sets of PVIs: is a set of PVIs without evidence information and is a set of PVIs that encode information about evidence, where is the set of actions present in the summands of the original LPS. If the solution of the PBES without evidence information is true then , otherwise .

The PVIs belonging to or are relevant and must be kept untouched by the rewriter.

If the solution of the PBES without evidence information is true then the rewriter is as follows:

where , a data expression and, , and PBES expressions.

While, if the solution of the PBES without evidence information is false the rewriter changes in the following case:

PBES instantiation algorithm

Algorithm PbesInstStructureGraph gets as input a PBES , its initial state , rewriter which first applies simplify rewriter and then one-point-rule rewriter, a set of edges (can be empty), a set of vertices (can be empty), and generates a structure graph .

Let PBES be , then with , for , we indicate the right-hand side of the equation for where is substituted to and then the rewriter is applied, namely . Sets and are the input for rewriter –the set used in rewriter is here defined as the set of PVIs that are successors of node in the set of edges . In case the structure graph of PBES without evidence information has been already solved, then is the set of relevant dependencies (edges) between nodes that do not encode information about evidence, and is the set of nodes that encode information about evidence. Otherwise, the sets are empty.

Algorithm PbesInstStructureGraph uses function to compute nodes and edges of the structure graph. Function uses functions decoration and rank to assign decorations and ranks to the nodes in the structure graph.

Definition (Decoration)

Let and for , is a partial function that assigns a decoration to a node in , where stands for undefined:

where we assume that in none of the is a conjunction, and in none of the is a disjunction.

Definition (Rank)

Every predicate variable bound in PBES is assigned a rank, where if occurs before in , and is even is and only if is labelled with a greatest fixpoint.

In the following, rank is undefined, denoted with , if not applied to a predicate variable.

Function is defined as follows:

Definition (:math:`SG^0`)

where the otherwise case considers or and for which we assume that in none of the is a conjunction, and in none of the is a disjunction. And where returns a tuple where nodes, edges, decoration and rank are computed for subformulas of .

We define as follows:

Definition (:math:`SG^1`)

where the otherwise case considers or and for which we assume that in none of the is a conjunction, and in none of the is a disjunction.

Note that, for , if then the node is not created, but the edge to it is created. This is because either the node has already been created or it will be created (since it is a predicate variable).

The instantiation algorithm PbesInstStructureGraph is as follows:

The algorithm initializes sets and to the initial state . Set contains those PVIs that still need to be explored and set that contains PVIs that have been discovered but for which the corresponding right-hand side equation may not have been computed yet. While the set is not empty then an element () of is choosen to be the current candidate. The element is removed from the set. In line 9, the rewriter is applied to the right-hand side of the equation for where is substituted to , and the result is stored in . In line 10, rewriter is applied to and sets and are those containing relevant PVIs that should be not rewritten (note that this only applies if a PBES without evidence information as been solved previously, othewise the sets are empty). In line 12, computes nodes and edges to be added to the structure graph based on the current PVI that is considered and its right-hand side . In line 13, the nodes and edges discovered by are added to the actual structure graph that will be returned. Afterwards, sets and are updated such that the former will be extended with the occurrences found in that have not been discovered yet, and the latter is extended with the occurrences found in .

Solving strategies for PBES instantiation

The tool pbessolve has a flag that is used to set the solving strategy. The flas is --solve-strategy=NAME (for short -sNAME) where NAME goes from 0 to 4. The list of solving strategies is as follows:

List of solving strategies

• 0- No on-the-fly solving is applied

• 1- Propagate solved equations using an attractor

• 2- Detect winning loops

• 3- Solve subgames using a fatal attractor

• 4- Solve subgames using the solver

Solving strategy 0- No on-the-fly solving is applied is the combination of two techniques: self-loop removal and propagation of solved equations. Thus, we first present these two techniques.

Self-loop removal

The lemma below indicated that one can simplify the PBES equation that is being created without affecting the solution to the PBES.

Lemma 1

The solution to all variables in a PBES is equivalent to the solution to those variables in the PBES , where if and if .

Using this lemma in the instantiation algorithm, rather than creating a structure graph underlying the equation , we can create a structure graph for . This can be done by adding, in Algorithm PbesInstStructureGraph0, the assignment below assignment .

Propagation of solved equations

This technique exploits the fact that some of the PBES equations that are generated while exploring the PBES are already solved (possibly after using the self-loop removal technique).

We first introduce some additional notation. By we denote the set of vertices that represent equations with solution , whereas denotes the set of vertices representing equations with solution . Let be a partial function that maps vertices to the PVIs they represent. For a set of vertices , we define the substitution as follows for all if and if . The union of two substitutions is again a substitution, provided that the domain of variables these substitutions range over are disjoint.

The lemma below indicates how one can utilise such information to simplify the PBES equation that is being created, again without affecting the solution to the PBES.

Lemma 2

The solution to all variables in a PBES is equivalent to the solution to those variables in the PBES , where for all , where denotes the solution to under environment .

Using this lemma, rather than creating a structure graph underlying the equation , we can create a structure graph for , provided that and contain vertices that represent solved equations.

We implement this using a rewriter which takes a formula (and implicitly takes sets and into account). This leads to the following bottom-up procedure in which yields a tuple , where is either a Boolean value, or the value , and is a predicate formula that is equivalent to under the assumption that and are solved, but the formula is not fully solved using that information. Predicate formula (resp. ) is a conjunctive (resp. disjunctive) formula, representing in case is true (resp. false); in case is true, the conjunctive formula can be used to construct a witness, as it contains exactly all dependencies on that are needed to make formula hold. Dually for formula .

0- No on-the-fly solving is applied

In Algorithm PbesInstStructureGraph0 we present solving strategy 0- No on-the-fly solving is applied. This is a combination of two techniques: and :

Self-loop removal example

Example 1

Let us consider the following mCRL2 specification

act b;

proc L(n: Nat) = (n==1) -> b . L(2)
               + (n==2) -> b.  L(2);
init L(1);

The labelled transition system underlying this specification is

The property we verify is

mu V.(<b>V || nu W. <true>W ).

Let us consider the PBES without evidence information

pbes mu X(n_L: Nat) =
           (exists e_L: Bool. val(if(e_L, n_L == 2, n_L == 1)) && X(2)) || Y(n_L);
     nu Y(n_L: Nat) =
           exists e_L: Bool. val(if(e_L, n_L == 2, n_L == 1)) && Y(2);

init X(1);

If no optimization is applied then PBES is instantiated to the following structure graph

By the application of self-loop removal the PBES is instantiated to the following structure graph

In this latter the self-loops in and are removed.

0- No on-the-fly solving is applied - example

Example 2

Let us consider the following mCRL2 specification

act a;
proc P(n:Nat) = (n < 50) -> a. P(n+1)
                + (n == 10) -> a. P(n)
                + (n == 9)  -> a. P(n+2)
                + (n == 20) -> a. P(10);

init P(0);

The labelled transition system underlying this specification is (for the sake of clarity we also add numbers to identify the states)

The property we verify is

nu X. <a>X.

We again consider to instantiate the PBES without evidence information.

If no optimization is applied then 51 equations are generated and are the following

Y(0) = Y(1) with rank 0
Y(1) = Y(2) with rank 0
Y(2) = Y(3) with rank 0
Y(3) = Y(4) with rank 0
Y(4) = Y(5) with rank 0
Y(5) = Y(6) with rank 0
Y(6) = Y(7) with rank 0
Y(7) = Y(8) with rank 0
Y(8) = Y(9) with rank 0
Y(9) = Y(11) || Y(10) with rank 0
Y(11) = Y(12) with rank 0
Y(10) = Y(10) || Y(11) with rank 0
Y(12) = Y(13) with rank 0
Y(13) = Y(14) with rank 0
Y(14) = Y(15) with rank 0
Y(15) = Y(16) with rank 0
Y(16) = Y(17) with rank 0
Y(17) = Y(18) with rank 0
Y(18) = Y(19) with rank 0
Y(19) = Y(20) with rank 0
Y(20) = Y(10) || Y(21) with rank 0
Y(21) = Y(22) with rank 0
Y(22) = Y(23) with rank 0
Y(23) = Y(24) with rank 0
Y(24) = Y(25) with rank 0
Y(25) = Y(26) with rank 0
Y(26) = Y(27) with rank 0
Y(27) = Y(28) with rank 0
Y(28) = Y(29) with rank 0
Y(29) = Y(30) with rank 0
Y(30) = Y(31) with rank 0
Y(31) = Y(32) with rank 0
Y(32) = Y(33) with rank 0
Y(33) = Y(34) with rank 0
Y(34) = Y(35) with rank 0
Y(35) = Y(36) with rank 0
Y(36) = Y(37) with rank 0
Y(37) = Y(38) with rank 0
Y(38) = Y(39) with rank 0
Y(39) = Y(40) with rank 0
Y(40) = Y(41) with rank 0
Y(41) = Y(42) with rank 0
Y(42) = Y(43) with rank 0
Y(43) = Y(44) with rank 0
Y(44) = Y(45) with rank 0
Y(45) = Y(46) with rank 0
Y(46) = Y(47) with rank 0
Y(47) = Y(48) with rank 0
Y(48) = Y(49) with rank 0
Y(49) = Y(50) with rank 0
Y(50) = false with rank 0

and the PBES is instantiated to the following structure graph

If 0- No on-the-fly solving is applied is applied then 21 equations are generated and are the following

Y(0) = Y(1) with rank 0
Y(1) = Y(2) with rank 0
Y(2) = Y(3) with rank 0
Y(3) = Y(4) with rank 0
Y(4) = Y(5) with rank 0
Y(5) = Y(6) with rank 0
Y(6) = Y(7) with rank 0
Y(7) = Y(8) with rank 0
Y(8) = Y(9) with rank 0
Y(9) = Y(11) || Y(10) with rank 0
Y(11) = Y(12) with rank 0
Y(10) = true with rank 0
Y(12) = Y(13) with rank 0
Y(13) = Y(14) with rank 0
Y(14) = Y(15) with rank 0
Y(15) = Y(16) with rank 0
Y(16) = Y(17) with rank 0
Y(17) = Y(18) with rank 0
Y(18) = Y(19) with rank 0
Y(19) = Y(20) with rank 0
Y(20) = Y(10) with rank 0

The instantiation procedure stops when it finds that , which is solved, is a successor of , and the structure graph is simplified to the following

Optimizations 1-4

Solving strategies 1 to 4 each use a different function for , in Algorithm PbesInstHolder. These solving strategies are considered to be optimizations of solving strategy 0.

Routine ExtractMinimalStructureGraph is used to extract a minimal structure graph based on the strategies set in . The procedure returns a structure graph in which information about local winning strategies has been exploited to minimise the structure graph, preserving relevant information to construct evidence. The strategies and are assumed to be consistent with the sets and , i.e, be a closed and winning strategy for the vertices in those sets.

Since optimizations 1 to 4 each use a different function for that is executed periodically, to reproduce the results of Example 3, Example 4 and Example 5 flag --aggressive, of tool pbessolve, must be used.

1- Propagate solved equations using an attractor

In Algorithm PbesInstStructureGraph1 we present the algorithm for optimization 1- Propagate solved equations using an attractor. Algorithm PbesInstStructureGraph1 uses AttrDefaultWithTau.

Example 3

Let us consider again Example 2.

If 1- Propagate solved equations using an attractor is applied then 12 equations are generated and are the following

Y(0) = Y(1) with rank 0
Y(1) = Y(2) with rank 0
Y(2) = Y(3) with rank 0
Y(3) = Y(4) with rank 0
Y(4) = Y(5) with rank 0
Y(5) = Y(6) with rank 0
Y(6) = Y(7) with rank 0
Y(7) = Y(8) with rank 0
Y(8) = Y(9) with rank 0
Y(9) = Y(11) || Y(10) with rank 0
Y(11) = Y(12) with rank 0
Y(10) = true with rank 0

and the PBES is instantiated to the following structure graph

The instantiation procedure does not explore further vertex and, in turn, it finds that vertex is solved. The information that vertex is solved is propagated backwords. Consequently, strategy is set and the structure graph is simplified to the following minimal structure graph

2- Detect winning loops

In Algorithm PbesInstStructureGraph2 we present the algorithm for optimization 2- Detect winning loops. Algorithm PbesInstStructureGraph2 uses FindLoops2. In FindLoops2 routine yields the ranked vertices.

where AttrMinRankGeneric is a slightly modified version of the original attractor set computation AttrDefault, which computes the -min attractor into set restricted to vertices of rank :

where

The above optimisation can be integrated in the instantiation algorithm as follows:

Example 4

Let us consider the following mCRL2 specification

act a;
proc P(n:Nat) = (n < 10) -> a. P(n+1)
            + (n == 5) -> a. P(Int2Nat(n-1))
            + (n == 4)  -> a. P(n+2)
            + (n == 8) -> a. P(5);

init P(0);

The labelled transition system underlying this specification is (for the sake of clarity we also add numbers to identify the states)

The property we verify is

nu X. <a>X.

We again consider to instantiate the PBES without evidence information.

If 0- No on-the-fly solving is applied or 1- Propagate solved equations using an attractor then 11 equations are generated and are the following

Y(0) = Y(1) with rank 0
Y(1) = Y(2) with rank 0
Y(2) = Y(3) with rank 0
Y(3) = Y(4) with rank 0
Y(4) = Y(5) || Y(6) with rank 0
Y(6) = Y(7) with rank 0
Y(5) = Y(4) || Y(6) with rank 0
Y(7) = Y(8) with rank 0
Y(8) = Y(5) ||Y(9) with rank 0
Y(9) = Y(10) with rank 0
Y(10) = false with rank 0

and the PBES is instantiated to the following structure graph

If 2- Detect winning loops is applied then 7 equations are generated and are the following

Y(0) = Y(1) with rank 0
Y(1) = Y(2) with rank 0
Y(2) = Y(3) with rank 0
Y(3) = Y(4) with rank 0
Y(4) = Y(5) || Y(6) with rank 0
Y(6) = Y(7) with rank 0
Y(5) = Y(4) || Y(6) with rank 0

and the PBES is instantiated to the following structure graph

The instantiation procedure does not explore further vertex and, in turn, sets strategies and . Consequently, the structure graph is simplified to the following minimal structure graph

3- Solve subgames using a fatal attractor

In Algorithm PbesInstStructureGraph3 we present the algorithm for optimization 3- Solve subgames using a fatal attractor. Algorithm PbesInstStructureGraph3 uses FatalAttractorOriginal, which is very close to the original fatal attractors computation [HKP13].

where AttrMinRankOriginal is a slightly modified version of the original attractor set computation AttrMinRankGeneric, which computes the -min attractor into set restricted to vertices of rank at least :

where

The above optimisation can be integrated in the instantiation algorithm as follows:

Example 5

Let us consider the following mCRL2 specification

act a,b;
proc P(n:Nat) = (n <= 4) -> a. P(n+1)
            + (n < 8 && n > 4) -> b . P(n+1)
            + (n == 5) -> b. P(Int2Nat(n-1) )
            + (n == 6) -> b. P(5);

init P(0);

The labelled transition system underlying this specification is (for the sake of clarity we also add numbers to identify the states)

The property we verify is

mu Y.(nu X .(mu W.(<a>Y || <b>X || <a>W)))

We again consider to instantiate the PBES without evidence information. The PBES is as follows:

sort Enum3 = struct e2_3 | e1_3 | e0_3;

map C3_: Enum3 # Nat # Nat # Nat -> Nat;
    C3_1: Enum3 # Bool # Bool # Bool -> Bool;

var x2,y3,y2,y1: Nat;
    e1,e2: Enum3;
    x3,y6,y5,y4: Bool;
eqn C3_(e1, x2, x2, x2)  =  x2;
    C3_(e2_3, y3, y2, y1)  =  y3;
    C3_(e1_3, y3, y2, y1)  =  y2;
    C3_(e0_3, y3, y2, y1)  =  y1;
    C3_1(e2, x3, x3, x3)  =  x3;
    C3_1(e2_3, y6, y5, y4)  =  y6;
    C3_1(e1_3, y6, y5, y4)  =  y5;
    C3_1(e0_3, y6, y5, y4)  =  y4;

pbes mu Z(n_P: Nat) =
    X0(n_P);
    nu X0(n_P: Nat) =
    Y0(n_P);
    mu Y0(n_P: Nat) =
    val(n_P <= 4) && Z(n_P + 1) || (exists e_P: Enum3. val(false)) || (exists e_P: Enum3. val(C3_1(e_P, n_P == 6, n_P == 5, n_P < 8 && 4 < n_P)) && X0(C3_(e_P, 5, Int2Nat(n_P - 1), n_P + 1))) || val(n_P <= 4) && Y0(n_P + 1) || (exists e_P: Enum3. val(false));

init Z(0);

If 0- No on-the-fly solving is applied or 1- Propagate solved equations using an attractor or 2- Detect winning loops then 24 equations are generated and are the following

Z(0) = X0(0) with rank 1
X0(0) = Y0(0) with rank 2
Y0(0) = Z(1) || Y0(1) with rank 3
Z(1) = X0(1) with rank 1
Y0(1) = Z(2) || Y0(2) with rank 3
X0(1) = Y0(1) with rank 2
Z(2) = X0(2) with rank 1
Y0(2) = Z(3) || Y0(3) with rank 3
X0(2) = Y0(2) with rank 2
Z(3) = X0(3) with rank 1
Y0(3) = Z(4) || Y0(4) with rank 3
X0(3) = Y0(3) with rank 2
Z(4) = X0(4) with rank 1
Y0(4) = Z(5) || Y0(5) with rank 3
X0(4) = Y0(4) with rank 2
Z(5) = X0(5) with rank 1
Y0(5) = X0(4) || X0(6) with rank 3
X0(5) = Y0(5) with rank 2
X0(6) = Y0(6) with rank 2
Y0(6) = X0(5) || X0(7) with rank 3
X0(7) = Y0(7) with rank 2
Y0(7) = X0(8) with rank 3
X0(8) = Y0(8) with rank 2
Y0(8) = false with rank 3

and the PBES is instantiated to the following structure graph

If 3- Solve subgames using a fatal attractor is applied then 17 equations are generated and are the following

Z(0) = X0(0) with rank 1
X0(0) = Y0(0) with rank 2
Y0(0) = Z(1) || Y0(1) with rank 3
Z(1) = X0(1) with rank 1
Y0(1) = Z(2) || Y0(2) with rank 3
X0(1) = Y0(1) with rank 2
Z(2) = X0(2) with rank 1
Y0(2) = Z(3) || Y0(3) with rank 3
X0(2) = Y0(2) with rank 2
Z(3) = X0(3) with rank 1
Y0(3) = Z(4) || Y0(4) with rank 3
X0(3) = Y0(3) with rank 2
Z(4) = X0(4) with rank 1
Y0(4) = Z(5) || Y0(5) with rank 3
X0(4) = Y0(4) with rank 2
Z(5) = X0(5) with rank 1
Y0(5) = X0(4) || X0(6) with rank 3

and the PBES is instantiated to the following structure graph

The instantiation procedure does not explore further vertices and and, in turn, sets strategies , , , , , and . Consequently, the structure graph is simplified to the following minimal structure graph

4- Solve subgames using the solver

In Algorithm PbesInstStructureGraph4 we present the algorithm for optimization 4- Solve subgames using the solver. Algorithm PbesInstStructureGraph4 uses PartialSolve, where and are extended by solving a partial game.

The above optimisation can be integrated in the instantiation algorithm as follows:

4- Solve subgames using the solver

Optimization 4- Solve subgames using the solver does not perform as expected. Currently, for Example 2 it is comparable to optimization 1- Propagate solved equations using an attractor, for Example 4 it is comparable to optimizations 0- No on-the-fly solving is applied and 1- Propagate solved equations using an attractor, and for Example 5 it is comparable to optimizations 0- No on-the-fly solving is applied, 1- Propagate solved equations using an attractor and 2- Detect winning loops.

Additional optimizations to PBES instantiation

During the execution of the instantiation algorithm (with any solving strategy), the set todo may contain nodes that become irrelevant, as the solution of the PBES can already be computed without exploring these irrelevant nodes. This for instance happens in a right hand side when is true. The variable does not need to be explored further. To this end we present a routine, PruneTodo, that recalculates the set todo.

In the tool pbessolve, flag --prune-todo-list can be used to enable this routine. The routine can be used in combination with any solving strategy, and it takes time at most proportional to the time to instantiate the PBES.

Variables that are removed from the todo set, may become relevant again, but may not be added automatically to todo. Consider equations . At some point is explored and is in the todo set. If becomes irrelevant, is removed from the todo set, without being explored. If at a later point is explored, becomes relevant again, but as is explored already will not be investigated further. Hence, is not added to todo. Therefore, it is needed that once pruning has taken place once, it must be repeated to detect such variables to be readded to todo.

In particular when todo becomes empty, it is necessary to do one more prune, to be sure that all reachable BES variables are being investigated.

In Algorithm PbesInstStructureGraphPrune we present the instantiation algorithm in which pruning is applied. In fact, algorithm PbesInstStructureGraphPrune uses PruneTodo.

The above routine can be integrated in the instantiation algorithm as follows. Note, the following is the instantiation algorithm for 0- No on-the-fly solving is applied and where pruning is applied.

Pruning the todo set can help reduce the number of iterations to execute in the instantiation procedure.

Recursive procedure for solving structure graphs

The algorithm to recursively solve a structure graph, Algorithm SolveRecursive, is based on Zielonka’s recursive algorithm [Z98]. It computes a partitioning of the set of vertices of a structure graph into of vertices that represent equations evaluating to true, and vertices that represent equations evaluating to false. A precondition of this algorithm is that it contains no nodes with decoration or .

To satisfy the precondition, a pre-processing step is needed, see Algorithm PreProcessing.

Algorithm SolveRecursive is as follows:

In Algorithm SolveRecursive the routine starts by checking whether the set of nodes is empty and if so it returns a tuple with empty sets. Otherwise, gets the value of the minimal rank of the nodes in , (the player) is computed such that the result is either 0 or 1 depending on , and the set is updated to be the set of all nodes in that have rank . Then, by executing routine and a set of vertices that represent equations evaluating to true, and a set of vertices that represent equations evaluating to false are computed.

Note that this algorithm does not explicitly include how to extract strategies from the procedure of solving a structure graph.

Before defining Algorithm SolveRecursiveStrategies which solves a structure graph and computes strategies , let us define strategies function and priority function.

Definition (:math:`\tau(U)`)

Let , we define the strategy for nodes in set , denoted as , such that:

Definition (:math:`f_1 \lceil f_2`)

Let be partial functions and , we define the priority function as follows:

The priority function application is left-associative, thus, given partial functions for then is interpreted as .

In line 11 the strategy for player is updated, in particular is the strategy computed in set , is the strategy that results from the computation of the attractor set of and is the strategy resulting from the recursive call to . In line 12 the strategy for player is empty. In line 17 the strategy for player is updated, in particular is the strategy resulting from the recursive call to , is the strategy that results from the computation of the attractor set of and is the strategy resulting from the recursive call to .

References

[KRW12]

J.J.A. Keiren, M.A. Reniers and T.A.C. Willemse. Structural Analysis of Boolean Equation Systems. In ACM Transactions on Computational Logic 13(1): 8-1/35, 2012. (DOI)

[HKP13]

M. Huth, J.HP. Kuo, N. Piterman, (2013). Fatal Attractors in Parity Games. In: Pfenning, F. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2013. Lecture Notes in Computer Science, vol 7794. Springer, Berlin, Heidelberg. (DOI)

[Z98]

W. Zielonka, Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci. 200, 1-2 (1998), 135–183, (DOI)