In this section, we present a new logical framework that defines the design space for (sound) package algorithms. The core of this framework is our *package logic*, which defines the space of potential algorithmic choices of a footprint for a particular magic wand. Successfully packaging a wand in a given state is (as we will show) equivalent to finding a derivation in our package logic, and any actual

package algorithm must correspond to a proof search in our logic (if it is sound). In particular, we provide soundness (Theorem 1) and completeness (Theorem 2) results for our logic. We define a specific package algorithm with this logic at its foundation, inspired by the FIA package algorithm [39] (described in Sect. 2.4) but amending its unsoundness, resulting in (to the best of our knowledge) the first sound and relatively automatic package algorithm.

All definitions and results in this section have been fully mechanised [13] in Isabelle/HOL. Our mechanised definitions are parametric with the underlying verification logic in various senses: the underlying separation algebra is a parameter, the syntax of assertions is defined in a way which allows simple extension with different base cases and connectives, and the semantics of magic wands itself can be restricted if only particular kinds of footprint are desired in practice. As a specific example of the latter parameter, in Sect. 4 we define a novel restriction of magic wand footprints which guarantees better properties in combination with certain usages of fractional permissions; this is seamlessly supported by the general package logic presented here. Nonetheless, to simplify the exposition of this section, we will assume that any magic wand footprint satisfying the connective's standard semantics is an acceptable result.

#### 3.1 Footprint Selection Strategies

As we explained in Sect. 1, there is a wide design space for package algorithms; in particular, many potential strategies for finding a magic wand's footprint exist and none is clearly optimal. Recall that a footprint is a state, and thus consists of permissions to certain heap locations as well as storing their corresponding values; for simplicity we identify a footprint by the permissions it contains.

For example, consider the following magic wand (using fractional permissions) acc(x.b, 1/2) −∗ acc(x.b, 1/2) ∗ (x.b ⇒ acc(x.f)). Suppose this magic wand is to be packaged in a state where full permissions to both x.b and x.f are held, and the value of x.b is currently false. Two valid potential footprints are:

There is no clear reason to prefer one choice over the other: different package algorithms (or manual choices) might choose either. Our package logic allows either choice along with any of many less optimal choices, such as taking both permissions. On the other hand, as motivated earlier in Sect. 3.1, our package logic must (and does) enforce that a single valid footprint is chosen for a wand that works for each and every potential state satisfying its left-hand side.

#### 3.2 Package Logic: Preliminaries

To capture different state models and flavours of separation logic, our package logic is parameterised by a separation algebra. For space reasons, we present here a simplified overview of this algebra, but all definitions (including our assertion semantics) are given in App. D of the TR [16] and have been mechanised. We consider a separation algebra [8,19] where Σ is the set of states, ⊕ : Σ ×Σ → Σ is a partial operation that is commutative and associative, and e ∈ Σ, which corresponds to the empty state, is a neutral element for ⊕. We write for the induced partial order of the resulting partial commutative monoid, and σ1#σ2 iff σ1⊕σ2 is defined (i.e. σ1 and σ2 are compatible). Finally, if σ2 σ1, we define the subtraction σ2 σ1 to be the -largest state σ*r* such that σ2 = σ1 ⊕ σ*r*.

We define our package logic for an assertion language with the following grammar: A = A∗A | B⇒A | B, where A ranges over assertions and B over *semantic assertions*. To allow our package logic to be applied to a variety of underlying assertion logics, we distinguish only the two most-relevant connectives: the separating conjunction and an implication (for expressing conditional assertions). To support additional constructs of the assertion logic, the third type of assertion we consider is a *semantic assertion*, i.e. a function from Σ to Booleans. This third type can be instantiated to represent logical assertions that do not match the first two cases. In particular, assertions such as x.f = 5, acc(x.f), abstract predicates (such as Tree(x)) or magic wands can be represented as semantic assertions. This core assertion language can also be easily extended with native support for e.g. the logical conjunction and disjunction connectives; we explain in App. E of the TR [16] how to extend the rules of the logic accordingly.

#### 3.3 The Package Logic

We define our package logic to prescribe the design space of algorithms for deciding how, in an initial state σ0, to select a valid footprint (or fail) for a magic wand A−∗B. The aim is to infer states σ*w* and σ1 that partition σ0 (i.e. σ0 = σ1 ⊕σ*w*) such that σ*w* is a valid footprint for A−∗B (when combined with any compatible state satisfying A, the resulting state satisfies B). In particular, all permissions (and logical facts) required by the assertion B must either come from the footprint or be guaranteed to be provided by any compatible state satisfying A.

Recall from Sect. 2.4 that the mistake underlying the FIA approach ultimately resulted from allowing multiple different footprints to be selected conditionally on a state satisfying A, rather than a single footprint which works for all such states. Our package logic addresses this concern by defining judgements in terms of the *set* of all states satisfying A; whenever *any* of these tracked states is insufficient to provide a permission required by B, our logic will force this permission to be added *in general* to the wand's footprint (taken from the current state).

A *witness set* S is a set of pairs of states (σ*A*, σ*B*); conceptually, the first represents the state available for trying to prove B *in addition* to the current state; this is initially a state satisfying the wand's left-hand side A. The second represents the state assembled (so-far) to attempt to satisfy the right-hand side B. We write S1 for the set of first elements of all pairs in a witness set S. A *context* Δ is a pair (σ, S) of a state and a witness set; here, σ represents the (asyet unused remainder of the) current state in which the wand is being packaged.

The basic idea behind a derivation in our logic is to show how to assemble a witness set in which *all* second elements are states satisfying B, via some combinations of: (1) moving a part of the first element of a pair in the witness set into the second, and (2) moving a part of the outer state σ into *all* first elements of the pairs (this becomes a part of the wand's footprint). The actual judgements of the logic are a little more complex, to correctly record any hypotheses (called *path-conditions*) that result from deconstructing conditional assertions in B.

Configurations and Reductions. A *configuration* represents a current objective in our package logic: the part of the wand's right-hand side still to be satisfied as well as the current state of a footprint computation. A configuration is a triple B, *pc*,(σ, S), where B is an assertion, pc is a *path condition* (a function from Σ to Booleans), and (σ, S) is a context. Conceptually, B is the assertion still to be satisfied, *pc* represents hypotheses we are currently working under, and the context (σ, S) tracks the current state and witness set, as described above.

A *reduction* is a judgement B, *pc*,(σ0, S0) - (σ1, S1), representing the achievement of the objective described via the configuration on the left, resulting in the final context on the right; σ1 is the new version of the outer state (and becomes the new current state after the package operation); whatever was removed from the initial outer state is implicitly the selected footprint state σ*w*. If a reduction is derivable in our package logic, this footprint σ*w* guarantees that for all (σ*A*, σ*B*) ∈ S0, if (σ*A* ⊕ σ*B*)#σ*w*, then σ*A* ⊕ σ*w* satisfies *pc* ⇒ B. The condition (σ*A* ⊕ σ*B*)#σ*w* ensures that the pair (σ*A*, σ*B*) actually corresponds to a state in which the wand can be applied given the chosen footprint σ*w*, as we explain later. The package logic defines the steps an algorithm may take to achieve this goal.

We represent packaging a wand A −∗ B in state σ0 by the derivation of a reduction B, λσ. ,(σ0, {(σ*A*, e) | σ*A* |= A}) - (σ1, S1), for some state σ1 and witness set S1. The path condition is initially true (we are not yet under any hypotheses). The initial witness set contains all pairs of a state σ*A* that satisfies A and the empty state e, to which a successful reduction will add permissions in order to satisfy B2. An actual algorithm need not explicitly compute this (possibly infinite) set, but can instead track it symbolically. If the algorithm finds a derivation of this reduction, it has proven that the difference between σ0 and σ1 is a valid footprint of the wand A−∗B, since the logic is sound (Theorem 1 below).

Rules. Figure 2 presents the four rules of our logic, defining (via derivable reductions) how a configuration can be reduced to a context. There is a rule for each type of assertion B: *Implication* for an implication, *Star* for a separating conjunction, and *Atom* for a semantic assertion. The logic also includes the rule *Extract*, which represents a choice to extract permissions from the outer state and adds

2 If B is intuitionistic, this can be simplified to only the -*minimal* states that satisfy A. B is intuitionistic [38] iff, if B holds in a state σ, then B holds in any state σ- such that σ-σ. In intuitionistic SL or in IDF, all assertions are intuitionistic.

$$\frac{\langle A, \lambda \sigma, pc(\sigma) \wedge b(\sigma), \Delta \rangle \leadsto \Delta'}{\langle b \Rightarrow A, pc, \Delta \rangle \leadsto \Delta'} \operatorname{Implication} \qquad \frac{\langle A\_1, pc, \Delta\_0 \rangle \leadsto \Delta\_1}{\langle A\_2, pc, \Delta\_1 \rangle \leadsto \Delta\_2} \operatorname{Str} \mathsf{T}$$

$$\begin{array}{c} \forall (\sigma\_A, \sigma\_B) \in S.pc(\sigma\_A) \Longrightarrow \sigma\_A \succeq \mathit{choice}(\sigma\_A, \sigma\_B) \land \mathcal{B}(\mathit{choice}(\sigma\_A, \sigma\_B))\\ S\_\top = \{ (\sigma\_A \ominus \mathit{choice}(\sigma\_A, \sigma\_B), \sigma\_B \oplus \mathit{choice}(\sigma\_A, \sigma\_B)) | (\sigma\_A, \sigma\_B) \in S \land pc(\sigma\_A) \} \\ S\_\bot = \{ (\sigma\_A, \sigma\_B) | (\sigma\_A, \sigma\_B) \in S \land \neg pc(\sigma\_A) \} \\ \hline \end{array}$$

$$\begin{array}{c} \mathit{\bf{S}}\_\bot \mbox{\bf{\mathbin{\bf{\varepsilon}}}}(\mathit{\bf{\varepsilon}}, \mathit{\bf{\varepsilon}}, \mathit{\bf{\varepsilon}}) \{ \mathit{\bf{\varepsilon}}\_\bot, \sigma\_B \} \in S \land \neg pc(\sigma\_A) \} \\ \hline \end{array} \begin{array}{c} \mathit{\bf{\varepsilon}} \mbox{\bf{\varepsilon}} \mbox{\bf{\varepsilon}} \} \end{array}$$

$$\begin{array}{ll} \sigma\_{0} = \sigma\_{1} \oplus \sigma\_{w} & \mathsf{stable}(\sigma\_{w}) \quad \langle A, pc, (\sigma\_{1}, S\_{1}) \rangle \leadsto \Delta\\ S\_{1} = \{ (\sigma\_{A} \oplus \sigma\_{w}, \sigma\_{B}) | (\sigma\_{A}, \sigma\_{B}) \in S\_{0} \land (\sigma\_{A} \oplus \sigma\_{B}) \# \sigma\_{w} \} & \textit{Extract} \end{array}$$

Fig. 2. Rules of the package logic.

them to all pairs of states in the witness set. In the following, we informally write *reducing an assertion* to refer to the process of deriving (in the logic) that the relevant configuration containing this assertion reduces to some context.

To reduce an implication B ⇒ A, the rule *Implication* conjoins the hypothesis B with the previous path condition, leaving A to be reduced. Informally, this expresses that satisfying pc ⇒ (b ⇒ A) is equivalent to satisfying (pc ∧ b) ⇒ A.

For a separating conjunction A1 ∗ A2, the *Star* rule expresses that both A1 and A2 must be reduced, in order to reduce A1 ∗ A2; permissions used in the reduction of the first conjunct must not be used again, which is reflected by the threading-through of the intermediate context Δ1. 3

The *Atom* rule specifies how to prove that all states in S1 (where S is the witness set) satisfy the assertion pc ⇒ B. To understand the premises, consider a pair (σ*A*, σ*B*) ∈ S. If σ*A* does not satisfy the path condition, i.e. ¬pc(σ*A*), then σ*A does not* have to justify B, and thus the pair (σ*A*, σ*B*) is left unchanged; this case corresponds to the set S⊥. Conversely, if σ*A* satisfies the path condition, i.e. pc(σ*A*), then σ*A* must satisfy B, and the corresponding permissions must be transferred from σ*A* to σ*B*. Since some assertions may be satisfied in different ways, such as disjunctions, the algorithm has a choice in how to satisfy B, which might be different for each pair (σ*A*, σ*B*). This choice is represented by *choice*(σ*A*, σ*B*), which must satisfy B and be smaller or equal to σ*A*. We update the witness set by transferring *choice*(σ*A*, σ*B*) from σ*A* to σ*B*. This second case corresponds to the set S. Note that the *Atom* rule can be applied only if σ*A* satisfies B, for all pairs (σ*A*, σ*B*) ∈ S such that pc(σ*A*). If not, a package algorithm must either first extract more permissions from the outer state with the *Extract* rule, or fail.

The *Extract* rule (applicable at any step of a derivation), expresses that we can extract permissions (the state4 σ*w*) from the outer state σ0, and combine

3 The order in the premises is unimportant since A1 ∗ A2 and A2 ∗ A1 are equivalent. 4 We explain formally in App. D of the TR [16] the notion of a stable state, which is a technicality of our general state model; in standard SL, all states are stable.

them with the first element of each pair of states in the witness set. Note that (σ*A*, σ*B*) is removed from the witness set if σ*A* ⊕σ*B* is not compatible with σ*w*. In such cases, adding σ*w* to σ*A* would create a pair in the witness set representing a state in which the wand cannot be applied. Consequently, there is no need to establish the right-hand side of the wand for this pair and our logic correspondingly removes it. Finally, the rule requires that we reduce the assertion A in the new context.

A package algorithm's strategy is mostly reflected by how it uses the *Extract* rule. To package acc(x.b, 1/2) −∗ acc(x.b, 1/2) ∗ (x.b ⇒ acc(x.f)) from Sect. 3.1 one algorithm might use this rule to extract permission to x.f; another might use it to extract permission to x.b (if x.b had value false in the original state).

Example of a Derivation. Let us now illustrate how these rules can be used to package the wand from Sect. 3.1, w := acc(x.f)∗(x.f = y∨x.f = z)−∗acc(x.f)∗ acc(x.f.g). We omit the path condition since it is always the trivial condition (λσ. ). Assume that the outer state σ0 is the addition of σ*yz*, a state that contains permission to y.g and z.g, and σ1. S0 := {(σ*A*, e) | σ*A* ∈ Σ ∧ σ*A* |= acc(x.f) ∗ (x.f = y ∨ x.f = z)} is the initial witness set. We show below a part of a proof that acc(x.f) \* acc(x.f.g),(σ0, S0) - (σ1, S3) is correct, and thus that σ*yz* is a correct footprint of the wand w (since σ0 = σ1 ⊕ σ*yz*):

$$\begin{array}{c} \cdots \\ \hline \langle \mathtt{acc}(\mathtt{x}.\mathtt{t},\mathtt{0},\mathtt{S}\_{0}) \rangle \leadsto (\sigma\_{0},S\_{1}) \\ \hline \end{array} Atom \quad \begin{array}{c} \begin{array}{c} \cdots \\ \hline \langle \mathtt{acc}(\mathtt{x}.\mathtt{t},\mathtt{g}),(\sigma\_{1},S\_{2}) \rangle \leadsto (\sigma\_{1},S\_{3}) \\ \hline \langle \mathtt{acc}(\mathtt{x}.\mathtt{t},\mathtt{g}),(\sigma\_{0},S\_{1}) \rangle \leadsto (\sigma\_{1},S\_{3}) \\ \hline \end{array} \operatorname{Extract} t \\ \hline \end{array} \\ Extract \begin{array}{c} \begin{array}{c} \mathtt{Att} \\ \mathtt{Extract} \\ \mathtt{Set} \\ \mathtt{Set} \\ \mathtt{Set} \\ \end{array} \\ \hline \end{array} \\ Stract \begin{array}{c} \mathtt{Att} \\ \mathtt{Set} \\ \mathtt{Set} \\ \mathtt{Set} \\ \end{array} \\ Start \begin{array}{c} \mathtt{Max} \\ \mathtt{Max} \\ \mathtt{Set} \\ \mathtt{Set} \\ \mathtt{Set} \\ \end{array} \\ Start \begin{array}{c} \mathtt{Max} \\ \mathtt{Max} \\ \mathtt{Set} \\ \mathtt{Set} \\ \mathtt{Set} \\ \end{array} \\ Start \begin{array}{c} \mathtt{Max} \\ \mathtt{Max} \\ \mathtt{Max} \\ \end{array} \\ Start \begin{array}{c} \mathtt{Max} \\ \mathtt{Max} \\ \mathtt{Max} \\ \end{array} \\ Start \begin{array}{c} \mathtt{Max} \\ \mathtt{Max} \\ \mathtt{Max} \\ \end{array} \\ Start \begin{array}{c} \mathtt{Max} \\ \mathtt{Max} \\ \mathtt{Max} \\ \end{array} \\ Start \begin{array}{c} \mathtt{Max} \\ \mathtt{Max} \\ \mathtt{Max} \\ \end{array} \\ Start \end{array}$$

This derivation, which reflects the package algorithm that we will describe in Sect. 3.5, can be read from bottom to top and from left to right. Using the rule *Star* , we split the assertion into its two conjuncts, acc(x.f) (on the left) and acc(x.f.g) (on the right). We then handle acc(x.f) using the rule *Atom*. acc(x.f) holds in the first element of each pair of S0, since any state that satisfies the wand's left-hand side owns x.f. Therefore, we use the rule *Atom* with a *choice* function that always chooses the relevant state with exactly full permission to x.f. S1 is the updated witness set where this permission to x.f has been transferred from the first to the second element of each pair of states. Next, we handle acc(x.f.g). We cannot do this directly using the rule *Atom* from S1. We know that, for each (σ*A*, σ*B*) ∈ S1, x.f.g evaluated in σ*A* is either y or z, but σ*A* owns neither y.g nor z.g. So, we transfer the permissions to both y.g and z.g from the outer state σ0 to all states of S1 1 , using the rule *Extract*, which results in the context (σ1, S2); † represents the three other premises of the rule, namely σ0 = σ*yz* ⊕ σ1, stable(σ*yz*), and S2's definition. Finally, we apply the rule *Atom* to prove acc(x.f.g),(σ1, S2) - (σ1, S3), where the *choice* function chooses for each pair the corresponding state that contains full permission to x.f.g.

#### 3.4 Soundness and Completeness

We write B, pc, Δ - Δ to express that a reduction can be derived in the logic. As explained above, the goal of a package algorithm is to find a derivation of B,λ\_. ,(σ, {(σ*A*, e) | σ*A* ∈ S*A*}) - (σ , S ). If it succeeds, then the difference between σ and σ is a valid footprint of A −∗ B, since our package logic is sound. In particular, we have proven the following soundness result in Isabelle/HOL:

#### Theorem 1 *Soundness. Let* B *be a well-formed*5 *assertion. If*

	- *(a)* B *is intuitionistic*
	- *(b) For all* (σ*A*, σ*B*) ∈ S *,* σ*A contains no permission (i.e.* σ*A* ⊕ σ*A* = σ*A)*

*then there exists a stable state* σ*w s.t.* σ = σ ⊕ σ*w and* σ*w is a footprint of* A −∗ B*.*

The third premise shows that, in an intuitionistic SL or in IDF, the correspondence between a derivation in the logic and a valid footprint of a wand is straightforward (case (a)). However, in classical SL, one must additionally check that all permissions in the witness set have been consumed (case (b)).

We have also proved in Isabelle/HOL that our package logic is complete, i.e. *any* valid footprint can be computed via a derivation in our package logic:

Theorem 2 *Completeness. Let* B *be a well-formed (see footnote 5) assertion. If* σ*w is a stable footprint of* A−∗B*, and* σ = σ ⊕σ*w, then there exists a witness set* S *such that* B,λ*\_*. ,(σ, {(σ*A*, e) | σ*A* ∈ S*A*}) - (σ , S )*.*

#### 3.5 A Sound Package Algorithm

We now describe an automatic package algorithm that corresponds to a proof search strategy in our package logic, and which is thus sound. To convey the main ideas, consider packaging a wand of the shape A −∗ B1 ∗ ... ∗ B*n*. 6 Our algorithm traverses the assertion B1 ∗ ... ∗ B*n* from left to right, similarly to the FIA approach; this traversal is justified by repeated applications of the rule *Star*. Assume at some point during this traversal that the current context is (σ0, S). When we encounter the assertion B*i*, we have two possible cases:

1. All states σ*A* ∈ S1 satisfy B*i*, which means that the permissions (or values) required by B*i* are provided by the left-hand side of the wand. In this case, for each pair (σ*A*, σ*B*) ∈ S, we transfer permissions (and the corresponding values) to satisfy B*i* from σ*A* to σ*B*, using the rule *Atom*. Note that the transferred permissions might be different for each pair (σ*A*, σ*B*). This gives us a new witness set S , while the outer state σ0 is left unchanged. We must then handle the next assertion B*i*+1 in the context (σ0, S ).

5 We formally define well-formedness in App. D of the TR [16]. Intuitively, a well-formed assertion roughly corresponds to a self-framing assertion as defined in Sect. 2.1.

6 In App. I of the TR [16], we also show how our package algorithm handles implications.

2. There is at least one pair (σ*A*, σ*B*) ∈ S such that B*i* does not hold in σ*A*. In this case, the algorithm fails if combining the permissions (and values) contained in the outer state with each σ*A* ∈ S1 is not sufficient to satisfy B*i*. Otherwise, we apply the rule *Extract* to transfer permissions from the outer state σ0 to each state σ*A* in S1 such that B*i* holds in σ*A*. This gives us a new context (σ 0, S ). We can now apply the first case with the context (σ 0, S ).

#### 4 Using the Logic with Combinable Wands

Extending SL with fractional permissions [4] is well-known to be useful for reasoning about heap-manipulating concurrent programs with shared state. In this setting, permission amounts are generalised to fractions 0 ≤ p ≤ 1. Reading a heap location is permitted if p > 0, and writing if p = 1, which permits concurrent reads and ensures exclusive writes. The assertion acc(x.f, p) holds in a state that has *at least* p permission to x.f. A permission amount p + q to a heap location x.f can be split into a permission amount p and a permission amount q, i.e. acc(x.f, p + q) |= acc(x.f, p) \* acc(x.f, q), and these two permissions can be recombined, i.e. acc(x.f, p) \* acc(x.f, q) |= acc(x.f, p + q).

This concept has been generalised [5,7,17,23,29] to *fractional assertions* A*p*, representing a fraction p of A. A*p* holds in a state σ iff there exists a state σ*A* in which A holds and σ is obtained from σ*A* by multiplying all permission amounts held by p [7,29]; in this case, we write σ = p · σ*A*. For example, acc(x.f)*p* ≡ acc(x.f, p), and Tree(x)*p* (where Tree is the predicate defined in Fig. 1) expresses p permission to all nodes of the tree rooted in x.

Using fractional assertions, one might specify a function find, which searches a binary tree and yields a subtree whose root contains key key, as follows [7]: { Tree(x)*p* } find(x, key) { λret.(Tree(ret) ∗ (Tree(ret) −∗ Tree(x)))*p* }, in which ret corresponds to the return value of find. This postcondition is similar to the loop invariant in Fig. 1, except that it needs only a fraction p of Tree(x). A number of automatic SL verifiers, such as Caper [18], Chalice [31], VerCors [2], VeriFast [24], and Viper [34], support fractional assertions in some form.

Combinable Assertions. While it is always possible to split an assertion A*p*+*q* into A*p* ∗A*q*, recombining A*p* ∗A*q* into A*p*+*q* is sound only under some conditions, for example [29] if A is *precise* (in the usual SL sense [38]). We say that A is *combinable* iff the entailment A*p* ∗ A*q* |= A*p*+*q* holds for any two positive fractions p and q such that p + q ≤ 1. As an example, acc(x.f) is combinable, but acc(x.f)∨acc(x.g) is not because a state containing half permission to both x.f and x.g satisfies (acc(x.f) ∨ acc(x.g))0*.*5 ∗ (acc(x.f) ∨ acc(x.g))0*.*5, but not acc(x.f)∨acc(x.g). Combinable assertions are particularly useful to reason about concurrent programs, for instance, to combine the postconditions of parallel branches when they terminate [7].

However, a magic wand is in general *not* combinable, as we show below. This is problematic for SL verifiers; they cannot soundly combine wands, nor predicates that could possibly contain wands in their bodies. One way to prevent

the latter is to forbid magic wands in predicate bodies entirely, but this limits the common usage of predicates to abstract over general assertions in specifications [35]. Another solution is to disallow combining fractional instances of a predicate if its body contains a wand, which means requiring additional annotations to "taint" such predicates transitively. This is overly restrictive for wands which are actually combinable and complicates reasoning about abstract predicate families [35].

To address this issue, we propose a novel restriction of the wand, called *combinable wand* (we use *standard wand* to refer to the usual, unrestricted connective). Unlike standard wands in general, a combinable wand is always combinable if its right-hand side is combinable. Thus, by only using combinable wands instead of standard wands, all assertions in logics such as those employed by Ver-Cors and Viper can be made combinable without any of the other aforementioned restrictions regarding predicates. Section 5 shows that the restriction combinable wands impose is sufficiently weak for practical purposes. Finally, footprints of combinable wands can be automatically inferred by package algorithms built on our package logic. All results in this section have been proven in Isabelle/HOL.

Standard Wands are Not Combinable in General. Even if B is combinable, the standard wand A −∗ B is, in general, not. As an example, the wand w := acc(x.f, 1/2) −∗ acc(x.g) is not combinable, because w0*.*5 ∗ w0*.*5 |= w. To see this, consider two states σ*f* and σ*g*, containing full permissions to only x.f and x.g, respectively. Both states are valid footprints of w, i.e. σ*f* |= w (because σ*f* is incompatible with all states that satisfy the left-hand side) and σ*g* |= w (because σ*g* entails the right-hand side). Thus, by definition, 0.5 · σ*f* |= w0*.*5 and 0.5 · σ*g* |= w0*.*5. However, 0.5 · σ*f* ⊕ 0.5 · σ*g*, i.e. a state with half permission to both x.f and x.g, is *not* a valid footprint of w, and thus w0*.*5 ∗ w0*.*5 |= w.

Intuitively, w is not combinable because one of its footprints, σ*f* , is incompatible with the left-hand side of the wand, but becomes compatible when the footprint is scaled down to a fraction. After scaling, the wand no longer holds trivially, and the footprint does not necessarily establish the right-hand side.

To make this intuition more precise, we introduce the notion of *scalable footprints*. For a state σ, we define *scaled*(σ) to be the set of copies of σ multiplied by any fraction 0 < α ≤ 1, i.e. *scaled*(σ) := {α · σ | 0 < α ≤ 1}. A footprint σ*w* is *scalable w.r.t. a state* σ*A* iff either (1) σ*A* is compatible with *all* states from *scaled*(σ*w*), or (2) σ*A* is compatible with *no* state in *scaled*(σ*w*). A footprint is *scalable for a wand* A −∗ B iff it is scalable w.r.t. all states that satisfy A. Intuitively, this means that the footprint does not "jump" between satisfying the wand trivially and having to satisfy the right-hand side. In the above example, σ*g* is a scalable footprint for w, but σ*f* is not.

Making Wands Combinable. The previous paragraphs show that, even if B is combinable, the standard wand A−∗B is in general not combinable because it can be satisfied by non-scalable footprints. Therefore, we define a novel restricted interpretation for wands that *forces* footprints to be scalable, in the following sense. The restricted interpretation of a wand accepts all scalable footprints, and transforms non-scalable footprints before checking whether they actually satisfy the wand. We call a wand with this restricted interpretation a *combinable wand*, and write A −∗*c* B to differentiate it from the standard wand A −∗ B.

For standard wands, *any* state σ*w* is a footprint of A−∗B iff, for all states σ*A* that satisfy A, σ*A*#σ*w* ⇒ σ*A* ⊕ σ*w* |= B. We obtain the definition of combinable wands by replacing σ*w* with a (possibly smaller) state R(σ*A*, σ*w*) that is scalable w.r.t. σ*A*. R(σ*A*, σ*w*) is defined as σ*w* if *no* state in *scaled*(σ*w*) is compatible with any σ*A*; in that case, condition (2) of scalable footprints holds for R(σ*A*, σ*w*) w.r.t. σ*A*. Otherwise, R(σ*A*, σ*w*) is obtained by removing just enough permissions from σ*w* to ensure that *all* states in *scaled*(R(σ*A*, σ*w*)) are compatible with σ*A*, which ensures that condition (1) holds for R(σ*A*, σ*w*) w.r.t. σ*A*.

To formally define R(σ*A*, σ*w*), we fix a concrete separation algebra (formally defined in App. G of the TR [16]), whose states are pairs (π, h) of a *permission mask* π, which maps heap locations to fractional permissions, and a partial heap h, which maps heap locations to values.

Definition 1. *Let* (π*A*, h*A*) *and* (π*w*, h*w*) *be two states, and let* π *w be the permission mask such that* ∀l. π *w*(l) = min(π*w*(l), 1 − π*A*(l))*. Then*

$$\mathcal{R}((\pi\_A, h\_A), (\pi\_w, h\_w)) = \begin{cases} (\pi\_w, h\_w) & \text{if } \forall \sigma \in scaled((\pi\_w, h\_w)) . \neg(\pi\_A, h\_A) \# \sigma \\ (\pi'\_w, h\_w) & \text{otherwise} \end{cases}$$

*The* combinable wand A −∗*c* B *is then interpreted as follows:*

σ*w* |= A −∗*c* B ⇐⇒ (∀σ*A*. σ*A* |= A ∧ σ*A*#R(σ*A*, σ*w*) =⇒ σ*A* ⊕ R(σ*A*, σ*w*) |= B)

The following theorem (proved in Isabelle/HOL) shows some key properties of combinable wands.

Theorem 3. *Let* B *be an intuitionistic assertion.*

Property 1 expresses that combinable wands constructed from combinable assertions are combinable, which enables verification methodologies underlying tools such as VerCors and Viper to support flexible combinations of wands and predicates (as motivated at the start of this section). Property 2 implies that A∗(A−∗*c*B) |= B, that is, combinable wands can be applied like standard wands. Property 3 states that combinable wands pose no restrictions if the left-hand side is binary, that is, if it can be expressed without fractional permissions (formally defined in App. G of the TR [16]). For example, the predicate Tree(x) from Fig. 1 is binary, which implies that the wands Tree(y) −∗*c* Tree(x) and Tree(y) −∗ Tree(x) are equivalent. This property is an important reason for why combinable wands are expressive enough for practical purposes, as we further evidence in Sect. 5.

Footprints of combinable wands can be automatically inferred by algorithms built on our package logic. We explain (along with examples) in App. H of the TR [16] how to lift the package logic presented in Sect. 3 to handle alternative definitions of allowable footprints such as the restrictions imposed by Definition 1.

#### 5 Evaluation

We have implemented package algorithms for the standard wands and combinable wands in a custom branch of Viper's [34] verification condition generator (VCG). Both are based on the package logic described in Sect. 3, adapted to the fractional permission setting. Both algorithms automate the proof search strategy outlined in Sect. 3.5. Viper's VCG translates Viper programs to Boogie [32] programs. It uses a total-heap semantics of IDF [36], where Viper states include a heap and a permission mask (tracking fractional permission amounts). The heap and mask are represented in Boogie as maps; we also represent witness sets as Boogie maps.

We evaluate our implementations of the package algorithms on Viper's test suite and compare them to Viper's implementation of the FIA as presented in Sect. 2.4. Our key findings are that our algorithms (1) enable the verification of almost all correct package operations. (2) correctly report package operations that are supposed to fail (in contrast to the FIA), and (3) have an acceptable performance overhead compared to the FIA. Moreover, interpreting wands as combinable wands as explained in Sect. 4 has only a minor effect on the results, but correctly rejects attempts to package a non-combinable wand. This finding suggests that verifiers could improve their expressiveness by allowing flexible combinations of wands and predicates with only a minor completeness penalty.

For our evaluation, we considered all 85 files in the test suite for Viper's VCG with at least one package operation. From these 85 files, we removed 29 files containing features that our implementation does not yet support. 28 of these 29 files require proof scripts to guide the footprint inference, which are orthogonal to the concerns of this paper (see App. J of the TR [16] for details).

Table 1 gives an overview of our results. These confirm that our algorithms for standard and combinable wands (S-Alg and C-Alg) do not produce false negatives, that is, are sound. In contrast, the FIA does verify an incorrect program (which is similar to the example in Sect. 2.4). While this is only a single unsound

example, it is worth emphasing that (a) it comes from the pre-existing test suite of the tool itself, (b) the unsoundness was not known of until our work, and (c) soundness issues in a program verifier are critical to address; we show how to achieve this.

Compared with the FIA, our implementation reports a handful of false positives (spurious errors). For S-Alg, 3 out of 5 false positives are caused by missing features of our implementation (such as remembering a subset of the permissions that are inside predicate instances when manipulating predicates); these features could be straightforwardly added in the future. The other 2 false positives are caused by S-Alg's strategy. In one, the only potential footprint prevents the wand from ever being applied; although technically a false positive, it seems useful to reject the wand and alert the user. The other case is due to a coarse-grained heuristic applied by S-Alg that can be improved.

C-Alg reports the expected result in 48 benchmarks. Importantly, it correctly rejects one wand that indeed does not hold as a combinable wand. 5 of the 8 false positives are identical to those for S-Alg. In the other three benchmarks, the wands still do hold as combinable wands, but further extensions to C-Alg are required to handle them due to technical challenges regarding predicate instances. Once these extensions have been implemented, C-Alg will be as precise as S-Alg, indicating that comparable program verifiers could switch to combinable wands to simply enable sound, flexible combinations with predicates.

To evaluate performance, we ran each of the three implementations 5 times on each of the 56 benchmarks on a Lenovo T480 with 32 GB of RAM and a i7- 8550U 1.8 GhZ CPU, running on Windows 10. We removed the slowest and fastest time, and then took the mean of the remaining 3 runs. The FIA takes between 1 and 11 seconds per benchmark. On average, S-Alg is 21% slower than the FIA. For 46 of the 56 examples, the increase is less than 30%, and for 3 examples S-Alg is between a factor 2 and 3.4 slower. The overhead is most likely due to the increased complexity of our algorithms, which track more states explicitly and require more quantified axioms in the Boogie encoding. C-Alg is on average 10% slower than S-Alg. We consider the performance overhead of our algorithms to be acceptable, especially since wands occur much more frequently in our benchmarks than in average Viper projects, as judged by existing tests and examples. More representative projects will, thus, incur a much smaller slow-down.

#### 6 Related Work

VerCors [2] and Viper [34] are to the best of our knowledge the only automatic SL verifiers that support magic wands. Both employ package and apply ghost operations. VerCors' package algorithm requires a user to manually specify a footprint whereas Viper infers footprints using the FIA, which is unsound as we show in Sect. 2.4. Our package algorithm is as automatic as the FIA but is sound.

Lee and Park [30] develop a sound and complete proof system for SL including the magic wand. Moreover, they derive a decision procedure from their completeness proof for propositional SL. However, more expressive versions of SL (that

include e.g. predicates and quantifiers) are undecidable [6] and so this decision procedure cannot be directly applied in the logics employed by program verifiers.

Chang *et al.* [11] define a shape analysis that derives magic wands A −∗ B of a restricted form (A and B cannot contain general imprecise assertions); our package logic does not impose such restrictions, which rule out some useful kinds of wands. For example, A may be a data structure with a read-only part expressed via existentially-quantified fractional permissions or A may contain the necessary permission to invoke a method, which may be an arbitrary assertion. In follow-up work, Chang and Rival [10] present a restricted "inductive" magic wand. Footprints of inductive wands are expressed via a finite unrolling of an inductive predicate defining B until the permissions in A are revealed. Such wands are useful to reason about data structures with back-pointers such as doubly-linked lists.

Iris [26] provides a custom proof mode [27] for interactive SL proofs in Coq [12]. Separation logics expressed in Iris support wands and are more expressive than those of automatic SL verifiers at the cost of requiring more user guidance. Packaging a wand in the proof mode requires manually specifying a footprint and proving that the footprint is correct. While tactics can be used in principle to automate parts of this process, there are no specific tactics to infer footprints.

Fractional assertions have been used in various forms [5,7,17,23,29]. Le and Hobor [29] allow combining two fractional assertions A*p* and A*q* only if A is *precise* in the SL sense (i.e. A describes the contents of the heaps in which it holds precisely). To avoid requiring A to be precise, Brotherston *et al.* [7] introduce *nominal labels* for assertions. If an assertion is split into two fractional assertions, then the same fresh label can be associated with both parts to indicate that they were split from the same assertion.

Two fractional assertions with the same label can be combined. However, this solution has not been implemented and does not deal with packaging wands. Our solution also avoids requiring that an assertion is precise and allows combining assertions even if they were not split from the same assertion. Instead of introducing labels, we introduce a light restriction that ensures that wands are always combinable. As a result, assertions containing combinable wands but no other potentially imprecise connectives (such as disjunction) are combinable. In particular, all assertions employed in verifiers such as VerCors and Viper can be made combinable thanks to our work.

#### 7 Conclusion

We presented a package logic that precisely characterises sound package algorithms for automated reasoning about magic wands. Based on this logic, we developed a novel package algorithm that is inspired by an existing approach, but is sound. Moreover, we identified a sufficient criterion for wands to be combinable, such that they can be used flexibly in logics with fractional permissions, and presented a package algorithm for combinable wands. We implemented our

solutions in Viper and demonstrated their practical usefulness. The soundness and completeness of our package logic, as well as key properties of combinable wands are all proved in Isabelle/HOL. As future work, we plan to extend the implementation of the two package algorithms described in Sect. 5 by porting various features of the pre-existing FIA implementation. Moreover, we will use our package logic to develop another algorithm for Viper's symbolic-execution verifier.

Acknowledgement. This work was partially funded by the Swiss National Science Foundation (SNSF) under Grant No. 197065.

#### References

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

## **Divide-and-Conquer Determinization of B¨uchi Automata Based on SCC Decomposition**

Yong Li1 , Andrea Turrini1,2 , Weizhi Feng1,3 , Moshe Y. Vardi4 , and Lijun Zhang1,2,3(B)

1 State Key Laboratory of Computer Science, Institute of Software,

Chinese Academy of Sciences, Beijing, China<EMAIL_ADDRESS>2 Institute of Intelligent Software, Guangzhou, China 3 University of Chinese Academy of Sciences, Beijing, China

4 Rice University, Houston, USA

**Abstract.** The determinization of a nondeterministic B¨uchi automaton (NBA) is a fundamental construction of automata theory, with applications to probabilistic verification and reactive synthesis. The standard determinization constructions, such as the ones based on the Safra-Piterman's approach, work on the whole NBA. In this work we propose a divide-and-conquer determinization approach. To this end, we first classify the strongly connected components (SCCs) of the given NBA as inherently weak, deterministic accepting, and nondeterministic accepting. We then present how to determinize each type of SCC *independently* from the others; this results in an easier handling of the determinization algorithm that takes advantage of the structure of that SCC. Once all SCCs have been determinized, we show how to compose them so to obtain the final equivalent deterministic Emerson-Lei automaton, which can be converted into a deterministic Rabin automaton without blowup of states and transitions. We implement our algorithm in our tool COLA and empirically evaluate COLA with the state-of-the-art tools Spot and Owl on a large set of benchmarks from the literature. The experimental results show that our prototype COLA outperforms Spot and Owl regarding the number of states and transitions.

#### **1 Introduction**

Nondeterministic B¨uchi automata (NBAs) [6] are finite automata accepting infinite words; they are a simple and popular formalism used in model checking to represent reactive and non-terminating systems and their specifications, characterized by ω-regular languages [2]. Due to their nondeterminism, however, there are situations in which NBAs are not suitable, so deterministic automata are required, as it happens in probabilistic verification [2] and reactive synthesis from logical specifications [34]. Consequently, translating NBAs into equivalent deterministic ω-automata (that is, deterministic automata accepting the same

S. Shoham and Y. Vizel (Eds.): CAV 2022, LNCS 13372, pp. 152–173, 2022. https://doi.org/10.1007/978-3-031-13188-2\_8

ω-regular language) is a necessary operation for solving these problems. While there exists a direct translation from linear temporal logic (LTL) to deterministic ω-automata [15], not all problems of interests can be formalized by LTL formulas, since LTL cannot express the full class of ω-regular properties [42]. For instance, we have to use Linear Dynamic Logic (LDL) [11,41] instead of LTL to express the ω-regular property "the train will arrive in every odd minute". To the best of our knowledge, we still need to go through the determinization of NBAs for LDL to obtain deterministic ω-automata. Therefore, NBA determinization is very important in verifying the whole class of ω-regular properties.

The determinization of NBAs is a fundamental problem in automata theory that has been actively studied for decades. For the determinization of nondeterministic automata accepting finite words, it suffices to use a subset construction [20]. Determinization constructions for NBAs are, however, much more involved since the simple subset construction is not sufficient [36]. Safra [36] gave the first determinization construction for NBAs with the optimal complexity 2O(n log n) , here n is the number of states of the input NBA; Michel [30] then gave a lower bound n! for determinizing NBAs. Safra's construction has been further optimized by Piterman [33] to O((n!)2) [38], resulting in the widely known Safra-Piterman's construction. The Safra-Piterman's construction is rather challenging, while still being the most practical way for B¨uchi complementation [40]. Research on determinization since then either aims at developing alternative Safraless constructions [18,21,28] or further tightening the upper and lower bounds of the NBA determinization [9,26,39,43].

In this paper, we focus on the *practical* aspects of B¨uchi determinization. All works on determinization mentioned above focus on translating NBAs to either deterministic Rabin or deterministic parity automata. According to [37], the more relaxed an acceptance condition is, the more succinct a finite automaton can be, regarding the number of states. In view of this, we consider the translation of NBAs to deterministic *Emerson-Lei* automata (DELAs) [13,37] whose acceptance condition is an arbitrary Boolean combination of sets of transitions to be seen finitely or infinitely often, the most generic acceptance condition for a deterministic automaton. We consider here transition-based automata rather than the usual state-based automata since the former can be more succinct [12].

The B¨uchi determinization algorithms available in literature operate on the *whole* NBA structure at once, which does not scale well in practice due to the complex structure and the big size of the input NBA. In this work we apply a *divide-and-conquer* methodology to B¨uchi determinization. We propose a determinization algorithm for NBAs to DELAs based on their strongly connected components (SCCs) decomposition. We first classify the SCCs of the given NBA into three types: *inherently weak*, in which either all cycles do not visit accepting transitions or all must visit accepting transitions; *deterministic accepting* and *nondeterministic accepting*, which contain an accepting transition and are deterministic or nondeterministic, respectively. We show how to divide the whole B¨uchi determinization problem into the determinization for each type of SCCs *independently*, in which the determinization for an SCC takes advantage of the structure of that SCC. Then we show how to compose the results of the local determinization for each type of SCCs, leading to the final equivalent DELA. An extensive experimental evaluation confirms that the divide-and-conquer approach pays off also for the determinization of the whole NBA.

**Contributions.** First, we propose a *divide-and-conquer* determinization algorithm for NBAs, which takes advantage of the structure of different types of SCCs and determinizes SCCs independently. Our construction builds an equivalent DELA that can be converted into a deterministic Rabin automaton without blowing up states and transitions (cf. Theorem 2). To the best of our knowledge, we propose the *first* determinization algorithm that constructs a DELA from an NBA. Second, we show that there exists a family of NBAs for which our algorithm gives a DELA of size 2n+2 while classical works construct a DPA of size at least n! (cf. Theorem 3). Third, we implement our algorithm in our tool COLA and evaluate it with the state-of-the-art tools Spot [12] and Owl [23] on a large set of benchmarks from the literature. The experiments show that COLA outperforms Spot and Owl regarding the number of states and transitions. Finally, we remark that the determinization complexity for some classes of NBAs can be exponentially better than the known ones (cf. Corollary 1).

#### **2 Preliminaries**

Let Σ be a given alphabet, i.e., a finite set of letters. A transition-based Emerson-Lei automaton can be seen as a generalization of other types of ω-automata, like B¨uchi, Rabin or parity. Formally, it is defined in the HOA format [1] as follows:

**Definition 1.** *A* nondeterministic Emerson-Lei automaton *(NELA) is a tuple* A = (Q, ι, δ, Γk, p,Acc)*, where* Q *is a finite set of* states*;* ι ∈ Q *is the* initial state*;* δ ⊆ Q × Σ × Q *is a* transition relation*;* Γk = {0, 1, ··· , k}*, where* k ∈ N*, is a set of* colors*;* p: δ → 2Γk *is a* coloring function *for transitions; and* Acc *is an* acceptance formula *over* Γk *given by the following grammar, where* x ∈ Γk*:*

$$\alpha := \mathtt{tt} \mid \mathtt{ff} \mid \mathsf{Fin}(x) \mid \mathsf{Inf}(x) \mid \alpha \lor \alpha \mid \alpha \land \alpha.$$

We remark that the colors in Γk are not required to be all used in Acc. We call a NELA a *deterministic* Emerson-Lei automaton (DELA) if for each q ∈ Q and a ∈ Σ, there is at most one q ∈ Q such that (q, a, q ) ∈ δ.

In the remainder of the paper, we consider δ also as a function δ : Q × Σ → 2Q such that q ∈ δ(q, a) whenever (q, a, q ) ∈ δ; we also write q a−→ q for (q, a, q ) ∈ δ and we extend it to words u = u0u1 ··· un ∈ Σ∗ in the natural way, i.e., q u−→ q = q u[0] −→ q1 u[1] −→ · · · u[n] −→ q , where σ[i] denotes the element si of the sequence of elements σ = s0s1s2 ··· at position i. We assume without loss of generality that each automaton is *complete*, i.e., for each state q ∈ Q and letter a ∈ Σ, we have δ(q, a) = ∅. If it is not complete, we make it complete by adding a fresh state q⊥ ∈/ Q and redirecting all missing transitions to it.

A *run* of A over an ω-word w ∈ Σω is an infinite sequence of states ρ such that ρ[0] = ι, and for each i ∈ N, (ρ[i], w[i], ρ[i + 1]) ∈ δ.

The *language* L(A) of A is the set of words accepted by A, i.e., the set of words w ∈ Σω such that there exists a run ρ of A over w such that p(*inf* (ρ)) |= Acc, where *inf* (ρ) = { (q, a, q ) ∈ δ | ∀i ∈ N.∃j > i.(ρ[j], w[j], ρ[j + 1]) = (q, a, q ) } and the satisfaction relation |= is defined recursively as follows: given M ⊆ Γk,

$$\begin{aligned} M &= \mathtt{tt}, \quad M \mid = \mathtt{Fin}(x) \text{ iff } x \notin M, \quad M \mid = \alpha\_1 \lor \alpha\_2 \text{ iff } M \mid = \alpha\_1 \text{ or } M \mid = \alpha\_2, \\\ M &\not\equiv \mathtt{ff}, \quad M \mid = \mathtt{Inf}(x) \text{ iff } x \in M, \quad M \mid = \alpha\_1 \land \alpha\_2 \text{ iff } M \mid = \alpha\_1 \text{ and } M \mid = \alpha\_2. \end{aligned}$$

Intuitively, a run ρ over w is accepting if the set of colors (induced by p) that occur infinitely often in ρ satisfies the acceptance formula Acc. Here Fin(x) specifies that the color x only appears for finitely many times while Inf(x) requires the color x to be seen infinitely often.

The more common types of ω-automata, such as B¨uchi, parity and Rabin can be treated as Emerson-Lei automata with the following acceptance formulas.

## **Definition 2.** *A NELA* A = (Q, ι, δ, Γk, p,Acc) *is said to be*

When the NELA A = (Q, ι, δ, Γk, p,Acc) is a nondeterministic BA (NBA), we just write A as (Q, ι, δ, F) where F is the set of accepting transitions. We call a set C ⊆ Q a *strongly connected component* (SCC) of A if for every pair of states q, q ∈ C, we have that q u−→ q for some u ∈ Σ∗ and q v −→ q for some v ∈ Σ∗, i.e., q and q can be reached by each other; by default, each state q ∈ Q reaches itself. C is a *maximal* SCC if it is *not* a proper subset of another SCC. *All* SCCs considered in the work are maximal. We call an SCC C *accepting* if there is a transition (q, a, q ) ∈ (C ×Σ ×C)∩F and *nonaccepting* otherwise. We say that an SCC C is *reachable* from an SCC C if there exist q ∈ C and q ∈ C such that q u−→ q for some u ∈ Σ∗. An SCC C is *inherently weak* if either every cycle going through the C-states visits at least one accepting transition or none of the cycles visits an accepting transition. We say that an SCC C is *deterministic* if for every state q ∈ C and a ∈ Σ, we have |δ(q, a) ∩ C| ≤ 1. Note that a state q in a deterministic SCC C can have multiple successors for a letter a, but at most one successor remains in C.

Figure 1 shows an example of NBA we will use for our examples in the remainder of the paper; we depict the accepting transitions with a double arrow. Clearly, inside each SCC, depicted as a box, each state can be reached by any other state, and the SCCs are maximal. The SCC {q2, q3} is inherently weak and accepting, since every cycle takes an accepting transition; the SCC {q6} is also inherently weak, but nonaccepting, since every cycle never takes an accepting transition.

**Fig. 1.** An example of NBA.

The remaining two SCCs, i.e., {q0, q1} and {q4, q5}, are not inherently weak, since some cycle takes accepting transitions (like the cycle q0 a−→ q0) while others do not (like the cycle q0 b −→ q0). Both SCCs contain an accepting transition, so they are accepting; the SCC {q0, q1} is clearly nondeterministic, while the SCC {q4, q5} is deterministic. Note that from q5 we have two transitions labelled by b, but only the transition q5 b −→ q4 remains inside the SCC, while the other transition q5 b −→ q6 leaves the SCC, so the SCC is still deterministic.

The following proposition is well known and is often used in prior works.

**Proposition 1.** *Let* A *be an NBA and* w ∈ Σω*. A run of* A *over* w *will eventually stay in an SCC. Moreover, if* w ∈ L(A)*, every accepting run of* A *over* w *will eventually stay in an accepting SCC.*

Proposition 1 is the key ingredient of our algorithm: it allows us to determinize the SCCs independently as L(A) is the union of the words whose runs stay in each accepting SCCs. In the remainder of the paper, we first present a translation from an NBA A to a DELA AE based on the SCC decomposition of A. The obtained DELA AE in fact can be converted to a *deterministic* Rabin automaton (DRA) AR without blowing up states and transitions, i.e., we can just convert the coloring function and the acceptance formula of AE to DRAs.

#### **3 Determinization Algorithms of SCCs**

Determinizing each SCC of A independently is not straightforward since it may be reached from the initial state only after reading a nonempty finite word; moreover, there can be words of different length leading to the SCC, entering through different states. To keep track of the different arrivals in an SCC at different times, we make use of run DAGs [24], that are a means to organize the runs of A over a word w. In this section, we first recall the concept of run DAGs and then describe how to determinize SCCs with their help.

**Definition 3.** *Let* A = (Q, ι, δ, F) *be an NBA and* w ∈ Σω *be a word. The run DAG* GA,w = V,E *of* A *over* w *is defined as follows: the set of vertices* V ⊆ Q×N *is defined as* V = l≥0(Vl×{l}) *where* V0 = {ι} *and* Vl+1 = δ(Vl, w[l]) *for every* l ∈ N*; there is an edge* ( q,l, q , l ) ∈ E *if* l = l+1 *and* q ∈ δ(q, w[l])*.*

Intuitively, a state q at a level may occur in several runs and only one vertex is needed to represent it, i.e., the vertex q, who is said to be on level . Note that by definition, there are at most |Q| vertices on each level. An edge ( q,l, q , l + 1) is an F*-edge* if (q, w[l], q ) ∈ F. An infinite sequence of vertices γ = q0, 0 q1, 1··· is called an ω*-branch* of GA,w if q0 = ι and for each ∈ N, we have ( q, , q+1, + 1) ∈ E. We can observe that there is a bijection between the set of runs of A on w and the set of ω-branches in GA,w. In fact, to a run ρ = q0q1 ··· of A over w corresponds the ω-branch ˆρ = q0, 0 q1, 1··· and, symmetrically, to an ω-branch γ = q0, 0 q1, 1··· corresponds the run γˆ = q0q1 ··· . Thus w is accepted by A if and only if there exists an ω-branch in GA,w that takes F-edges infinitely often.

In the remainder of this section, we will introduce the algorithms for computing the successors of the current states inside different types of SCCs, with the help of run DAGs. We fix an NBA A = (Q, ι, δ, F) and a word w ∈ Σω. We let Q = {q1,...,qn} and apply a total order on Q such that qi qj if i<j. Let S ⊆ Q, ∈ N, be the set of states reached at the level in the run DAG GA,w; we assume that this sequence S0, ··· , S, ··· is available as a *global* variable during the computations of every SCC where S0 = {ι} and S+1 = δ(S, w[ ]).

When determinizing the given NBA A, we classify its SCCs into three types, namely inherently weak SCCs (IWCs), deterministic-accepting SCCs (DACs) and nondeterministic-accepting SCCs (NACs). We assume that all DACs and NACs are *not* inherently weak, otherwise they will be classified as IWCs.

In our determinization construction, every level in GA,w corresponds to a state in our constructed DELA AE while reading the ω-word w. Let m be the state of AE at level . The computation of the successor m+1 of m for the letter w[ ] will be divided into the successor computation for states in IWCs, DACs and NACs independently. Then the successor m+1 is just the Cartesian product of these successors. In the remainder of this section, we present how to compute the successors for the states in each type of SCCs.

#### **3.1 Successor Computation Inside IWCs**

As we have seen, GA,w contains all runs of A over w, including those within DACs and NACs. Since we want to compute the successor only for IWCs, we focus on the states inside the IWCs and ignore other states in DACs and NACs. Let W be the set of states in all IWCs and WA ⊆ W be the set of states in all accepting IWCs.

For the run DAG GA,w, we use a pair of sets of states (P, O) ∈ 2W × 2WA to represent the set of IWC states reached in GA,w at level . The set P is used to keep track of the states in W reached at level , while O, inspired by the breakpoint construction used in [31], keeps only the states reached in WA, that is, it is used to track the runs that stay in accepting IWCs. Since by definition each cycle inside an accepting IWC must visit an accepting transition, for each run tracked by O we do not need to remember whether we have taken an accepting transition: it suffices to know whether the run is still inside some accepting IWC or whether the run has left them.

We now show how to compute the sets (P, O) along w. For level 0, we simply set P0 = {ι} ∩ W and O0 = ∅. For the other levels, given (P, O) at level ∈ N, the encoding (P+1, O+1) for the next level + 1 is defined as follows:

– P+1 = S+1 ∩W, i.e., P+1 keeps track of the W-states reached at level + 1; – if O = ∅, then O+1 = δ(O, w[ ]) ∩ WA, otherwise O+1 = P+1 ∩ WA.

Intuitively, the O-set keeps track of the runs that stay in the accepting IWCs. So if O = ∅, then O+1 maintains the runs remaining in some accepting IWC; otherwise, O = ∅ means that at level all runs seen so far in the accepting IWCs have left them, so we can just start to track the new runs that entered the accepting IWCs but were not tracked yet.

2 - 3 4 On the right we show the fragment of the run DAG GA,aω for the NBA A shown in Fig. 1 and its IWCs; we have W = {q2, q3, q6} and WA = {q2, q3}. The set P contains all states q at level ; the set O contains the underlined ones. As a concrete application of the construction given above, from P3 = {q2, q3} and O3 = δ(O2, a) ∩ WA = {q3}, at level 4 we get P4 = {q2, q3, q6} and O4 = δ(O3, a) ∩ WA = {q2}.

It is not difficult to see that checking whether w is accepted reduces to check whether the number of empty O-sets is finite. We assign color 1 to the transition from

(P, O) to (P+1, O+1) via w[ ] if O = ∅, otherwise we assign color 2. Lemma 1 formalizes the relation between accepting runs staying in accepting IWCs and the colors we get from our construction.

**Lemma 1.** *(1) There exists an accepting run of* A *over* w *eventually staying in an accepting IWC if and only if we receive color* 1 *finitely many times when constructing the sequence* (P0, O0)···(P, O)··· *while reading* w*. (2) The number of possible* (P, O) *pairs is at most* 3|W| *.*

The proof idea is trivial: an accepting run ρ that stays in an accepting IWC will make the O-set contain ρ forever and we always get color 2 from some point on. A possible pair (P, O) can be seen as choosing a state from W, which can be from W\P, P ∩O and P \O, respectively. It thus gives at most 3|W| possibilities.

To ease the construction for the whole NBA A, we make the above computation of successors available as a function weakSucc, which takes as input a pair of sets (P, O) and a letter a, and returns the successor (P , O ) and the corresponding color c ∈ {1, 2} for the transition ((P, O), a,(P , O )).

The construction we gave above works on all IWCs at the same time; considering IWCs separately does not improve the resulting complexity. If there are two accepting IWCs with n1 and n2 states, respectively, then the number of possible (P, O) pairs for the two IWCs is 3n1 and 3n2 , respectively. When combining the pairs for each IWC together, the resulting number of pairs in the Cartesian product is 3n1 × 3n2 = 3n1+n2 , which is the same as considering them together. On the other hand, for each accepting IWC, we need to use two colors, so we need 2 ·i colors in total for i accepting IWCs, instead of just two colors by operating on all IWCs together. Hence, we prefer to work on all IWCs at once.

#### **3.2 Successor Computation Inside DACs**

In contrast to IWCs, we do not work on all DACs at once but we process each DAC separately. This is because there may be nondeterminism between DACs: a run in a DAC may branch into multiple runs that jump to different DACs, which requires us to resort to a Safra-Piterman's construction [33,36] when considering all DACs at once. Working on each DAC separately, instead, allows us to take advantage of the internal determinism: for a given DAC D, the transition relation δ inside D, denoted as δD = (D × Σ × D) ∩ δ, is now deterministic.

Although every run ρ entering D can have only one successor in D, ρ may just leave D while new runs can enter D, which makes it difficult to check whether there exists an accepting run that remains trapped into D. In order to identify accepting runs staying in D, we identify the following two rules for distinguishing runs that come to D by means of *unique* labelling numbers: **(1)** the runs already in D have precedence over newly entering runs, thus the latter get assigned a higher number. In practice, the labelling keeps track of the relative order of entering D, thus the lower the labelling value is, the earlier the run came to D; **(2)** when two runs in D merge, we only keep the run that came to D earlier, i.e., the run with lower number. If two runs enter D at the same time, we let them enter according to the total state order for their respective entry states.

We use a level-labelling function g : D → {1, ··· , 2·|D|}∪ {∞} to encode the set of D-states reached at level of the run DAG GA,w. Here we use g(q) = ∞ to indicate that the state q ∈ D is not reached by A at level .

At level 0, we set g0(q) = ∞ for every state q ∈ D \ {ι}, and g0(ι) = 1 if ι ∈ D. Note that the SCC that ι resides in can be an IWC, a DAC or a NAC.

For a given level-labelling function g, we will make { q ∈ D | g(q) = ∞ } = S ∩ D hold, i.e., tracing correctly the set of D-states reached by A at level ; we denote the set g(D) \ {∞} by β(g), so β(g) is the set of unique labelling numbers at level . By the construction given below about how to generate g+1 from g on reading w[ ], we ensure that β(g) ⊆ {1, ··· , 2 · |D|} for all ∈ N.

We now present how to compute the successor level-labelling function g+1 of g on letter w[ ]. The states reached by A at level + 1, i.e., S+1 ∩D, may come from two sources: some state may come from states not in D via transitions in δ \ δD; some other via δD from states in S ∩ D. In order to generate g+1, we first compute an intermediate level-labelling function g +1 as follows.

1. To obey Rule **(2)**, for every state q ∈ δD(S ∩ D, w[ ]), we set

$$\mathfrak{g}'\_{\ell+1}(q') = \min \{ \mathfrak{g}\_{\ell}(q) \mid q \in S\_{\ell} \cap \mathbf{D} \land \delta\_D(q, w[\ell]) = q' \}.$$

That is, when two runs merge, we only keep the run with the lower labelling number, i.e., the run entered in D earlier.

2. To respect Rule **(1)**, we set g +1(q ) = |D|+i for the i-th newly entered state q ∈ (S+1 ∩ D) \ δD(S ∩ D, w[ ]) and the states q are ordered by the total order of the states. Since every state in δD(S ∩ D, w[ ]) is on a run that already entered D, its labelling has already been determined by the case 1.

It is easy to observe that in order to compute the transition relation between two consecutive levels, we only need to know the labelling at the previous level. More precisely, we do not have to know the exact labelling numbers, since it suffices to know their relative order. Therefore, we can compress the level-labelling g +1 to g+1 as follows. Let ord: β(g +1) → {1, ··· , |β(g +1)|} be the function that maps each labelling value in β(g +1) to its relative position once the values in β(g +1) have been sorted in ascending order. For instance, if β(g +1) = {2, 4, 7}, then ord = {2 → 1, 4 → 2, 7 → 3}. Then we set g+1(q) = ord(g +1(q)) for each q ∈ S+1 ∩ D, and g+1(q ) = ∞ for each q ∈ D \ S+1. In this way, all level-labelling functions g we use are such that β(g) ⊆ {1, ··· , |D|}.

The intuition behind the use of these level-labelling functions is that, if we always see a labelling number h in the intermediate level-labelling g for all ≥ k after some level k, we know that there is a run that eventually stays in D and is eventually always labelled with h. To check whether this run also visits infinitely many accepting transitions, we will color every transition e = (g, w[ ], g+1). To decide what color to assign to e, we first identify which runs have merged with others or got out of D (corresponding to *bad* events and *odd* colors) and which runs still continue to stay in D and take an accepting transition (corresponding to *good* events and *even* colors).

The bad events correspond to the discontinuation of labelling values between g and g +1, defined as B(e) = β(g) \ β(g +1). Intuitively, if a labelling value k exists in the set B(e), then the run ρ associated with labelling k merged with a run with lower labelling value k < k, or ρ left the DAC D. The good events correspond to the occurrence of accepting transitions in some runs, whose labelling we collect into G(e) = { k ∈ β(g) | ∃(q, w[ ], q ) ∈ F.g(q) = g +1(q ) = k = ∞ }. In practice, a labelling value k in G(e) indicates that we have seen a run with labelling k that visits an accepting transition. We then let B(e) = B(e) ∪ {|D| + 1} and G(e) = G(e) ∪ {|D| + 1} where the value |D| + 1 is used to indicate that no bad (i.e., no run merged or left the DAC) or no good (i.e., no run took an accepting transition) events happened, respectively.

In order to declare a sequence of labelling functions as accepting, we want the good events to happen infinitely often and bad events to happen only finitely often, when the runs with bad events have a labelling number lower than that of the runs with good events. So we assign the color c = min{2 · min B(e) − 1, 2 · min G(e)} to the transition e. Since the labelling numbers are in {1, ··· , |D|}, we have that c ∈ {1, ··· , 2 · |D| + 1}. The intuition why we assign colors in this way is given as the proof idea of the following lemma.

**Lemma 2.** *(1) An accepting run of* A *over* w *eventually stays in the DAC* D *if and only if the minimal color* c *we receive infinitely often is even. (2) The number of possible labelling functions* g *is at most* 3 · |D|!*.*

The proof idea is as follows: an accepting run ρ on the word w that stays in D will have stable labelling number, say k ≥ 1, after some level since the labelling value cannot increase by construction and is finite. So all runs on w that have labelling values lower than k will not leave D: if they would leave or just merge with other runs, their labelling value vanishes, so ord would decrease the value for ρ. This implies that the color we receive afterwards infinitely often is either 1) an odd color larger than 2k, due to vanishing runs with value at least k + 1 or simply because no bad or good events occur, or 2) an even color at most 2k, depending on whether there is some run with value smaller than ρ also taking accepting transitions. Thus the minimum color occurring infinitely often is even. The number of labelling functions g is bounded by |D| i=0 |D| i · i! ≤ 3 · |D|!.

The fragment of the DAG GA,aω shown on the right is relative to the only DAC D = {q4, q5}. The value of g (q), g(q) and the corresponding ord is given by the mapping near each state q; as a concrete application of the construction given above, consider how to get g4 from g3, defined as g3(q4) = 1 and g3(q5) = ∞: since q5 ∈ δD(S3 ∩ D, a), according to case 1 we define g 4(q5) = 1 because q5 = δD(q4, a) and g3(q4) = 1;

3 - 4 5 q4, 3 → 1 q5, 1 → 1 q4, 3 → 2 q4, 1 → 1 q5, 2 → 2

since q4 ∈ (S4 ∩ D) \ δD(S3 ∩ D, a), then case 2 applies, so g 4(q4) = 3. The function ord is ord = [1 → 1, 3 → 2], thus we get g4(q4) = 2 and g4(q5) = 1. As bad/good sets for the transition e = g3 a−→ g4, we have B(e) = ∅∪{3} while G(e) = {1}∪{3}, so the resulting color is 2.

Again, we make the above computation of successors available as a function detSucc, which takes as input the DAC D, a labelling g and a letter a, and returns the successor labelling g and the color c ∈ {1, ··· , 2 · |D| + 1}.

#### **3.3 Successor Computation Inside NACs**

The computation of the successor inside a NAC is more involved since runs can branch, so it is more difficult to check whether there exists an accepting run. To identify accepting runs, researchers usually follow the Safra-Piterman's idea [33,36] to give the runs that take more accepting transitions the precedence over other runs that join them. We now present how to compute labelling functions encoding this idea for NACs, instead of the whole NBA. Differently to the previous case about DACs, the labelling functions we use here use lists of numbers, instead of single numbers, to keep track of the branching, merging and new incoming runs. This can be seen as a generalization of the numbered brackets used in [35] to represent ordinary Safra-Piterman's trees. Differently from this construction, in our setting the main challenge we have to consider is how to manage correctly the newly entering runs, which are simply not occurring in [35] since there the whole NBA is considered. The fact that runs can merge, instead, is a common aspect, while the fact that a run ρ leaves the current NAC can be treated similarly to dying out runs in [35]. Below we assume that N is a given NAC; we denote by δN = (N × Σ × N) ∩ δ the transition function δ inside N.

To manage the branching and merging of runs of A over w inside a NAC, and to keep track of the accepting transitions taken so far, we use level-labelling functions as for the DAC case. For a given NAC N, the functions we use have lists of natural numbers as codomain; more precisely, let LN be the set of lists taking value in the set {1, ··· , 2 · |N|}, where a list is a finite sequence of values in ascending order. Given two lists [v1, ··· , vk] and [v 1, ··· , v k-], we say that [v1, ··· , vk] is a prefix of [v 1, ··· , v k- ] if 1 ≤ k ≤ k and for each 1 ≤ j ≤ k, we have vj = v j . Note that the empty list *is not* a prefix of any list. Given two lists [v1, ··· , vk] and [v 1, ··· , v k- ], we denote by [v1, ··· , vk][v 1, ··· , v k- ] their concatenation, that is the list [v1, ··· , vk, v 1, ··· , v k- ]. Moreover, we define a total order on lists as follows: given two lists [v1, ··· , vk] and [v 1, ··· , v k- ], we order them by padding the shorter of the two with ∞ in the rear, so to make them of the same length, and then by comparing them by the usual lexicographic order. This means, for instance, that the empty list [] is the largest list and that [1, 3, 5] is smaller than [1, 3] but larger than [1, 2]. The lists help to keep track of the branching history from their prefixes, such as [1, 2] is branched from [1].

As done for DACs, we use a level-labelling function t : N → LN to encode the set of N-states reached in the run DAG GA,w at level . We denote by β(t) the set of non-empty lists in the image of t, that is, β(t) = { t(q) | q ∈ N ∧t(q) = [] }. We use the empty list [] for the states in N that do not occur in the vertexes of GA,w at level , so β(t) contains only lists associated with states that A is currently located at. Similarly to the other types of SCCs, at level 0, we set t0(ι) = [1] if ι ∈ N, and t0(q) = [] for each state q ∈ N \ {ι}.

To define the transition from t to t+1 through the letter w[ ], we use again an intermediate level-labelling function t +1 that we construct step by step as follows. We start with t +1(q) = [] for each q ∈ N and with the set of unused numbers U = { u ≥ 1 | u /∈ β(t) }, i.e., the numbers not used in β(t).

1. For every state q ∈ δN (S∩N, w[ ]), let Pq- = { q ∈ S∩N | (q, w[ ], q ) ∈ δN } be the set of currently reached predecessors of q , and Cq- = ∅. For each q ∈ Pq- , if (q, w[ ], q ) ∈ F, then we add t(q)[u] to Cq- , where u = minU, and we remove u from U, so that each number in U is used only once; otherwise, for (q, w[ ], q ) ∈ δN \F, we add t(q) to Cq- . Lastly, we set t +1(q ) = min Cq- , where the minimum is taken according to the list order.

Intuitively, if a run ρ can branch into two kinds of runs, some via accepting transitions and some others via nonaccepting transitions at level + 1, then we let those from nonaccepting transitions inherit the labelling from ρ, i.e., t(ρ[ ]); for the runs taking accepting transitions we create a new labelling t(ρ[ ])[u]. In this way, the latter get precedence over the former. Moreover, if a run ρ has received multiple labelling values, collected in Cρ[+1], then it will keep the smallest one, by t +1(ρ[ + 1]) = min Cρ[+1].

2. For each state q ∈ (S+1 ∩ N) \ δN (S ∩ N, w[ ]) taken according to the state order -, we first set t +1(q )=[u], where u = minU, and then we remove u from U, so we do not reuse the same values. That is, we give the newly entered runs lower precedence than those already in N, by means of the larger list [u].

We now need to prune the lists in β(t +1) and recognize good and bad events. Similarly to DACs, a bad event means that a run has left N or has been merged with runs with smaller labelling, which is indicated by a discontinuation of a labelling between β(t) and β(t +1). For the transition e = (t, w[ ],t+1) we are constructing, to recognize bad events, we put into the set B(e) the number |N| + 1 and all numbers in β(t) that have disappeared in β(t +1), that is, B(e) = {|N| + 1}∪{ v ∈ N | v occurs in β(t) but not in β(t +1) }.

Differently from the good events for DACs, which require to visit an accepting transition, we need all runs branched from a run to visit an accepting transition, which is indicated by the fact that there are no states labelled by t +1 with some list l ∈ β(t) but there are extensions of l associated with some state. To recognize good events, let G(e) = {|N| + 1} and t +1 be another intermediate labelling function. For each q ∈ S+1 ∩ N, consider the list t +1(q ): if for each prefix [v1, ··· vk] of t +1(q ) we have [v1, ··· vk] ∈ β(t +1), then we set t +1(q ) = t +1(q ). Otherwise, let [v1, ··· vk¯] ∈/ β(t +1) be the shortest prefix of t +1(q ) not in β(t +1); we set t +1(q )=[v1, ··· vk¯] and add vk¯ to G(e). Setting t +1(q ) = [v1, ··· vk¯] in fact corresponds, in the Safra's construction [36], to the removal of all children of a node N for which the union of the states in the children is equal to the states in N. Lastly, similarly to the DAC case, we set t+1(q) = ord(t +1(q)) for each q ∈ S+1 ∩ N and t+1(q ) = [] for each q ∈ N \ S+1, where ord([v1, ··· , vk]) = [ord(v1), ··· , ord(vk)]. Regarding the color to assign to the transition e, we just assign the color c = min{2 · min G(e), 2 · min B(e) − 1}.

**Lemma 3.** *(1) An accepting run of* A *over* w *eventually stays in the NAC* N *if and only if the minimal color* c *we receive infinitely often is even. (2) The number of possible labelling functions* t *is at most* 2 · (|N|!)2*.*

Similarly to DACs, also for NACs we have handled each NAC independently. The reason for this is that this potentially reduces the complexity of the single cases: assume that we have two NACs N1 and N2. If we apply the Safra-Piterman's construction directly to N1 ∪ N2, we might incur in the worst-case complexity 2 · ((|N1| + |N2|)!)2, as mentioned in the introduction. However, if we determinize them separately, then the worst complexity for each NAC Ni is 2 ·(Ni!)2, for an overall 4 ·(|N1|! · |N2|!)2, much smaller than 2 ·((|N1| + |N2|)!)2.

As usual, we make the above construction available as a function nondetSucc, which takes as input the NAC N, a labelling t and a letter a, and returns the successor labelling t and the corresponding color c ∈ {1, ··· , 2 · |N| + 1}.

0 - 1 2 q0, [1] q0, [1, 2] q1, [1] q0, [1] q1, [1] Similarly to the constructions for other SCCs, we show on the right the fragment of run DAG GA,aω for the NAC N = {q0, q1}, with q0 q1. The construction of t1 is easy, so consider its a-successor t2: we start with U = {3, 4, ···}; for q0, we have Pq0 = {q0, q1} and Cq0 = {[1, 2, 3], [1]}, hence t 2(q0) = [1, 2, 3]. For q1, we get Pq1 = {q0} and Cq1 = {[1, 2]}, so t 2(q1) = [1, 2]. Thus, for e = (t1, w[1],t2), we have B(e) = {3} while G(e) = {1, 3}, since both lists in β(t 2) = {[1, 2], [1, 2, 3]} are missing the prefix [1], so we get t2(q0) = t2(q1) = [1] and color c = 2.

#### **4 Determinization of NBAs to DELAs**

In this section, we fix an NBA A = (Q, ι, δ, F) with n = |Q| states and we show how to construct an equivalent DELA AE = (QE, ιE, δE, Γ E, pE,AccE), by using the algorithms developed in the previous section. We assume that A has {D1, ··· , Dd} as set of DACs and {N1, ··· , Nk} as set of NACs.

When computing the successor for each type of SCCs while reading a word w, we just need to know the set S of states reached at the current level and the letter a ∈ Σ to read. We can ignore the actual level , since if S = S- , then their successors under the same letter will be the same. As mentioned before, every state of AE corresponds to a level of GA,w. We call a state of AE a *macrostate* and a run of AE a *macrorun*, to distinguish them from those of A.

**Macrostates** QE**.** Each macrostate consists of the pair (P, O) for encoding the states in IWCs, a labelling function gi : Di → {1, ··· , |Di |} ∪ {∞} for the states of each DAC Di and a labelling function t j : Nj → LNj for each NAC Nj , without the explicit level number. The initial macrostate ι E of AE is the encoding of level 0, defined as the set {(P0, O0)}∪{ gi 0 | Di is a DAC }∪{ t j 0 | Nj is a NAC }, where each encoding for the different types of SCCs is the one for level 0.

We note that ι must be present in one type of SCCs. In particular, if ι is a transient state, then {ι} is classified as an IWC.

**Transition Function** δE**.** Let m be the current macrostate in QE and a ∈ Σ be the letter to read. Then we define m = δE(m, a) as follows.

Note that the set S of the current states of A used by the different successor functions is implicitly given by the sets P, { q ∈ Di | gi (q) = ∞ } for each DAC Di and { q ∈ Nj | t j (q) = [] } for each NAC Nj in the current macrostate m.

**Color Set** Γ E **and Coloring Function** pE. From the constructions given in Sect. 3, we have two colors from the IWCs, 2 · |Di | + 1 colors for each DAC Di , and 2 · |Nj | + 1 colors for each NAC Nj , yielding a total of at most 3 · |Q| colors. Thus we set Γ E = {0, 1, ··· , 3 · |Q|} with color 0 not being actually used.

Regarding the color to assign to each transition, we need to ensure that the colors returned by the single SCCs are treated separately, so we transpose them. For a transition e = (m, a, m ) ∈ δE, we define the coloring function pE as follows.

Intuitively, we make the colors returned for each SCC not overlap with those of other SCCs without changing their relative order. In this way, we can still independently check whether there exists an accepting run staying in an SCC.

**Acceptance Formula** AccE**.** We now define the acceptance AccE, which is basically the *disjunction* of the acceptance formula for each different types of SCCs, after transposing them. Regarding the IWCs, we trivially define AccE W = Fin(1), since this is the acceptance formula for IWCs; as said before, color 0 is not used.

For DACs and NACs, the definition is more involved. For instance, regarding the DAC Di , we know that all returned colors are inside {1, ··· , 2 · |Di | + 1}. According to Lemma 2, an accepting run eventually stays in Di if and only if the minimum color that we receive infinitely often is even. Thus, the acceptance formula for the above lemma is parity(|Di |) = -|Di| c=1( c j=1 Fin(2j − 1) ∧ Inf(2c)). Let bi = 2+ h<i(2 · |Dh| + 1) be the base number for the colors of Di , which is also the number of colors already used by IWCs and the DACs Dh with h<i. Since we have added the base number bi to every color of Di , we then have the acceptance formula AccE Di = -|Di| c=1( c j=1 Fin(2j − 1 + bi) ∧ Inf(2c + bi)).

For each NAC Nj , the colors we receive are in {1, ··· , 2 · |Nj | + 1}. Let bj =2+ 1≤h≤d(2 · |Dh| + 1) + h<j (2 · |Nj | + 1) be the base number for Nj . Similarly to the DAC case, for each NAC Nj , we let AccE Nj = -|Nj | c=1( c i=1 Fin(2i− 1 + bj ) ∧ Inf(2c + bj )).

The acceptance formula for AE is AccE = AccE W ∨ d i=1 AccE Di ∨ k j=1 AccE Nj .

Consider again the NBA A given in Fig. 1 and its various SCCs. As acceptance formula for the constructed DELA, it is the disjunction of the formulas AccE W = Fin(1); AccE D = -2 c=1( c j=1 Fin(2j − 1 + 2) ∧ Inf(2c + 2)), since the base number for D is 2; and AccE N = -2 c=1( c i=1 Fin(2i − 1 + 7) ∧ Inf(2c + 7)), since 7 is the base number for N.

The construction given in this section is correct, as stated by Theorem 1.

**Theorem 1.** *Given an NBA* A *with* n = |Q| *states, let* AE *be the DELA constructed by our method. Then (1)* L(AE) = L(A) *and (2)* AE *has at most* 3|W| · d i=1 3 · |Di |! · k j=1 2 · (|Ni |!)2 *macrostates and* 3n + 1 *colors.*

Obviously, if d = k = 0, A is a weak BA [32]. If k = 0, A is an elevator BA, a new class of BAs recently introduced in [19] which have only IWCs and DACs, a strict superset of semi-deterministic BAs (SDBAs) [10]. SDBAs will behave *deterministically* after seeing acceptance transitions. An elevator BA that is not an SDBA can be obtained from the NBA A shown in Fig. 1 by setting q2 as initial state and by removing all states and transitions relative to the NAC.

It is known that the lower bound for determinizing SDBAs is n! [14,27]. Then the determinization complexity of weak BAs and elevator BAs can be easily improved exponentially as follows.

**Corollary 1.** *(1) Given a weak B¨uchi automaton* A *with* n = |Q| *states, the DELA constructed by our algorithm has at most* 3n *macrostates. (2) Given an* *elevator B¨uchi automaton* A *with* n = |Q| *states, our algorithm constructs a DELA with* Θ(n!) *macrostates; it is asymptotically optimal.*

The upper bound for determinizing weak BAs is already known [5]. Elevator BAs are, to the best of our knowledge, the *largest* subclass of NBAs known so far to have determinization complexity Θ(n!).

The acceptance formula for an SCC can be seen as a parity acceptance formula with colors being shifted to different ranges. A parity automaton can be converted into a Rabin one without blow-up of states and transitions [16]. Since AccE is a disjunction of parity acceptance formulas, Theorem 2 then follows.

**Theorem 2.** *Let* AE *be the constructed DELA for the given NBA* A*. Then* AE *can be converted into a DRA* AR *without blow-up of states and transitions.*

**Translation to Deterministic Parity Automata (DPAs).** We note that there is an *optimal* translation from a DRA to a DPA described in [7], implemented in Spot via the function acd transform [8].

#### **5 Empirical Evaluation**

To analyze the effectiveness of our Divide-and-Conquer determinization construction proposed in Sect. 3, we implemented it in our tool COLA, which is built on top of Spot [12]. The source code of COLA is publicly available from https://github.com/liyong31/COLA. We compared COLA with the official versions of Spot [12] (2.10.2) and Owl [23] (21.0). Spot implements the algorithm described in [35], a variant of [33] for transition-based NBAs, while Owl implements the algorithms described in [28,29], both constructing DPAs as result. To make the comparison fair, we let all tools generate DPAs, so we used the command autfilt --deterministic --parity=min\ even -F file.hoa to call Spot and owl nbadet -i file.hoa to call Owl. Recall that we use the function acd transform [8] from Spot for obtaining DPAs from our DRAs. The tools above also implement optimizations for reducing the size of the output DPA, like simulation and state merging [29], or stutter invariance [22] (except for Owl); we use the default settings for all tools. We performed our experiments on a desktop machine equipped with 16GB of RAM and a 3.6 GHz Intel Core i7-4790 CPU. We used BenchExec1 [3] to trace and constrain the tools' executions: we allowed each execution to use a single core and 12 GB of memory, and imposed a timeout of 10 min. We used Spot to verify the results generated by three tools and found only outputs equivalent to the inputs.

As benchmarks, we considered all NBAs in the HOA format [1] available in the automata-benchmarks repository.2 We have pre-filtered them with autfilt to exclude all deterministic cases and to have nondeterministic BAs, obtaining in total 15,913 automata coming from different sources in literature.

The artifact with tools, benchmarks, and scripts to run the experiments and generate the plots is available at [25].

1 https://github.com/sosy-lab/benchexec/.

2 https://github.com/ondrik/automata-benchmarks/.

**Fig. 2.** The cactus plot for the determinization of NBAs from automata-benchmarks.

**Fig. 3.** States comparison for the determinization of NBAs from automatabenchmarks. (Color figure online)

In Fig. 2 we show a cactus plot reporting how many input automata have been determinized by each tool, over time. As we can see, COLA works better than Spot, with COLA solving in total 15,903 cases and Spot 15,862 cases, with Owl solving in total 15,749 cases and taking more time to solve as many instances as COLA and Spot. From the plot given in Fig. 2 we see that COLA is already very competitive with respect to its performance.

In Fig. 3 we show the number of states of the generated DPAs. In the plot we indicate with the bold dashed line the maximum number of states of the automata produced by either of the two tools, and we place a mark on the upper or right border of the plot to indicate that one tool has generated an automaton with that size while the other tool just failed. The color of each mark represents how many instances have been mapped to the corresponding point. As the plots show, Spot and COLA generate automata with similar size, with COLA being more likely to generate smaller automata, in particular for larger outputs. Owl, instead, very frequently generates automata larger than COLA. In fact, on the 15,710 cases solved by all tools, on average COLA generated 44 states, Spot 65, and Owl 87. If we compare COLA with just one tool at a time, on the 15,854 cases solved by both COLA and Spot, we have 125 states for COLA and 246 for Spot; on the 15,749 cases solved by both COLA and

**Fig. 4.** Acceptance sets comparison for the determinization of NBAs from automatabenchmarks. (Color figure online)

**Table 1.** Pearson correlation coefficients for the automata-benchmarks experiments.

Owl, we have 45 states for COLA and 88 for Owl. A similar situation occurs for the number of transitions, so we omit it.

Lastly, in Fig. 4 we compare the number of acceptance sets (i.e., the colors in Definition 1) of the generated DPAs; more precisely, we consider the integer value occurring in the mandatory Acceptance: INT acceptance-cond header item of the HOA format [1], which can be 0 for the automata with all or none accepting transitions. From the plots we can see that COLA generates more frequently DPAs with a number of colors that is no more than the number used by Spot, as indicated by the yellow/red marks on (10,394 cases) or above (5,495 cases) the diagonal. Only in very few cases COLA generates DPAs with more colors than Spot (22 cases), as indicated by the few blue/greenish marks below the diagonal. Regarding Owl, however, from the plot we can clearly see that COLA uses almost always (15,840 cases) fewer colors than Owl; the only exception is for the mark at (0, 0) representing 63 cases.

The number and sizes of SCCs influence the performance of COLA, so we provide some statistics about the correlation between these and the runtime and size of the generated DPA. By combining the execution statistics with the input SCCs and states, we get the Pearson correlation coefficients shown in Table 1. Here the larger the number in a cell is, the stronger the positive correlation between the element that the row and the column represent. From these coefficients we can say that there is a quite strong positive correlation between the number of states and of SCCs and the running time, but not for the average SCC size; regarding the output states, the situation is similar but much weaker.

We also considered a second set of benchmarks – 644 NBAs generated by Spot's ltl2tgba on the LTL formulas considered in [23], as available in the

**Fig. 5.** The family of NBAs *An* with Σ = *{*0, 1, *···* , n*}*.

Owl's repository at https://gitlab.lrz.de/i7/owl. The outcomes for these benchmarks are similar, but a bit better for COLA, to the ones for automatabenchmarks, so we do not present them in detail.

#### **6 Related Work**

To the best of our knowledge, our determinization construction is the *first* algorithm that determinizes SCCs *independently* while taking advantage of different structures of SCCs, which is the main difference between our algorithm and existing works. We illustrate other minor differences below.

Different types of SCCs, like DACs and IWCs, are also taken with special care in [29] as in our work, modulo the handling details. However, the work [29] does not treat them independently as the labelling numbers in those SCCs still have relative order with those in other SCCs. Thus their algorithm can be exponentially worse than ours (cf. Theorem 3) and performs not as well as ours in practice; see the comparison with Owl in Sect. 5. The determinization algorithm given in [14] for SDBAs is a special case of the one presented in [35] for NBAs, which gives precedence to the deterministic runs seeing accepting transitions earlier, while we give precedence to runs that enter DACs earlier. More importantly, the algorithm from [14] does not work when there is nondeterminism between DACs, while our algorithm overcomes this by considering DACs separately and by ignoring runs going to other SCCs.

Current works for determinization of general NBAs, such as [18,21,28,35,36, 38] can all be interpreted as different flavours of the Safra-Piterman based algorithm. Our determinization of NACs is also based on Safra-trees and inspired by Spot, except that we may have newly arriving states from other SCCs while other works only need to consider the successors from the current states in the Safra-tree. The modular approach for determinizing B¨uchi automata given in [17] builds on reduced split trees [21] and can construct the deterministic automaton with a given tree-width. The algorithm constructs the final deterministic automaton by running in parallel the NBA for all possible tree-widths, rather than working on SCCs independently as we do in this work.

Compared to the algorithms operating on the whole NBA, our algorithm can be exponentially better on the family of NBAs shown in Fig. 5, as formalized in Theorem 3; we can encounter some variation of this family of NBAs when working with fairness properties. The intuition is that we take care of the DACs {qi}n i=1 independently, so for each of them we have only two choices: either the run is in the DAC, or it is not in the DAC; resulting in a single exponential number of combinations. Existing works [14,21,28,33,35,36] order the runs entering the DACs based on when they visit accepting transitions, in which every order corresponds to a permutation of {q1, ··· , qn}.

**Theorem 3.** *There exists a family of NBAs* An *with* n + 2 *states for which the algorithms in [14,21,28,33,35,36] give a DPA with at least* n! *macrostates while ours gives a DELA with at most* 2n+2 *macrostates.*

In practice, for each NBA An, n ≥ 3, COLA produces a DELA/DPA with n macrostates, while both Spot and Owl give a DPA with n! + 1 macrostates.

## **7 Conclusion and Future Work**

We proposed a divide-and-conquer determinization construction for NBAs that takes advantage of the structure of different types of SCCs and determinizes them independently. In particular, our construction can be exponentially better than classical works on a family of NBAs. Experiments showed that our algorithm outperforms the state-of-the-art implementations regarding the number of states and transitions on a large set of benchmarks. To summarize, our divide-andconquer determinization construction is very *practical*, being a good complement to existing theoretical approaches.

Our divide-and-conquer approach for NBAs can also be applied to the complementation problems of NBAs. By Proposition 1, w is not accepted by A if and only if there are no accepting runs staying in an SCC. Thus we can construct a *generalized* B¨uchi automaton with a conjunction of Inf(i) as the acceptance formula to accept the complement language Σω \ L(A) of A; the generalized B¨uchi automaton in fact takes the *intersection* of the complement language of each type of SCCs. For complementing IWCs, we use the same construction as determinization except that the acceptance formula will be Inf(1). For complementing DACs, we can borrow the idea of NCSB complementation construction [4] which complements SDBAs in time 4n. For complementing NACs, we just adapt the *slice-based* complementation [21] of general NBAs. We leave the details of this divide-and-conquer complementation construction for NBAs as future work.

**Acknowledgement.** We thank the anonymous reviewers for their valuable suggestions to this paper. This work is supported in part by the National Natural Science Foundation of China (Grant Nos. 62102407 and 61836005), NSF grants IIS-1527668, CCF-1704883, IIS-1830549, CNS-2016656, DoD MURI grant N00014-20-1-2787, and an award from the Maryland Procurement Office.

This project has received funding from the European Union's Horizon 2020 research and innovation programme under the Marie Sklodowska-Curie grant agreement No 101008233.

#### **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

## **From Spot 2.0 to Spot 2.10: What's New?**

Alexandre Duret-Lutz1(B) , Etienne Renault1 , Maximilien Colange2 , Florian Renkin1 , Alexandre Gbaguidi Aisse2, Philipp Schlehuber-Caissier1 , Thomas Medioni2, Antoine Martin1 , J´erˆome Dubois1, Cl´ement Gillard2,

and Henrich Lauko2

1 LRDE, EPITA, Le Kremlin-Bicˆetre, France {adl,renault,frenkin,philipp<EMAIL_ADDRESS>2 Bicˆetre, France

**Abstract.** Spot is a C**++**17 library for LTL and ω-automata manipulation, with command-line utilities, and Python bindings. This paper summarizes its evolution over the past six years, since the release of Spot 2.0, which was the first version to support ω-automata with arbitrary acceptance conditions, and the last version presented at a conference. Since then, Spot has been extended with several features such as acceptance transformations, alternating automata, games, LTL synthesis, and more. We also shed some lights on the data-structure used to store automata. **Artifact:** https://zenodo.org/record/6521395.

#### **1 Availability, Purpose, and Evolution**

Spot is a library for LTL and ω-automata manipulation, distributed under a GPLv3 license. Its source code is available from https://spot.lrde.epita.fr/. We provide packages for some Linux distributions like Debian and Fedora, but other packages can also be found for Conda-Forge [17] (for Linux & Darwin), Arch Linux, FreeBSD...

Spot can be used via three interfaces: a C**++**17 library, a set of commandline tools that give easy access to many features of the library, and Python bindings, that makes prototyping and interactive work very attractive. Our web site now contains many examples of how to perform some tasks using these three interfaces, and we have a public mailing list for questions.

In our last tool paper [21], Spot 2.0 had just converted from being a library for working on Transition-based Generalized B¨uchi Automata and had become a library supporting ω-automata with arbitrary Emerson-Lei [22,41] acceptance conditions, as enabled by the development of the HOA format [5].

In the HOA format, transitions can carry multiple colors, and acceptance conditions are expressed as a positive Boolean formulas over atoms like Fin(i) or Inf(i) that tell if a color should be seen finitely or infinitely often for a run to be accepting. Table 1 gives some examples.

M. Colange, A. Gbaguidi Aisse, T. Medioni, C. Gillard and H. Lauko—Previously at LRDE.

S. Shoham and Y. Vizel (Eds.): CAV 2022, LNCS 13372, pp. 174–187, 2022. https://doi.org/10.1007/978-3-031-13188-2\_9

**Table 1.** Acceptance formulas corresponding to classical names.

While Spot 2.0 was able to read automata with arbitrary acceptance conditions, not all of its algorithms were able to support such a generality. For instance testing an automaton for emptiness or finding an accepting word, would only work on automata with "Fin-less" acceptance conditions. For other conditions, Spot 2.0 would rely on a procedure called remove fin() to convert automata with arbitrary acceptance conditions into "Fin-less" acceptance conditions [9]. This was ultimately fixed by developing a generic emptiness check [6]. Additionally the support for arbitrary acceptance conditions has allowed us to implement many useful algorithms; the most recent being the Alternating Cycle Decomposition [15,16] a powerful data structure with many applications (conversion to parity acceptance, degeneralization, typeness checks...)1.

There have been 56 releases of Spot since version 2.0, but only 10 of these are major releases. Releases are numbered 2.x.y where y is updated for minor upgrades that mostly fix bugs, and x is updated for major release that add new features. (The leading 2 would be incremented in case of a serious redesign of the API.) Table 2 summarizes the highlights of the various releases in chronological order. Not appearing in this list are many micro-optimizations and usability improvements that Spot has accumulated over the years.

#### **2 Use-cases of Spot, and Related Tools**

As it is a library, there are many ways to use Spot. We are mostly aware of such uses via citations2. Historical and frequent uses-cases are to use Spot for translating LTL formulas to automata (Winners of the sequential LTL and parallel LTL tracks of RERS'19 challenge [26] both used Spot to translate the properties into automata, many competitors on the Model Checking Contest [28] also use

1 https://spot.lrde.epita.fr/ipynb/zlktree.html.

2 Our previous tool paper [21] has over 250 citations according to Google scholar.

**Table 2.** Milestones in the history of Spot.

Spot this way), or to use it as a research/development toolbox, since it provides helper tools for generation of random formulas/automata, verification of LTLto-automata translation, simplifications, syntax conversions, etc. Nowadays, the algorithms for ω-automata implemented in Spot are often used as baseline for studying better algorithms [e.g., 18,25,32,33], but we also see some new applications built on top of ω-automata algorithms from Spot [e.g., 12,13].

The projects that have the largest intersections of features with Spot seem to be GOAL [43] and Owl [30]. These are two Java-based frameworks that deal with similar objects and provide a range of algorithms. Owl and Spot share a similar and traditional Unix view of the command-line experience, where multiple commands are expected to be chained with pipes, and they both communicate smoothly via the HOA format [5]. GOAL is centered on a graphical interface in which the user can edit automata, and apply algorithms listed in menu entries. Using GOAL from the command-line is possible by writing short scripts in a custom language.

As far as interfacing goes, the most important feature of Spot is probably that it exposes its algorithms and data structures in Python. Beside being usable as a glue language between various tools, this allows us (1) to leverage Python's ecosystem and (2) to quickly prototype new algorithms in Python.

#### **3 Automata Representation**

In this section and the next three, we focuses on how the storage of automata evolved to support alternation, games, and Mealy machines.

The main automaton class of Spot is called twa graph and inherits from the twa class. The letters twa stand for *Transition-based* ω-Automaton.

The class twa implements an abstract interface that allows on-the-fly exploration of an automaton similar to what had been present in Spot from the start: essentially, one can query the initial state, and query the transitions leaving any known state. In particular, before exploring the state-space of a twa, it is unknown how many states are reachable. Various subclasses of twa are provided in Spot, for instance to represent the state-space of Promela or Divine models [21]. Users may create subclasses, for instance to create a Kripke structure on-the-fly.3

The class twa graph, introduced in Spot 2.0, implements an explicit, graphbased, representation of an automaton, in which states and edges are designated by integers. This makes for a much simpler interface4 and usually simplifies the data structures used in algorithms (since states and edges can be used as indices in arrays). The data structure is best illustrated by using the show storage() method of the Python bindings, as shown by Fig. 1. A twa graph is stored as two C**++** vectors: a vector of states, and a vector of edges. For each state, the first vector stores two edge numbers: succ is the first outgoing edge, and succ tail is the last one. These number are indices into the edge vector, which stores five pieces of information per edge. Four of them are related to the identity of the

3 As demonstrated by https://spot.lrde.epita.fr/tut51.html.

4 Contrast on-the-fly and explicit APIs at https://spot.lrde.epita.fr/tut50.html.

**Fig. 1.** Internal representation of a twa graph as two vectors.

edge: src, dst, cond, acc are respectively the source, destination, guard, and color sets of the edge. The remaining field, next succ gives the next outgoing edge, effectively creating a linked list of all edges leaving a given state. There is no edge 0: this value is used as terminator for such lists. Outgoing edges of the same state are not necessarily adjacent in that structure. When a new edge is added to the automaton, it is simply appended to the edge vector, and the succ tail field of the state is used to update the previous end of the list.

To iterate over successors of state 1 in C**++** or Python, one can ignore the above linked list implementation and write one of the following loops:

The twa graph::out methods simply returns a lightweight temporary object which can be iterated upon using iterators that will follow the linked list. Then the object e is effectively a reference to a column of the edge vector.

As seen on Fig. 1, the automaton additionally stores an initial state (Spot only supports a single initial state), a number of colors (num sets), an acceptance condition, a list of atomic propositions (Spot only supports alphabets of the form 2*AP* ), and 10 fields storing structural properties of the automaton.

These property fields have only three possible values: they default to *maybe*, but can be set to *no* or *yes* by algorithms that work on the automaton. They can also be read and written in the HOA format. For instance if prop universal is set to *yes*, it means that automaton does not have any existential choice (a.k.a. non-determinism). Spot's *is deterministic()* algorithm can return in constant time if prop universal is known, otherwise it will inspect the automaton and set that property before returning, so that the next call to *is deterministic()* will be instantaneous. Some algorithms know how to take advantage of any hint they get from those properties: for instance the product() of two automata is optimized to use fewer colors when one of the arguments is known to be weak (i.e., in an SCC all transitions have the same colors).

Note that algorithms that modify an automaton in place have to remember to update those properties. This has caused a couple of bugs over the years.

#### **4 Introduction of Alternating Automata**

Support for alternating ω-automata, as defined in the HOA format, was added to Spot in version 2.3 without introducing a new class. Rather, the twa graph class was extended to support alternation in such a way that existing algorithms would not require any modification to continue working on automata without universal branching. This was done by reserving the sign bit of the destination state number of each transition to signal universal branching.

Figure 2 shows an example of Alternating automaton (top-left) with co-B¨uchi acceptance. In many works on alternating automata, it is conventional to not represent accepting sinks, and instead have transition without destination. The top-right picture shows that Spot has a rendering option to hide accepting sinks.

The bottom of the figure shows that the automaton has prop state acc set, which means that the automaton is meant to be interpreted as using state-based acceptance. Colors are still stored on edges internally, but all edges leaving a state have the same colors. Seeing that the condition is co-B¨uchi (Fin(0)), the display code automatically switched to the convention of using double-circles for rejecting states.

Destinations with the sign bit set are called *universal destination groups* and appear as pink in the figure. There are two groups here: ~0 and ~3. The complement of these numbers can be used as indices in the dests vector, that actually store the destination groups. At the given index, one can read the size n of the destination group, followed by the state number of the n destinations.

Algorithms that work on alternating automata need to be able to iterate over all destinations of an edge. The process of checking the sign bit of the destination to decide if its a group, and to iterate on that group is hidden by the univ dests() method:

}

**Fig. 2.** Internal representation of alternating automata.

```
for(auto& e: aut->out(1)) {
 // use e.cond, e.acc, e.src
 for(unsigned d:aut->univ_dests(e))
  // use d
                                     for e in aut.out(1):
                                        # use e.cond, e.acc, e.src
                                        for d in aut.univ_dests(e):
                                           # use d
```
Note that this code works on non-universal branches as well: if e.dst is unsigned, univ dests(e) will simply iterate on that unique value.

Spot has two alternation removal procedures. One is an on-the-fly implementation of the Breakpoint construction [37] which transforms an n-state alternating B¨uchi automaton into a non-alternating B¨uchi automaton with at most 3*n* states. For very weak alternating automata, it is known that a powerset-based procedure can produce a transition-based generalized B¨uchi automaton with 2*n* states [23]; in fact that algorithm even works on *ordered* automata [11], i.e., alternating automata where the only rejecting cycles are self-loops. The second alternation removal procedure of Spot is a mix between these two procedures but does not work on the fly: it takes a *weak* automaton as input, and uses the break-point construction on rejectings SCCs that have more than one state, and uses the powerset construction for other SCCs.

#### **5 Extending Automata via Named Properties**

Spot's automata have a mechanism to attach arbitrary data to automata, called *named properties*. (This is similar to the notion of attributes in the R language.) An object can be attached to the automaton with:

```
aut->set_named_prop("property-name", new mytype(...));
```
and later retrieved with:

mytype\* data = aut->get\_named\_prop<mytype>("property-name");

Ensuring that mytype is the correct type for the retrieved property is the programmer's responsibility.

Spot has grown a list of many such properties over time.5 For instance automaton-name stores a string that would be displayed as the name of the automaton. The highlight-edges and highlight-states properties can be used to color edges and states. The state-names is a vector of strings that gives a name to each state, etc. While those examples are mostly related to the graphical rendering of the automata, some algorithms store useful byproducts as properties. For instance the product() algorithm will define a product-states named property that store a vector of pairs of the original states.

These named properties are sometimes used to provide additional semantics to the automaton, for instance to obtain a game or a Mealy machine.

#### **6 Games, Mealy Machines, and LTL Synthesis**

The application of Spot to LTL synthesis was introduced in Spot 2.5 in the form of the ltlsynt tool [35], but the inner workings of this tool were progressively redesigned and publicly exposed until version 2.10.