For a finite set Ω, let Dist(Ω) = - μ: Ω → [0, 1] | ω∈Ω μ(ω)=1 be the set of probability distributions over Ω with support supp(μ) = {ω ∈ Ω | μ(ω) > 0}. We write R≥0 = {|x| | x ∈ R} and R∞ = R∪{∞} for the non-negative and extended real numbers, respectively. **1** = 1,..., 1 denotes the vector of size ∈ N with all entries 1. We just write **1** if is clear. Let *p*i denote the i th entry and *p* · *p* the dot product of *p*, *p* ∈ (R∞). *p* ≤ *p* , *p* + *p* , and |*p*| are entry-wise. For Boolean expression cond, let [cond]=1 if cond is true and [cond]=0 otherwise.

#### 2.1 Markov Decision Processes, Strategies, and End Components

Definition 1 (Markov decision process [36]). A Markov decision process (MDP) is a tuple M = S, Act, **P**, sI with finite set of states S, initial state sI ∈ S, finite set of actions Act, and transition function **P**: S ×Act ×S → [0, 1] with s-∈S **P**(s, α, s ) ∈ {0, 1} for all s ∈ S and α ∈ Act.

We fix an MDP M = S, Act, **P**, sI . Intuitively, **P**(s, α, s ) is the probability to take a transition from s to s when choosing action α. An infinite path in M is a sequence π = s0α1s1α2 ··· ∈ (S×Act)ω with **P**(si, αi+1, si+1) > 0 for all i ∈ N. We write π[i] = si for the (i+1)th state visited by π and define the length of π as |π| = ∞. A finite path is a finite prefix πˆ = s0α1 ...αnsn of infinite path π, where last(ˆπ) = sn ∈ S, |πˆ| = n and πˆ[i] = si for i ≤ n. The set of finite (infinite) paths in M is denoted by PathsM fin (PathsM inf). The enabled actions at a state s ∈ S are given by the set Act(s) = {α ∈ Act | ∃ s ∈ S : **P**(s, α, s ) > 0}. We assume Act(s) = ∅ for all s. If |Act(s)| = 1 for all s ∈ S, M is called a Markov Chain (MC). We write Ms for the MDP obtained by replacing the initial state of M by s ∈ S. For s ∈ S and α ∈ Act, we define the set of successor states succ(s, α) = {s | **P**(s, α, s ) > 0}. For s ∈ S, the set of predecessor state-action pairs is given by pre(s ) = {s, α | **P**(s, α, s ) > 0}. For a set E ⊆ S × Act, we define S-E = {s ∈ S | ∃ α: s, α ∈ E}, Act-E = {α ∈ Act | ∃ s: s, α ∈ E}, and **P**-E(s, α, s )=[s, α∈E] · [s ∈ S-E] · **P**(s, α, s ). We say E is closed for M if ∀ s, α∈E : α ∈ Act(s) and succ(s, α) ⊆ S-E.

Definition 2 (Sub-MDP). The sub-MDP of M, closed E ⊆ S × Act, and s ∈ S-E is given by M-E, s = S-E, Act-E, **P**-E, s. We also write M-E for the sub-MDP M-E, s and an arbitrary state s ∈ S-E.

Definition 3 (End Component). A non-empty set E ⊆ S × Act is an end component (EC) of M if E is closed for M and for each pair of states s, s ∈ S-E there is a finite path πˆ ∈ PathsM-E fin with πˆ[0] = s and last(ˆπ) = s . An EC E is maximal, if there is no other EC E with E - E . The set of all maximal end components of M is MECS(M).

The maximal ECs of a Markov chain are also called bottom strongly connected components (BSCCs). A strategy resolves nondeterminism in MDPs:

Definition 4 (Strategy). A (general) strategy for MDP M is a function σ : PathsM fin → Dist(Act) with supp(σ(πˆ)) ⊆ Act(last(ˆπ)) for all πˆ ∈ PathsM fin.

Let σ be a strategy for M. Intuitively, σ(ˆπ)(α) is the probability to perform action α after observing history πˆ ∈ PathsM fin. A strategy is pure if all histories are mapped to Dirac distributions, i.e., the support is a singleton. A strategy is stationary if its decisions only depend on the current state, i.e., ∀ π, ˆ πˆ ∈ PathsM fin : last(ˆπ) = last(ˆπ ) implies σ(ˆπ) = σ(ˆπ ). We often assume σ : S → Dist(Act) for stationary and σ : S → Act for pure stationary strategies σ. Let ΣM and ΣM PS be the sets of general and pure stationary strategies, respectively. A set of paths Π ⊆ PathsM inf is compliant with σ ∈ ΣM if for all π = s0α1s1 ···∈ Π and prefixes πˆ of π satisfy σ(ˆπ)(α|πˆ|+1) > 0. The induced Markov chain of M and σ ∈ ΣM PS is given by Mσ = M-Eσ, sI with Eσ = {s, σ(s) | s ∈ S}.

MDP M and strategy σ ∈ ΣM induce a probability measure PrMσ on subsets Π ⊆ PathsM inf given by a standard cylinder set construction [4,22]. The expected value of X : PathsM inf → R∞ is EMσ (X) = π X(π) dPrMσ ({π}). For σ ∈ ΣM PS, PrMσ and EMσ coincide with the corresponding measures on MC Mσ.

#### 2.2 Objectives

A reward structure **R**: S × Act × S → R≥0 assigns non-negative rewards to transitions. We accumulate rewards on (in)finite paths π = s0α1s1α2 ... : **R**(π) = |π| i=1 **R**(si−1, αi, si). For a set of goal states G ⊆ S, let **R**♦G(π) = **R**(ˆπ), where πˆ is the smallest prefix of π with last(ˆπ) ∈ G (or πˆ = π if no such prefix exists). Intuitively, **R**♦G(π) is the reward accumulated on π until a state in G is reached. A (reward) objective has the form E∼(**R**♦G) for ∼ ∈ {≥, ≤}. We write M, σ, p |= E∼(**R**♦G) iff EMσ (**R**♦G) ∼ p, i.e., for M and σ, the expected accumulated reward until reaching G is at least (or at most) p ∈ R∞. We call the objective maximizing if ∼ = ≥ and minimizing otherwise. If G = ∅ (i.e., **R**♦G(π) = **R**(π) for all paths π), we call the objective a total reward objective. Let the reward structure **R**G be given by **R**(s, α, s )=[s ∈ G]. Then, PrMσ (♦G)=EMσ (**R**G♦G) for every σ ∈ ΣM, where ♦G ⊆ PathsM inf denotes the set of paths that visit a state in G. We use P∼(♦G) as a shortened for E∼(**R**G♦G) and call such an objective a reachability objective.

Definition 5 (Multi-objective query). For MDP M, an -dimensional multiobjective query is a tuple Q = ψ1,...,ψ of objectives ψj = E∼j (**R**j♦Gj ).

Each objective ψj considers a different reward structure **R**j . The MDP M, strategy σ, and point *p* ∈ (R∞) satisfy a multi-objective query Q = ψ1,...,ψ (written M, σ, *p* |= Q) iff ∀ j : M, σ, *p*j |= ψj . Then, we also say σ achieves *p* and call *p* achievable. Let AchM(Q) (AchM PS(Q)) denote the set of points achieved by a general (pure stationary) strategy. The closure of a set P ⊆ (R∞) with respect to query Q is clQ(P) = - *p* ∈ (R∞) | ∃ *p* ∈ P : ∀ j : *p* j ∼j *p*j . For *p*, *p* ∈ (R∞), we say that *p* dominates *p* if *p* ∈ clQ({*p*}). In this case, M, σ, *p* |= Q implies M, σ, *p* |= Q for any σ ∈ ΣM. We are interested in the Pareto front, which is the set of non-dominated achievable points.

Figure 1: An MDP and a plot of the pure stationary and general Pareto fronts.

Definition 6 (Pareto front). The (general) Pareto front for M and Q is ParetoM(Q) = *p* ∈ AchM(Q) | ∀ *p* ∈ AchM(Q): *p* ∈ clQ({*p* }) =⇒ *p* = *p* .

The Pareto front is the smallest set P ⊆ (R∞) with clQ(P) = AchM(Q). In a similar way, we define the pure stationary Pareto front ParetoM PS(Q) which only consider points in AchM PS(Q).

Example 1. Let M be the MDP in Fig. 1a and Q = P≥(♦G), P≥(♦G-). A pure stationary strategy choosing β at s1 reaches both, s4 ∈ G and s3 ∈ G- with probability 0.7 and thus achieves 0.7, 0.7. Similarly, 0, 1 and 1, 0 are achievable by a pure stationary strategy. Point 1, 0.8 is achievable by a nonstationary pure strategy that chooses α at s1, γ at the first visit of s2, and δ in all other cases. Changing this strategy by picking γ only with probability 0.5 achieves 0.5, 0.9. Fig. 1b illustrates ParetoM PS(Q) (dots), AchM PS(Q) (green area), ParetoM(Q) (dotted line), and AchM(Q) (blue and green area).

## 3 Deciding Achievability

The achievability problem asks whether a given point is achievable.

```
General Multi-objective Achievability Problem (GMA)
Input: MDP M, -dimensional multi-objective query Q, point p ∈ (R∞)
Output: Yes iff p ∈ AchM(Q) holds
```
For GMA, the point can be achieved by a general strategy that can potentially make use of memory and randomization. As discussed earlier, this class of strategies is not suitable for various applications. In this work, we focus on a variant of the achievability problem that only considers pure stationary strategies. Sect. 5 also addresses pure strategies that can store more information from the history, e.g., whether a goal state set has been reached already.

Pure Stationary Multi-objective Achievability Problem (PSMA)

Input: MDP M, -dimensional multi-objective query Q, point *p* ∈ (R∞) Output: Yes iff *p* ∈ AchM PS(Q) holds

#### 3.1 Complexity Results

GMA is PSPACE hard (already with only reachability objectives) [40] and solvable within exponential runtime [20,23]. To the best of our knowledge, a PSPACE upper bound on the complexity of GMA is unknown. This complexity is rooted in the dimension of the query Q: for fixed , the algorithms of [20,23] have polynomial runtime. In contrast, PSMA is NP-complete, even if restricted to 2 objectives.

## Lemma 1. PSMA with only reachability objectives is NP-hard.

Proof. The result follows by a reduction from the subset sum problem. Given n ∈ N, *a* ∈ Nn and z ∈ N, the subset sum problem is to decide the existence of *v* ∈ {0, 1}n such that *v* · *a* = z. This problem is NP-complete [25]. For a given instance of the subset sum problem, we construct the MDP M = S, Act, **P**, sI with state space S = {sI , s1,...,sn, g1, g2}, actions Act = {α, Y, N}, and for all i ∈ {1,...,n}, **P**(sI , α, si) = *a*i **1***·a* and **P**(si,Y,g1) = **P**(si,N,g2)=1. States g1 and g2 are made absorbing, i.e., **P**(g1, α, g1) = **P**(g2, α, g2)=1.

We claim that the PSMA problem for M, Q = P≥(♦ {g1}), P≥(♦ {g2}), and *p* = z **1**·*a* , 1 − z **1**·*a* answers "yes" iff there is a vector *v* satisfying the subset sum problem for n, *a* and z. Consider the bijection f : ΣM- PS → {0, 1}n with f(σ)i = [σ(si)=Y ] for all σ ∈ ΣM- PS and i ∈ {1,...,n}. We get PrM- σ (♦ {g1}) = n i=1 *a*i **1***·a* [σ(si)=Y ] = f(σ)·*a* **1**·*a* . Moreover, PrM- σ (♦ {g2})=1 − PrM- σ (♦ {g1}) = 1− f(σ)·*a* **1**·*a* . It follows that σ achieves *p* iff f(σ) is a solution to the instance of the subset sum problem. Our construction is inspired by similar ideas from [14,40].

Lemma 2 ([14]). PSMA with only total reward objectives is NP-hard.

Theorem 1. PSMA is NP-complete.

Proof. Containment follows by guessing a pure stationary strategy and evaluating it on the individual objectives. This can be done in polynomial time [4]. Hardness follows by either Lemma 1 or 2.

Proofs of Lemmas 1 and 2 only consider 2-dimensional multi-objective queries. Hence, in contrast to GMA, the hardness of PSMA is not due to the size of the query.

Corollary 1. PSMA with only two objectives is NP-complete.

#### 3.2 A Mixed Integer Linear Programming Approach

An MDP M = S, Act, **P**, sI has exactly |ΣM PS| = s∈S |Act(s)| many pure stationary strategies. A simple algorithm for PSMA enumerates all σ ∈ ΣM PS and checks whether M, σ, *p* |= Q holds. In practice, however, such a brute-force approach is not feasible. For the MDPs that we consider in our experiments in Sect. 6, the number of pure stationary strategies often exceeds 1010 000. Instead, our approach is to encode an instance for PSMA as an MILP problem.

For an MILP instance as above, each of the n rows of the inequation system *Ax* ≤ *b* represent a constraint that is linear over the integral and m real-valued variables given by *x*. We call the constraints feasible if there is a solution to the inequation system. The task is to decide whether the constraints are feasible and if so, find a solution that maximizes a linear optimization function *c*T *x*. The optimization function can be omitted if we are only interested in feasibility. MILP is NP-complete [35]. However, tools such as Gurobi [27] and SCIP [26] implement practically efficient algorithms that can solve large instances.

For the rest of this section, let M = S, Act, **P**, sI , Q = ψ1,...,ψ with ψj = E∼j (**R**j♦Gj ), and *p* ∈ (R∞) be an instance for PSMA. We provide a translation of the PSMA instance to an instance for MILP that has a feasible solution iff *p* ∈ AchM PS(Q). The MILP encoding considers integer variables to encode a pure stationary strategy σ ∈ ΣM PS. The other variables and constraints encode the expected reward for each objective on the induced MC Mσ.

#### 3.3 Unichain MDP and Finite Rewards

Restriction 1 (Unichain MDP). MDP M has exactly one end component.

Restriction 2 (Reward Finiteness). EMs σ (**R**j♦Gj ) < ∞ holds for each objective ψj = E∼j (**R**j♦Gj ), state s, and pure stationary strategy σ.

For simplicity, we first explain our encoding for unichain MDP with finite reward. Sect. 3.5 lifts Restriction 1 and Sect. 3.6 lifts Restriction 2 with more details given in [17, App. B]. Sect. 3.4 presents an alternative to the encoding of this section, which is smaller but restricted to total reward objectives.

Fig. 2 shows the MILP encoding in case Restrictions 1 and 2 hold. We assume ∀ j : *p*j = ∞ for the point *p* since (i) EMσ (**R**j♦Gj ) ≤ ∞ holds trivially and (ii) EMσ (**R**j♦Gj ) ≥ ∞ will never hold due to Restriction 2. For j ∈ {1,...,}, let Sj 0 = {s ∈ S | ∀ σ ∈ ΣM : EMσ (**R**j♦Gj )=0} and Sj ? = {s ∈ S \ Sj 0 | s can be reached from sI without visiting a state in Sj 0}. These sets can be obtained a priori by analyzing the graph structure of M [4]. Moreover, we consider upper bounds Uj s ∈ Q for the expected reward at state s ∈ Sj ? such that Uj s ≥ maxσ∈ΣM EMs σ (**R**j♦Gj ). We compute such upper bounds using singleobjective model checking techniques [4,5]. The MILP encoding applies the characterization of expected rewards for MCs as a linear equation system [4].

Lemma 3. For every σ ∈ ΣM PS, the following equation system has a unique solution Φ: {xs | s ∈ S} → R|S| satisfying Φ(xs)=EMs σ (**R**j♦Gj ):

$$\forall s \in S\_0^j \colon x\_s = 0 \qquad \forall s \in S\_? \colon x\_s = \sum\_{s' \in S} \mathbf{P}(s, \sigma(s), s') \cdot \left(x\_{s'} + \mathbf{R}(s, \sigma(s), s')\right)$$

∀ s ∈ S : - Select an action at each state ∀ α ∈ Act(s):

$$a\_{s, \alpha} \in \{0, 1\} \tag{1}$$

$$\sum \quad a\_{s, \alpha} = 1 \tag{2}$$

$$\forall j \in \{1, \ldots, \ell\}: \begin{array}{ll} \alpha \in \mathcal{A}ct(s) \\\\ \cdot \end{array} \qquad\qquad\Rightarrow \begin{array}{ll} \Rightarrow \begin{array}{ll} Compute \; \, e \; \text{array } \epsilon \text{-} x \; \text{end} \; \vert \; \text{ward} \; \text{ward} \; \text{ward} \; \text{ward} \; \text{ward} \end{array}$$

∀ s ∈ Sj 0 : xj s = 0 (3)

If ψj is maximising, ± = + and [min] = 0. Otherwise, ± = − and [min] = 1.

$$\forall s \in S\_?^j: \qquad \qquad \pm x\_s^j \in [0, U\_s^j] \tag{4}$$

$$\forall \alpha \in Act(s): \qquad \pm x\_{s,\alpha}^j \in [0, U\_s^j] \tag{5}$$

$$x\_{s,\alpha}^j \le \sum\_{s' \in S} \mathbf{P}(s, \alpha, s') \cdot \left( x\_{s'}^j \pm \mathbf{R}\_{\boldsymbol{\beta}}(s, \alpha, s') \right) \tag{6}$$

$$x\_{s, \alpha}^j \le U\_s^j \cdot (a\_{s, \alpha} - \text{[min]}) \tag{7}$$

$$x\_s^j \le \sum\_{\alpha \in Act(s)} x\_{s,\alpha}^j + \left[ \min \right] \cdot \left( |Act(s)| - 1 \right) \cdot U\_s^j \tag{8}$$

$$\pm x\_{s\_I}^j \sim\_j \mathbf{p}[j] \qquad\qquad\Rightarrow \text{A secret value at initial state} \tag{9}$$

Figure 2: MILP encoding for unichain MDP and finite rewards.

Proof. Since M is unichain and we do not collect infinite reward, the only EC of M (i.e., the only BSCC of Mσ for any σ) either contains a goal state or only contains transitions with zero reward. It follows that ∀ σ ∈ ΣM PS : PrMσ (♦Sj 0)=1. Lemma 3 follows by standard arguments for MCs with rewards [4, Section 10.5.1].

We discuss the intuition of each constraint in Fig. 2. Let Φ: Var → R be an assignment of the occurring variables Var to values. Φ is a solution of the constraints if all (in)equations are satisfied upon replacing all variables v by Φ(v).

Lines 1 and 2 encode a strategy σ ∈ ΣM PS by considering a binary variable as,α for each state s and enabled action α such that σ(s)(α)=1 iff Φ(as,α)=1 for a solution Φ. Due to Line 2, exactly one action has to be chosen at each state.

Lines 3 to 8 encode for each objective ψj the expected rewards obtained for the encoded strategy σ. For every s ∈ S, the variable xj s represents a (lower or upper) bound on the expected reward at s. Line 3 sets this value for all s ∈ Sj 0, reflecting the analogous case from Lemma 3. For s ∈ Sj ? , we distinguish maximizing (∼j = ≥) and minimizing (∼j = ≤) objectives ψj .

For maximizing ψj , we have Φ(xj s) ≤ EMs σ (**R**j♦Gj ) for every solution Φ. This is achieved by considering a variable xj s,α for each enabled action α ∈ Act(s). In Line 6, we use the equation system characterization from Lemma 3 to assert that the value of xj s,α can not be greater than the expected reward at s, given that the encoded strategy σ selects α. If σ does not select α (i.e., Φ(as,α)=0), Line 7 implies Φ(xj s,α)=0. Otherwise, this constraint has no effect. Line 8 ensures that every solution satisfies Φ(xj s) ≤ Φ(xj s,α) ≤ EMs σ (**R**j♦Gj ) for α with Φ(as,α)=1.

For minimizing ψj , we have −Φ(xj s) ≥ EMs σ (**R**j♦Gj ) for every solution Φ, i.e., we consider the negated reward values. The encoding is as for maximizing

objectives. However, Line 7 yields Φ(xj s,α) = −Uj s if α is not selected. Thus, in Line 8 we add Uj s for each of the (|Act(s)| − 1) non-selected actions.

Line 9 and our observations above yield EMs σ (**R**j♦Gj ) ≥ Φ(xj sI ) ≥ *p*j for maximizing and EMs σ (**R**j♦Gj ) ≤ −Φ(xj sI ) ≤ *p*j for minimizing objectives. Therefore, *p* is achievable if a solution Φ exists. On the other hand, if *p* is achievable by some σ ∈ ΣM PS, the solution Φ exists with Φ(as,α) = σ(s)(α), Φ(xj s) = Φ(xj s,α) = ±EMs σ (**R**j♦Gj ) if α = σ(s), and Φ(v)=0 for other v ∈ Var .

Theorem 2. For unichain M and finite rewards, the constraints in Fig. 2 are feasible iff *p* ∈ AchM PS(Q).

Proposition 1. The MILP encoding above considers O(|S|·|Act| · ) variables.

#### 3.4 Alternative Encoding for Total Rewards

We now consider PSMA instances where all objectives ψj = E∼j (**R**j♦Gj ) are expected total reward objectives, i.e., Gj = ∅. For such instances, we can employ an encoding from [23] (restated in Lemma 4) for GMA. In fact, we can often translate reachability reward objectives to total reward objectives, e.g., if the set of goal states can not be left or if all objectives consider the same goal states.

Lemma 4 ([23]). For S0 ⊆ S, let Φ: Var → R≥0 be an assignment of variables Var = {ys,α | s ∈ S \ S0, α ∈ Act(s)} and let σΦ be a stationary strategy satisfying σΦ(s)(α) = Φ(ys,α)/ β∈Act(s) Φ(ys,β) for all s ∈ S \ S0 and α ∈ Act(s) for which the denominator is non-zero. Then, Φ is a solution to the equation system

$$\begin{aligned} \forall s \in S \mid S\_0 \colon \sum\_{\alpha \in Act(s)} y\_{s,\alpha} &= \begin{bmatrix} s = s\_I \end{bmatrix} + \sum\_{\langle s',\alpha' \rangle \in pr(s)} \mathbf{P}(s',\alpha',s) \cdot y\_{s',\alpha'}\\ 1 &= \sum\_{y\_{s,\alpha} \in Var} y\_{s,\alpha} \cdot \sum\_{s' \in S\_0} \mathbf{P}(s,\alpha,s') \end{aligned}$$

iff PrMσΦ (♦S0)=1 and ∀ ys,α ∈ Var : Φ(ys,α)=EMσΦ (**R**s,α♦S0) with reward structure **R**s,α given by **R**s,α(ˆs, α, s ˆ ) = [ˆs = s and αˆ = α].

In [23], the lemma is applied to decide achievability of multiple total reward objectives under strategies that are stationary, but not necessarily pure. Intuitively, EMσΦ (**R**s,α♦S0) coincides with the expected number of times action α is taken at state s until S0 is reached. Since this value can be infinite if PrMσΦ (♦S0) < 1, a solution Φ can only exist if it induces a strategy that almost surely reaches S0.

The encoding for unichain MDP with finite rewards and total reward objectives is shown in Fig. 3, where S0 = j Sj 0 and S? = S \ S0. We consider the constraints in conjunction with Lines 1 and 2 from Fig. 2. Let Φ be a solution and let σ be the strategy encoded by such a solution, i.e., σ(s)(α) = Φ(as,α).

Lines 10 to 12 reflect the equations of Lemma 4. Since M is unichain and we assume finite rewards, there is just one end component in which no reward can be collected. Hence, S0 is almost surely reached. Line 10 ensures that the

$$\forall s \in S\_{\mathcal{I}}, \alpha \in Act(s) \colon \underbrace{y\_{s,\alpha} \in [0, V\_s \cdot a\_{s,\alpha}]}\_{\hspace{0.1cm}} \tag{10}$$

$$\sum\_{\alpha \in Act(s)} y\_{s,\alpha} = [s = s\_I] + \sum\_{\langle s',\alpha'\rangle \in pre(s)} \mathbf{P}(s',\alpha',s) \cdot y\_{s',\alpha'} \tag{11}$$

$$1 = \sum\_{s \in S\_?} \sum\_{\alpha \in \mathcal{Act}(s)} y\_{s,\alpha} \cdot \sum\_{s' \in S\_0} \mathbf{P}(s,\alpha, s') \tag{12}$$

$$\forall j \in \{1, \ldots, \ell\}: \qquad x\_{s\_I}^j = \sum\_{s \in S\_{\mathcal{T}}} \sum\_{\alpha \in Act(s)}^{\ell} y\_{s,\alpha} \cdot \sum\_{s' \in S}^{\ell} \left(\mathbf{P}(s, \alpha, s') \cdot \mathbf{R}\_J(s, \alpha, s')\right) \tag{13}$$

$$x\_{s\_I}^j \sim\_j \mathbf{p}[j] \tag{14}$$

$$\text{Figure 3: } \mathsf{MLIP} \text{ encoding for total reward objects.}$$

strategy in Lemma 4 coincides with the encoded pure strategy σ. We write Vs for an upper bound of the value a solution can possibly assign to ys,α, i.e., ∀ σ ∈ ΣM PS : Vs ≥ EMσ (**R**s,α♦S0). Such an upper bound can be computed based on ideas of [5]. More details are given in [17, App. A].

With Lemma 4 we get that Φ(ys,σ(s)) is the expected number of times state s is visited under strategy σ. Therefore, in Line 13 we sum up for each state s ∈ S? the expected amount of reward collected at s. This yields Φ(xj sI )=EMσ (**R**j♦Gj ). Finally, Line 14 asserts that the resulting values exceed the thresholds given by *p*.

Theorem 3. For unichain M, finite rewards, and total reward objectives, the constraints in Fig. 3 and Lines 1 and 2 of Fig. 2 are feasible iff *p* ∈ AchM PS(Q).

Proposition 2. The MILP encoding above considers O(|S|·|Act| + ) variables.

The encoding for total reward objectives considers fewer variables compared to the encoding of Sect. 3.3 (cf. Proposition 1). In practice, this often leads to faster solving times as we will see in Sect. 6.

#### 3.5 Extension to Multichain MDP

We now lift the restriction to unichain MDP, i.e., we consider multichain MDP with finite rewards. We focus on the encoding of Sect. 3.3. Details for the approach of Sect. 3.4 are in [17, App. C]. The key challenge is that the equation system in Lemma 3 does not yield a unique solution for multichain MDP.

Example 2. For the multichain MDP in Fig. 5a with G = {s1} we have S0 = {s1} and S? = {s0} (the superscript j is omitted as there is only one objective). For σ with σ(s0) = α we get EMσ (**R**♦G)=0, but every Φ: - xs0 , xs1 → R × {0} is a solution for the equation system in Lemma 3.

For multichain MDP it can be the case that for some strategy σ the set Sj 0 is not reached with probability 1, i.e., there is a positive probability to stay in the set Sj ? forever. For the induced Markov chain Mσ, this means that there is a reachable BSCC consisting only of states in Sj ? . Since BSCCs of Mσ coincide with end components of M, we need to inspect the ECs of M that only consist of

zj

∀ j ∈ {1,...,} , E ∈ MECS(M-Ej ? ): -Detect states with zero reward

$$\forall s \in S \left[ \mathcal{E} \right] \colon \begin{array}{c} \quad \left. \pm x\_s^j \le U\_s^j \cdot \left( 1 - e\_s^j \right) \right| \\ \quad \left. \right| \quad \left. \left. \right| \quad \left. \right| \end{array} \tag{15}$$

$$\forall \begin{array}{c} \forall s, \alpha \rangle \in \mathcal{E}: \\\\ \end{array} \qquad \qquad \begin{array}{c} e\_{s,\alpha}^{j} \in \{0, a\_{s,\alpha}\} \end{array} \tag{16}$$

$$e' \in \underline{succ(s, \alpha)} \colon \qquad e^j\_{s, \alpha} \le e^j\_{s'} \tag{17}$$

$$\forall s \in succ(s, \alpha) \colon \qquad \begin{aligned} \forall s' \in succ(s, \alpha) & \quad & e'\_{s, \alpha} \le e'\_{s'} \\ \quad & e^j\_s = \sum\_{\alpha \in Act(s)} \left[ \langle s, \alpha \rangle \in \mathcal{E} \right] \cdot e^j\_{s, \alpha} \end{aligned} \tag{17}$$

$$\forall \alpha \in \operatorname{Act}(s): \qquad \qquad z\_{s,\alpha}^j \in [0, V\_s \cdot a\_{s,\alpha}] \tag{19}$$

$$z\_{s,\perp}^{j} + \sum\_{s',\perp}^{z\_{s,\perp}^{j}} z\_{s,\alpha}^{j} = \frac{1}{|S\llbracket \mathcal{E} \rceil|} + \sum\_{s',\perp,\perp'} \mathbf{P}(s',\alpha',s) \cdot z\_{s',\alpha'}^{j} \tag{21}$$

$$\begin{array}{llll} \sum\_{\alpha \in Act(s)} & \left| S \left[ \mathcal{E} \right] \right| & \sum\_{\langle s', \alpha' \rangle \in pre(s) \cap \mathcal{E}} & \left( \omega \cdot \omega \right) \cdot z\_{s', \alpha'} \\ & 1 = \sum\_{\omega} & \left( z\_{s, \bot}^{\psi\_j} + \sum\_{\bot} \quad \left[ \langle s, \alpha \rangle \notin \mathcal{E} \right] \cdot z\_{s, \alpha}^{j} \right) \end{array} \tag{22}$$

α∈Act(s)

Figure 4: MILP encoding for detection of end components.

s∈SE

Sj ? -states. These ECs correspond to the ECs of the sub-MDP M-Ej ? , where Ej ? is the largest subset of Sj ? ×Act that is closed for M. For each E ∈ MECS(M-Ej ? ), we need to detect whether the encoded strategy induces a BSCC E ⊆ E.

To cope with multiple ECs, we consider the constraints from Fig. 2 in conjunction with the constraints from Fig. 4. Let Φ be a solution to these constraints and let σ be the encoded strategy σ with σ(s)(α) = Φ(as,α). For each objective ψj and state s, a binary variable ej s is set to 1 if s lies on a BSCC of the induced MC Mσ. We only need to consider states s ∈ S-E for E ∈ MECS(M-Ej ? ).

Line 15 ensures that the value of xj s is set to 0 if s lies on a BSCC of Mσ. Lines 16 to 18 introduce binary variables ej s,α for each state-action pair in the EC such that any solution Φ satisfies Φ(ej s,α)=1 iff Φ(ej s) = Φ(as,α)=1. Line 17 yields that Φ(ej s,α)=1 implies Φ(e j s- )=1 for all successors s of s and the selected action α. Hence, for all s with Φ(ej s)=1 and for all s reachable from s in Mσ, we have Φ(e j s- )=1 and s , σ(s )∈E. Therefore, we can only set ej s to 1 if there is a BSCC E ⊆ E that either contains s or that is almost surely reached from s without leaving E. As finite rewards are assumed, E can not contain a transition with positive reward, yielding EMσ (**R**j♦Gj )=0 if Φ(ej s)=1.

An assignment that sets all variables ej s and ej s,α to 0 trivially satisfies the constraints in Lines 15 to 18. In Lines 19 to 22 we therefore ensure that if a BSCC E ⊆ E exists in Mσ, Φ(ej s)=1 holds for at least one s ∈ S-E . The idea is based on the observation that if a BSCC E ⊆ E exists, there is a state s ∈ S-E that does not reach the set S \S-E almost surely. We consider the MDP ME , a mild extension of M-E given by ME = (S-E - sE I , sE ⊥ , Act {αI , ⊥} , **P**E , sE I ), where **P**E extends **P**-E such that **P**E (sE ⊥, ⊥, sE ⊥)=1 and ∀ s ∈ S-E : – **P**E (sE I , αI , s)=1/|S-E|, **P**E (s, ⊥, sE ⊥)=1, and

$$-\left\{\alpha \stackrel{\cdot}{\in} \{\hat{\alpha} \in \operatorname{Act}(s) \mid \bar{\langle s, \stackrel{\cdot}{\alpha} \rangle} \notin \mathcal{E}\right\} \colon \mathbf{P}^{\mathcal{E}}(\bar{s}, \alpha, s\_{\perp}^{\mathcal{E}}) = 1.\right\}$$

Lines 21 and 22 reflect the equation system from Lemma 4 for MDP ME and S0 = {s⊥}. Additionally, Lines 19 and 20 exclude negative solutions and assert

Figure 5: MDPs referenced in Examples 2 and 4.

Φ(zj s,α)=0 if Φ(as,α)=0 and Φ(z ψj s,⊥)=0 if Φ(ej s)=0 for any solution Φ. Hence, for states s ∈ S-E where Φ(ej s)=0, the strategy σ encoded by the variables as,α coincides with the strategy considered in Lemma 4. Assume that solution Φ yields a BSCC within the states of E in Mσ and therefore also a BSCC in (ME )σ. Since sE ⊥ has to be reached almost surely in ME (cf. Lemma 4), the BSCC has to contain at least one state s with Φ(ej s)=1.

In summary, Lines 19 to 22 imply that every BSCC E ⊆ E of Mσ contains at least one state s with Φ(ej s)=1. Then, with Lines 16 to 18 we get that Φ(e j s- )=1 has to hold for all s ∈ S-E . In Mσ, the set Sj 0 ∪ - s | Φ(ej s)=1 is therefore reached almost surely and all the states in this set get assigned value 0. In this case, the solution of the equation system from Lemma 3 becomes unique again.

Theorem 4. For finite rewards, the constraints in Figs. 2 and 4 are feasible iff *p* ∈ AchM PS(Q).

#### 3.6 Extension to Infinite Rewards

Our approach can be modified to allow PSMA instances where infinite expected reward can be collected, i.e., where Restriction 2 does not hold. Infinite reward can be collected if we cycle through an EC of M that contains a transition with positive reward. Such instances are of practical interest as this often corresponds to strategies that do not accomplish a certain goal (e.g., a robot that stands still and therefore requires infinite time to finish its task).

We sketch the necessary modifications. More details are in [17, App. B]. Let S∞ be the set of states where every pure strategy induces infinite reward for at least one minimizing objective. To ensure that the MILP instance has a (realvalued) solution, we consider the sub-MDP of M obtained by removing S∞.

If infinite reward can be collected in an EC, it should not be considered in Fig. 4. We therefore let E range over maximal ECs that only consist of (a) states in Sj ? and (b) transitions with reward 0.

The upper bounds Uj s for the maximal expected rewards at each state can not be set to ∞. However, for the encoding it suffices to compute values that are sufficiently large. However, we remark that in practice our approach from [17, App. B] can lead to very large values, yielding numerical instabilities.

For maximizing objectives, we introduce one additional objective which, in a nutshell, checks that the probability to reach a 0-reward BSCC is below 1. If this is the case, there is a positive probability to reach a BSCC in which infinitely many reward can be collected.

## 4 Computing the Pareto Front

Our next goal is to compute the pure stationary Pareto front ParetoM PS(Q) for MDP M and multi-objective query Q. This set can be very large, in particular if the objectives are strongly conflicting with many different tradeoffs. In the worst case, every pure stationary strategy induces a point *p* ∈ ParetoM PS(Q) (e.g., for Q = E≤(**R**♦G), E≥(**R**♦G)). We try to find an approximation of ParetoM PS(Q).

Definition 7. Let ∈ (R>0). An -approximation of P ⊆ (R∞) is a pair L, U with L ⊆ P ⊆ U and ∀ *p* ∈ P : ∃ *p* ∈ L ∪ ((R∞) \ U): |*p* − *p* | ≤ .

Pure Stationary Pareto Approximation Problem (PSP ≈)

Input: MDP M, -dimensional multi-objective query Q, precision ∈ (R>0) such that ParetoM PS(Q) ⊆ R Output: An -approximation of clQ(ParetoM PS(Q))

For simplicity, we only consider inputs that satisfy restriction Restriction 2, i.e., for ψj = E∼j (**R**j♦Gj ) there is Uj = ∞ such that ∀ σ ∈ ΣM PS : Uj ≥ EMσ (**R**j♦Gj ). Ideas of Sect. 3.6 can be used for some other inputs. An all-embracing treatment of infinite rewards, in particular for maximizing ψj , is subject to future work.

Our approach for PSP ≈ successively divides the solution space into candidate regions. For each region R (initially, let R = [0, U1] × ··· × [0, U]), we use the MILP encoding from Sect. 3 with an optimization function to find a point *p* ∈R∩ ParetoM PS(Q) (or find out that no such point exists). The region R is divided into (i) an achievable region RA ⊆ AchM PS(Q), (ii) an unachievable region RU ⊆ R\AchM PS(Q), (iii) further candidate regions R1,..., Rn that are analyzed subsequently, and (iv) the remaining area R \ (RA ∪ RU ∪ R1 ∪···∪Rn) which does not require further analysis as we are only interested in an -approximation. The procedure stops as soon as no more candidate regions are found.

Example 3. Fig. 6 sketches the approach for an MDP M and a query Q with two maximizing objectives. We maintain a set of achievable points (light green) and a set of unachievable points (red). Initially, our candidate region corresponds to R1 = [0, U1]×[0, U2] given by the white area in Fig. 6a. We consider the direction vector *w*1 which is orthogonal to the line connecting U1, 0 and 0, U2 . To find some point *p* ∈ ParetoM PS(Q) ∩ R1, we solve the MILP resulting from the constraints as in Sect. 3, the constraint x1 sI , x2 sI ∈ R1, and the optimization function *w*1 · x1 sI , x2 sI . Fig. 6b shows the obtained point *p*1 ∈ R1. Since *p*1 is achievable, we know that any point in clQ({*p*1}) has to be achievable as well. Moreover, the set {*p* ∈ R1 | *w*1 · *p* > *w*1 · *p*1} indicated by the area above the diagonal line in Fig. 6b can not contain an achievable point. The gray areas do not have to be checked in order to obtain an -approximation. We continue with R2 indicated by the white area and the direction vector *w*2, orthogonal to the line connecting 0, U2 and *p*1. As before, we solve an MILP now yielding the point *p*2 in Fig. 6c. We find achievable points clQ({*p*2}) but no further unachievable points. The next iteration considers candidate region R3 and direction vector

Figure 6: Example exploration of achievable points.

*w*1, yielding point *p*3 shown in Fig. 6d. The trapezoidal area is added to the unachievable points whereas clQ({*p*3}) is achievable. Finally, we check R4 for which the corresponding MILP instance is infeasible, i.e., R4 is unachievable.

The ideas sketched above can be lifted to > 2 objectives. Inspired by [24, Alg. 4], we choose direction vectors that are orthogonal to the convex hull of the achievable points found so far. In fact, for total reward objectives we can apply the approach of [24] to compute the points in ParetoM PS(Q)∩ParetoM(Q) first and only perform MILP-solving for the remaining regions. As the distance between two found points *p*, *p* is at least |*p* − *p* | ≥ , we can show that our approach terminates after finding at most j Uj/j points. Other strategies for choosing direction vectors are possible and can strongly impact performance.

## 5 Bounded Memory

For GMA, it is necessary and sufficient to consider strategies that require memory exponential in the number of objectives [20,24,40] by storing which goal state set has been reached already. In contrast, restricting to pure (but not necessarily stationary) strategies imposes nontrivial memory requirements that do not only depend on the number of objectives, but also on the point that is to be achieved.

Example 4. Let M be the MDP in Fig. 5b and Q = P≥ (♦G), P≥ (♦G-). The point *p*k = 0.5k, 1−0.5k for k ∈ N is achievable by taking α with probability 0.5k. *p*k is also achievable with the pure strategy σk where σk(ˆπ) = α iff |πˆ| ≥ k. σk uses k memory states. Pure strategies with fewer memory states do not suffice.

We search for pure strategies with bounded memory. For an MDP M and K > 0, let ΣM P,K denote the set of pure K-memory strategies, i.e., any σ ∈ ΣM P,K can be represented by a Mealy machine using up to K states (c.f. [17, App. D]). For a query Q, let AchM P,K(Q) be the set of points achievable by some σ ∈ ΣM P,K.

Pure Bounded Multi-objective Achievability Problem (PBMA) Input: MDP M, multi-objective query Q, memory bound K, point *p* ∈ (R∞) Output: Yes iff *p* ∈ AchM P,K(Q)

Table 1: Results for stationary strategies.

The pure bounded Pareto approximation problem is defined similarly. We reduce a PBMA instance to an instance for PSMA. The idea is to incorporate a memory structure of size K into M and then construct a pure stationary strategy in this product MDP (see, e.g., [29] for a similar construction). The set of strategies can be further refined by considering e.g., a memory structure that only allows counting or that only remembers visits of goal states. See [17, App. D] for details.

## 6 Evaluation

We implemented our approach for PSP ≈ in the model checker Storm [16] using Gurobi [27] as back end for MILP-solving. The implementation takes an MDP (e.g., in Prism syntax), a multi-objective query, and a precision ε > 0 as input and computes an -approximation of the Pareto front. Here, we set j = ε · δj , where δj is the difference between the maximal and minimal achievable value for objective ψj . We also support reward objectives for Markov automata via [38]. The computations within Gurobi might suffer from numerical instabilities. To diminish their impact, we use the exact engine of Storm to confirm for each MILP solution that the encoded strategy achieves the encoded point. However, sub-optimal solutions returned by Gurobi may still yield inaccurate results.

We evaluate our approach on 13 multi-objective benchmarks from [24,28,38], each considering one or two parameter instantiations. Application areas range over scheduling (dpm [37], eajs [1], jobs [10], polling [43]), planning (rg [6], rover [28], serv [32], uav [21]), and protocols (mutex [38], str [38], team [15], wlan [31]).

The results for pure stationary strategies are summarized in Table 1. For each benchmark we denote the number of objectives and whether the alternative encoding from Sect. 3.4 has been applied (∗). For each parameter instantiation (Par.), the number of states (|S|), the percentage of the states that are contained in an end component (%E), and the average number of available actions at each state (Act) are given. For each precision ε ∈ {0.01, 0.001}, we then depict the

(a) Alt. (x) vs. original (y) encoding. (b) Pareto fronts for restricted strategies.

Figure 7: Comparison of the two encodings (left) and impact of memory (right).

runtime of Storm and the number of points on the computed approximation of the Pareto front. TO denotes that the approach did not terminate within 2 hours, MO denotes insufficient memory (16 GB). All experiments used 8 cores of an Intel R Xeon R Platinum 8160 Processor.

Storm is often able to compute pure stationary Pareto fronts, even for models with over 100 000 states (e.g., uav). However, the model structure strongly affects the performance. For example, the second instance of jobs is challenging although it only considers 117 states, a low degree of nondeterminism, and no (non-trivial) end components. Small increments in the model size can increase runtimes significantly (e.g., dpm or uav). If a higher precision is requested, much more points need to be found, which often leads to timeouts. Similarly, for more than 2 objectives the desired accuracy can often not be achieved within the time limit. The approach can be stopped at any time to report on the current approximation, e.g., after 2 hours Storm found 65 points for Instance 1 of mutex.

For almost all benchmarks, the objectives could be transformed to total reward objectives, making the more efficient encoding form Sect. 3.4 applicable. We plot the runtimes of the two encoding in Fig. 7a. The alternative encoding is superior for almost every benchmark. In fact, the original encoding timed out for many models as indicated at the horizontal line at the top of the figure.

In Fig. 7b we plot the Pareto front for the first polling instance under general strategies (Gen), pure 2-memory strategies that can change the memory state exactly once (PM2), pure strategies that observe which goal state set Gj has been visited already (PMG), and pure stationary strategies (PS). Adding simple memory structures already leads to noticeable improvements in the quality of strategies. In particular, PM2 strategies perform quite well, and even outperform PMG strategies (which would be optimal if randomization were allowed).

Data availability. The artifact [18] accompanying this paper contains source code, benchmark files, and replication scripts for our experiments.

Acknowledgments. The authors thank Sebastian Junges for his valuable contributions during early stages of this work.

## 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.

## Model Checking and Reachability

#### **Partial Order Reduction for Deep Bug Finding in Synchronous Hardware** *-*

Makai Mann and Clark Barrett

Stanford University, Stanford, CA 94305 USA

**Abstract.** Symbolic model checking has become an important part of the verification flow in industrial hardware design. However, its use is still limited due to scaling issues. One way to address this is to exploit the large amounts of symmetry present in many real world designs. In this paper, we adapt partial order reduction for bounded model checking of synchronous hardware and introduce a novel technique that makes partial order reduction practical in this new domain. These approaches are largely automatic, requiring only minimal manual effort. We evaluate our technique on open-source and commercial packet mover circuits – designs containing FIFOs and arbiters.

## **1 Introduction**

Modern society relies increasingly on electronic systems, powered by hardware components that continue to grow in complexity and variety. Ensuring the functional correctness of these components is essential, as bugs and errors can have consequences ranging from undermining a company's reputation to jeopardizing human safety [1,22,25,32,33]. Most electronic designs must therefore include a significant verification effort, and this effort often consumes more time and resources than all other aspects of the design process [17,34].

Formal methods such as symbolic model checking have become a crucial part of the verification effort because of their strong guarantees and automation [24]. However, due to the *state space explosion problem* [14], model checking typically only works well for small- to medium-sized circuits with primarily control logic, limiting its potential for addressing industry verification challenges.

One approach for combating the state space explosion problem is *partial order reduction* [14]. While symbolic partial order reduction has been successfully applied for the verification of asynchronous systems [37], its use in synchronous systems has been limited. In this paper, we introduce a novel approach for adapting symbolic partial order reduction to model checking of synchronous hardware

- This work was supported by the National Science Foundation Graduate Research Fellowship Program under Grant No. DGE-1656518. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation. This work was also supported by the Defense Advanced Research Projects Agency, grant FA8650-18-2-7854. We thank the funding agencies and our corporate collaborators for their support.

and demonstrate dramatic reductions in the time to reach deep bugs on certain classes of synchronous circuits. Moreover, the technique requires only an interface-level annotation of the circuit, and when fully automated approaches fail, can be guided by the user. The paper makes the following contributions:

The rest of the paper is organized as follows. We first provide a motivating example, below. Then, in Section 2, we cover relevant background material and notation. We explain our partial order reduction in Section 3 and our interface simplification technique in Section 4. We provide an experimental evaluation in Section 5. Section 6 covers related work, and Section 7 concludes.

#### **1.1 Motivating Example**

Throughout this paper we use the running example shown in Code Snippet 1. We chose this example because: i) it is easy to understand; ii) it resembles real-world packet mover circuits; and iii) it contains a difficult to reach bug.

The system has a synchronizing clock and takes two 1-bit inputs: inc x and inc y. The 6-bit registers (state elements) x and y index the valid vector and are initialized to 0. The 64-bit registers valid and data start at 0 and 1, respectively. The 64x64 bit memory is uninitialized. If inc x and en x are true, the system increments the value of x. When inc y is true, the system increments y, sets the valid bit at index y, writes data to the memory at location y, and rotates the data vector to the left. Notice that the en x signal ensures that x never surpasses y (until all bits in valid are set). This incrementing pointer logic is similar to that found in a circular pointer FIFO. To ensure the asserted property, the code attempts to maintain the invariant: data = 1 << y.

At first, it appears that the asserted property should hold based on this invariant, but it does not. There is a bug that can first occur at cycle 65: the overflow check in the data update uses integers, which are assumed to be 32 bits. Since y is zero-extended to be 32-bits, y+1 can never be equal to 0. Thus, when y has the value 63 and is incremented, data, which is supposed to be one-hot, is set to 0.

Although the system is small, this is a surprisingly difficult bug to reach using model checking. We believe this is due in part to the non-determinism in the

```
1 module deep_bug(input clk, input inc_x, input inc_y);
2 reg [5:0] x = 0;
3 reg [5:0] y = 0;
4 reg [63:0] valid = 0;
5 reg [63:0] data = 1;
6 reg [63:0] mem [63:0];
7 wire en_x;
8 assign en_x = valid[x];
9
10 always @(posedge clk) begin
11 if (inc_x & en_x)
12 x <= x + 1;
13 if (inc_y) begin
14 y <= y + 1; valid[y] <= 1'b1; mem[y] <= data;
15 data <= (y+1 == 0)?1: (data << 1);
16 end
17 end
18
19 always @*
20 assert ((mem[x] == (1 << x)) || ˜valid[x]);
21 endmodule // deep_bug
```
Code Snippet 1: Buggy Toy Example

update logic. In every state, there are 4 possible input combinations. As a result, there are an exponential number of execution paths. Model checkers routinely verify hardware designs with an exponential number of reachable states; however, we have observed that systems such as this which also have an exponential number of execution paths are difficult for a model checker to manage.

Specifically, all but two of the model checker configurations we tried timed out at 2 hours before reaching the bug. Since bounded model checking (BMC) is one of the best approaches for bug-finding, we focus on improvements to BMC that help reach this bug. We introduce automated, best effort techniques that reduce the time to hit this bug from over 1000 seconds to 46 seconds by safely adding temporal symmetry breaking constraints to the system.

## **2 Background**

Before explaining our algorithm, we adapt the standard notion of synchronous transition systems and review fundamental model checking concepts below. For a more thorough introduction to model checking, we refer the reader to [14,15].

**Definition 1.** *A Synchronous Transition System (STS) is a tuple,* -S,*Init*, A,*En*, D, T*:*

```
– S: a set of states
```
**–** *Init* ⊆ S*: a set of initial states*

For our purposes, an STS instruction can perform multiple atomic actions simultaneously. We define the system's *instruction set* (i.e. the set of actions that the system can perform in one transition) as I := P(A). We then define the set of *inputs* of an STS as *Input* := I × D. Thus, the transition relation T is a subset of S × *Input* × S.

We denote the cardinality of an instruction i as |i|. For s, s- ∈ S, *in* ∈ *Input*, T(s, *in*, s- ) holds *iff* it is possible to reach s from s by applying input *in*. It is often convenient to reason about sequences using vector notation. Let *in* ∈ *Input*n and *s* ∈ Sn+1, with n > 0. We use subscripts to name individual elements of vectors, e.g. *s* := s0, s1,.... We use the notation T(*in*, *s*) to denote - 0≤i<n T(si, *in*i, si+1). The length of a vector is given by |·|, e.g. |*s*| = n + 1, and prepending is represented as · : ·, e.g. *s* = s0 : *s* for some s- ∈ Sn. With some abuse of notation, we allow prepending both sequences and single elements. For k > 0, we say that *s* ∈ Sk is reachable if ∃n ∈ N, *s*- ∈ Sn+1,*in* ∈ *Input*n+k . *Init*(s- 0) ∧ T(*in*, *s*-: *s*).

The set of enabledness predicates *En* constrain the valid states in which an action can occur. For an instruction i ∈ I and s ∈ S, let *en*i(s) := - a∈i ena(s). In the remainder of the paper, we only consider transition relations T that respect the enabledness conditions. That is, we assume ∀ s, i.(*en*i(s) ↔ ∃ s- , d.T(s,i, d, s- )). Depending on the context, this can be checked with a model checker or added as an environmental assumption. We also assume that the existence of a transition does not depend on the data input, that is, ∀ s, i.(∃ d, s- . T(s,i, d, s- ) =⇒ ∀ d. ∃ s- . T(s,i, d, s- )).

*Example 1.* We can define an STS for the motivating example. Let *BV*k denote the set of all bitvectors of width k. Because there is only a single clock with no negative edge behavior, we model the system without the clock, where every transition corresponds to a clock cycle. Define an STS -S,*Init*, A,*En*, D, T, where:

**Model Checking.** Given an STS **S**, let a safety property P ⊆ S be a set containing acceptable states. The *model checking problem* is to determine whether the system stays within this acceptable set for all possible execution traces. Formally, we want to check whether the following holds:

$$\forall n \ge 0, \dot{m} \in Input^n, \mathbf{s} \in S^{n+1}. \left( Int(s\_0) \land T(\dot{m}, \mathbf{s}) \right) \implies s\_n \in P \tag{1}$$

When equation (1) holds, we say that P is an invariant of **S**. A number of techniques exist for solving this problem, including Binary Decision Diagram (BDD)-based [12] approaches, Interpolant-based [27] approaches, and IC3/PDR (property directed reachability) techniques [10,16]. We refer the interested reader to [15] for a more complete survey of model checking algorithms.

In this paper, we will focus on *bounded model checking* (BMC). In BMC, instead of proving (1) for all n, we prove it for all n less than some finite bound k. Though it typically cannot be used to prove properties, BMC can be quite effective at finding bugs [6] and is especially useful when full model checking is infeasible.

**Symmetry.** Early on in the development of model checking, researchers recognized the importance of symmetry reduction to combat the state explosion problem [13]. Existing approaches in the hardware domain perform data symmetry reduction and data type reduction through the use of bit-width reduction preprocessing passes or syntactic restrictions such as *scalarsets* [8,20,28]. There have also been abstraction-refinement loop algorithms proposed to handle memory symmetries [9]. All of these approaches are focused on symmetries present in the transition system description, such as the presence of large data types. We refer to these types of symmetries as *data* symmetries. Most of these techniques are intended to speed up proofs of true properties rather than accelerate bug-finding.

Model checking of asynchronous systems such as concurrent programs faces an orthogonal issue due to the many possible redundant interleavings of independent processes. Throughout this paper, we refer to this as *path* symmetry. Path symmetry is a temporal symmetry: it relates to executions of a system rather than just its size. Path symmetries occur when there are many distinct ways of reaching the same state in a system execution. Exploring all such paths can result in exponential case splitting.

This paper provides evidence that path symmetry can also severely hurt model checking performance in synchronous systems. One of the first techniques proposed to handle path symmetry was partial order reduction.

**Partial Order Reduction.** Partial order reduction was first developed in the explicit-state model checking context but was later extended to symbolic model checking [37]. The approach is named "partial order reduction" for historical reasons, but Clarke noted in [14] that "model checking using representatives" [30,31] may have been a more appropriate name. In particular, partial order reduction attempts to develop equivalence classes of behaviors so that only one representative from each class needs to be considered during model checking. Note that

partial order reductions are sound only for checking state invariants. If the property of interest is temporal, the reduction could disallow input sequences that trigger the property. This can be avoided by first instantiating a monitor [15] and, if necessary, converting liveness properties to safety [5].

Partial order reduction is less natural in the synchronous setting, because synchronous transition systems do not have easily expressible independent actions. Nevertheless, these systems can still benefit from partial order reduction. Consider our motivating example: despite the huge number of system execution paths to consider, many of them are redundant. Observe that if both inputs are zero, then the state does not change. Furthermore, there is a temporal symmetry in the system execution: from any state where en x is true, driving only inc x followed by only inc y results in the same state as driving them in the opposite order. Thus, this system has a large number of redundant interleavings, much like a multi-threaded program. To address this problem, we introduce a partial order reduction for synchronous hardware. Our goal is to remove redundant interleavings by adding constraints to the system. To maintain soundness, we provide a set of conditions which must pass before we can add constraints.

## **3 Synchronous Partial Order Reduction**

In order to be able to apply partial order reduction to a synchronous transition system, we are interested in identifying pairs of instructions that can be reordered without affecting the resulting state. More generally, we also want to be able to find pairs that can only be reordered under certain conditions. To formalize these notions, we adapt the notation and representation of *guarded independence relations* from [37].1

**Definition 2.** *Given an STS:* -S,*Init*, A,*En*, D, T *with instruction set* I*, let* G := P(S) *be the set of predicates over the states. Let* i0, i1, g *be a* guarded independence tuple *iff for all* d0, d1 ∈ D *and reachable s* ∈ S3*, the following condition holds:*

*en*i0 (s0)∧g(s0)∧T(-i1, d1,i0, d0, *s*) =⇒ ∃ s- .T(-i0, d0,i1, d1,s0, s- , s2).

According to this definition, if we can prove that i0, i1, g is a guarded independence tuple, then we can reorder i1, i0 instruction sequences as long as i) i0 is enabled in the first state; ii) g holds in the first state; and iii) we also reorder the corresponding data inputs. We check only the enabledness of i0 because i0, i1 is the representative order, and we only need to be able to reorder to the representative, not from it. The guard allows us to consider partial order reductions that only hold for a subset of the reachable states. To avoid trivially overconstraining the system with conflicting reorderings, we will only consider one ordering for each pair of instructions.

The condition in Definition 2 is difficult to check automatically because of the existential quantifier. We instead check two slightly weaker conditions that

1 The main differences are our STS formalism and that we consider reachability.

Fig. 1: Partial Order Reduction Condition (3) Proof Goal

imply guarded independence. These conditions are also standard in the POR literature [14,37]. The first condition states that instruction i0 cannot disable i1 under guard g:

$$\forall d \in D, \mathbf{s} \in S^2. \left( en\_{i\_1}(s\_0) \land g(s\_0) \land T(s\_0, \langle i\_0, d \rangle, s\_1) \right) \implies en\_{i\_1}(s\_1) \tag{2}$$

Intuitively, this condition ensures that we do not remove reachable states by disabling instructions. The second condition is that executing the instructions in either order leads to the same final state:

$$\begin{aligned} \forall d\_0, d\_1 \in D, \mathbf{s}, \mathbf{s}' \in S^3 \ &\ (g(s\_0) \land (s\_0 = s\_0') \land \\ T(\langle \langle i\_0, d\_0 \rangle, \langle i\_1, d\_1 \rangle \rangle, \mathbf{s} \rangle \land T(\langle \langle i\_1, d\_1 \rangle, \langle i\_0, d\_0 \rangle \rangle, \mathbf{s}')) \implies (s\_2 = s\_2') \end{aligned} \tag{3}$$

When applying partial order reduction to concurrent programs, the standard approach is to check conservative syntactic properties which guarantee conditions (2) and (3). Synchronous systems do not typically have these syntactic properties, because there is no notion of distinct processes. Instead, we must check these conditions directly. In real circuits, it is unlikely that (2) will hold over arbitrary states. However, it is sufficient to prove that it holds for all reachable states. This can be done with a model checker.

To prove (3), we could encode it as an LTL property or build a monitor automaton and use a model checker. Alternatively, we have found that we can often use a straightforward commuting-diagram approach starting from a symbolic initial state, depicted in Fig. 1. We duplicate the system, unroll it twice, then start both copies in the same symbolic state and check that applying the instructions in either order results in the same final state. This simple approach has the disadvantage that a symbolic initial state ignores reachability which could lead to spurious counterexamples. However, notice that the initial state is constrained by enabledness assumptions. To apply an instruction it must be enabled, so both instructions must be enabled in the initial state. We have found that these enabledness assumptions often constrain the initial state enough to rule out spurious counterexamples.

If both conditions pass, then we can choose a representative order and disallow the opposite ordering for that pair of instructions. If the proof of condition (3) fails, it provides a counterexample which should either convince the user that partial order reduction does not apply for that pair of instructions (a real counterexample), or serve as a guide for the user to write guards that would remove the spurious counterexample. Other invariants of the system, either obtained automatically or manually guessed by the user, could also remove spurious counterexamples. We can now state the first theorem of synchronous partial order reduction: that these conditions guarantee guarded independence over all reachable states.

**Theorem 1.** *Given an STS* **S** := -S,*Init*, A,*En*, D, T*, with instruction set* I := P(A)*: if conditions* (2) *and* (3) *hold for instructions* io, i1 ∈ I*, and guard* g ∈ P(S)*, then* i0, i1, g *is a guarded independence tuple.*

*Proof.* Assume conditions (2) and (3) and that for some d0, d1 ∈ D and reachable *s* ∈ S3, we have:

$$\operatorname{en}\_{i\_0}(s\_0) \land g(s\_0) \land T(\langle \langle i\_1, d\_1 \rangle, \langle i\_0, d\_0 \rangle \rangle, \mathbf{s})$$

Because eni0 (s0), we have ∃s- , d- . T(s0,i0, d- , s- ) because of our enabledness assumption. Furthermore, by the data-input independence property of transition relations, it follows that for some s- 1, T(s0,i0, d0, s- 1) Now, because one of our assumptions is a transition from s0 using i1, eni1 (s0) must be true. Condition (2) implies that eni1 (s- 1), thus ∃ s- , d- . T(-i0, d0,i1, d- ,s0, s- 1, s- ). As before, this implies that for some s- 2, we also have that T(-i0, d0,i1, d1,s0, s- 1, s- 2). It then follows from (3) that s- 2 = s2, and thus, i0, i1, g satisfies the condition from Definition 2. -

Let a guarded independence relation, R ⊆ I×I× G, be a set of guarded independence tuples. We now describe how to apply partial order reductions, given some R. For each i0, i1, g ∈ R, and for every *s* ∈ S2, d ∈ D, whenever T(s0,i1, d1, s1)∧eni0 (s0)∧g(s0) holds, we remove from T every transition of the form s1,i0, d, s (for any d and s). Let T R be the result. To apply this reduction in practice, we add a constraint to the BMC encoding: (g(s0)∧eni0 (s0)∧i1) =⇒ ¬*next*(i0).

This makes it impossible for the STS system to ever execute an instruction i0 after an instruction i1 when starting from a state where i0 is enabled and g holds. This effectively gives preference to i0 as long as it is enabled. The effect of partial order reduction on a pair of instructions in a synchronous system is depicted in Fig. 2. Red X's show removed transitions, and for simplicity, we assume a trivial guard of *true*. Notice that all states are still reachable via some path from the initial state in the bottom left corner.

**Theorem 2.** *Given* **S** := -S,*Init*, A,*En*, D, T*, let* R *be a guarded independence relation and let* **S**R *be the* reduced *STS obtained by replacing* T *with* T R *in* **S***. Then, if a property* P *is an invariant for* **S**R*, it is also an invariant for* **S***.*

Fig. 2: Effect of Partial Order Reduction for Instructions i0 and i1. Initial state is green.

*Proof.* It suffices to show that **S**R can reach all the same states as **S**. We prove this by contradiction. Assume there is some *in*, *s* such that *Init*(s0)∧T(*in*, *s*) and 0 ≤ j ≤ |*s*|−1 such that sj is the first state that is unreachable in SR. The value of j cannot be 0 or 1, because **S** and **S**R have the same initial states and T R only excludes sequences of length 2. Then, by the definition of TR, *in*j−2, *in*j−1 must be a sequence excluded by T R. Conditions (2) and (3) guarantee that permuting *in*j−2 and *in*j−1 results in an enabled sequence that ends in the same state, sj , which contradicts the assumption. Thus, there cannot be a state which is reachable in **S** but not **S**R. -

## **4 Reduced Instruction Sets**

Now that we can apply partial order reduction to synchronous systems, our main goal is to identify a maximal guarded independence relation, R. Recall that we defined instructions as sets of atomic actions. We call an instruction containing at most one action *atomic* (this includes the instruction with *no* actions). Non-atomic instructions are *complex*. Instructions thus reflect the parallelism of synchronous hardware, and lead to natural candidates for R: pairs of atomic instructions.

Furthermore, notice that the number of instructions is exponential in the number of actions. Thus, it could be prohibitively expensive to check every pair of instructions for guarded independence. In contrast, the number of *atomic* instructions is equal to the number of actions (plus one). Furthermore, it is likely that many complex instruction pairs will not have a guarded independence relationship because they contain common actions. Our goal in this section is to disallow as many complex instructions as possible without losing any reachable

states, thereby reducing the number of pairs of instructions we need to check while also making it more likely for the checks to succeed. Note that, in isolation, removing instructions might be problematic, because it could extend the bound needed to reach a property violation. However, as we will demonstrate in the experimental section, this disadvantage is more than compensated for when it is applied in combination with partial order reduction.

Given an STS with instruction set I, we seek a reduced instruction set, Ir ⊆ I, which preserves the reachable states of the system. Let *Input* r be the set of inputs which only use instructions from Ir. Given an input *in* ∈ *Input*, our goal is to prove the existence of a witness w(*in*) ∈ *Input*n r (for some n > 0) that simulates the behavior of *in* using only reduced instructions. Formally, the witness function w should satisfy:

$$\begin{aligned} \forall s, s' \in S, in &\in Input. \, T(s, in, s') \implies \\ \exists n \in \mathbb{N}, s \in S^n. \, T(w(in), s: \mathbf{s}) \land (s\_{n-1} = s') \end{aligned} \tag{4}$$

In other words, we need to show that for every instruction in the original instruction set, there exists a sequence of inputs, using only instructions from the reduced instruction set (RIS), that results in the same final state. Notice that a witness function that also depended on the state would be more general, but for our purposes, it is sufficient for the witness function to depend only on the input.

#### **4.1 Atomic instruction sets**

The condition in (4) is quite general and does not provide any intuition on how to choose w. Here, we focus on a specific case where w is easy to construct: we choose Ir to be an *atomic instruction set*, defined as an instruction set containing only atomic instructions. We then must prove that the set of reachable states is not affected by restricting the instructions to those in Ir.

It is sufficient to prove that for each complex instruction, we can remove one of its actions and perform that action in the next step, with the same result. For some complex instruction i containing a and some data input d, let wa(i, d) be -i−{a}, d,-{a}, d. We must show that for each input *in* containing a complex instruction, there exists some a where wa(*in*) has the equivalent effect on the system as *in*. Formally, the requirement is:

$$\begin{aligned} \forall i \in \mathcal{I} \; & \; \mathcal{I}\_r, d \in D, \mathbf{s} \in S^2. \\ \quad & T(s\_0, \langle i, d \rangle, s\_1) \implies \exists \; a \in i, \mathbf{s}' \in S^3. \; T(w^a(\langle i, d \rangle), \mathbf{s}') \land s\_0 = s\_0' \land s\_1 = s\_2' \end{aligned} \tag{5}$$

Condition (5) is still difficult to prove because of the existential quantifier. One conservative approach is to replace the existential quantifier with a universal quantifier and attempt to prove that stronger condition. For real systems, this is unlikely to hold. Instead, we propose a counterexample blocking procedure which, if it succeeds, guarantees (5). We introduce symbolic values for i, d, and a and then iteratively add constraints over them until the proof succeeds or

Fig. 3: Equivalence of original and reduced instruction sequences. Circles represent states.

we have enumerated all possibilities. This algorithm is a specialized ∀∃ decision procedure that exploits the structure of (5) and additional domain knowledge about the proof goal. We use a constraint solver as an oracle.

#### **Algorithm 1 ProveRIS(S)**

1: **S**- := -S- ,Init- , A- ,En- , D- , T- ← copy sys(**S**) 2: I := P(A), I- := P(A- ) // instruction sets are power sets of actions 3: **var** i : I, **var** i - : I- , **var** a : A 4: **var** *s* : S2, **var** *s*- : S-3, **var** d : D, **var** d- : D- 5: add constraint(s0 = s- 0 ∧ d = d- ∧ i - = i − {a}) 6: add constraint(T(-i, d, *s*) ∧ T- (-i - , d- ,-{a}, d- , *s*- )) 7: **for** c = 2 ... |A| **do** 8: **while** check sat(|i| = c ∧ s1 = s- 2) **do** 9: μ ← get model() 10: iμ ← assignment(μ, i) 11: aμ ← assignment(μ, a) 12: add constraint(iμ ⊆ i =⇒ a = aμ) 13: **if** ¬check sat(i = iμ) **then** 14: **return** false // exhausted all possible decompositions for this instruction 15: **end if** 16: **end while** 17: **end for** 18: **return** true // every instruction can be decomposed

Algorithm 1 takes an STS, **S** := -S,*Init*, A,*En*, D, T and returns true if the instruction set can be decomposed into an atomic instruction set by delaying a single action from each instruction.2 For simplicity, the algorithm assumes (and we check this assumption separately) that if a complex instruction i is enabled, then for each a ∈ i, executing i − {a} results in a state where a is enabled.

2 We also implemented a more general version of this algorithm which can drop more than one action at a time from the instruction i, but this simpler version is sufficient for the results we report in this paper.

Formally:

$$\forall i \in \mathcal{T} \left< \mathcal{Z}\_r, d \in D, \mathbf{s} \in S^2, a \in i. \text{ } en\_i(s\_0) \land T(s\_0, \langle i - \{a\}, d \rangle, s\_1) \implies en\_a(s\_1) \quad (6)$$

Note that this is only a slight generalization of the property that atomic instructions do not disable each other, a condition that we will need anyway in order to apply partial order reduction to the atomic instruction set (see condition (2)).

The algorithm first creates an identical copy of the STS in line 1. Lines 2-4 set up symbolic variables for the instructions, data, and states of each system. Line 5 adds constraints to the solver enforcing that both systems start in the same state, use the same data, and that i is i but with symbolic action a dropped. Line 6 adds the transition relation constraint for each STS. The initial symbolic set up is depicted in Fig. 3.

The outer loop at line 7 iterates over all possible complex instruction cardinalities. The inner loop starting at line 8 attempts to show that for each cardinality c, instructions of that cardinality can be decomposed by delaying one action (symbolically represented by a). If all instructions of cardinality c have been decomposed, then the while loop condition is false and the outer loop continues. Otherwise, it gets variable assignments from the constraint solver in lines 9-11 and learns a constraint at line 13 that prevents this particular action, aμ, from being chosen for decomposition again. To ensure that we have not blocked all possible actions, there is an additional check at line 13, which returns false in the case that no action can be delayed for the current instruction.

Importantly, the algorithm assumes that if the delay of action aμ does not create a valid witness sequence for a given complex instruction iμ, then the same is true *whenever* the instruction i includes iμ. We call this a *monotonicity* assumption, and it typically holds when actions are somewhat independent. The monotonicity assumption motivated the current structure of the algorithm and can significantly reduce the number of iterations in the algorithm. We can remove this assumption by changing iμ ⊆ i to iμ = i in the antecedent in line 13. Note that the monotonicity assumption does not make the algorithm unsound: if it returns true, then (as we prove below) condition (5) holds. However, if the algorithm returns false, then it may be that the version without the assumption would return true. For each of our experiments, we were able to get a true result with the monotonicity assumption.

Because the algorithm does not consider state reachability and looks for a witness function that only depends on inputs, it can still return false when an equivalent sequence might exist for reachable states. In such cases, users can examine the constraint solver models and attempt to remove some of them by proving other invariants.3

If algorithm 1 returns true, we replace T with Tr, where Tr is the result of removing from T all transitions s,i, d, s- where |i| > 1. Practically, this is

3 This was rarely necessary in our experiments. Our implementation also extended the algorithm to support predicate abstraction, which could also rule out spurious counterexamples, but this feature was never needed in our experiments.

achieved by adding a disjunctive constraint over the possible atomic actions. We can now state the main results for reduced instruction sets.

**Theorem 3.** *Let* S *be an STS. If condition* (6) *holds and ProveRIS(***S***) returns true, then* (5) *holds.*

*Proof.* We maintain the loop invariant at line 8 that for every instruction i - , there is some action a such that *check sat*(|i| = c ∧ i = i - ∧ a = a- ) is true. It's true initially for each c by condition (6). Afterwards, the check on line 14 ensures that it is maintained. Furthermore, the check on line 9 ensures that when the while loop is exited, then any satisfying assignment for *check sat*(|i| = c) is such that s1 = s- 2. Together, these conditions guarantee that (5) holds.

**Theorem 4.** *Let* **S** := -S,*Init*, A,*En*, D, T *be an STS such that condition* (6) *holds and ProveRIS(***S***) returns true, and let* Tr *be the transition relation for the reduced instruction set. Let* **S**r *be the* reduced *STS obtained by replacing* T *with* Tr *in* **S***. Then, safety property* P ∈ S *is an invariant for* **S**r *if and only if it is also an invariant for* **S***.*

*Proof.* It suffices to show that the reachable states of **S** and **S**r are identical. *Init* does not change, so the initial states cannot be different. Furthermore, Tr is obtained by removing transitions from T, we know that Sr cannot add any reachable states. To show that it also does not remove any reachable states, consider an arbitrary trace *Init*(s0) ∧ T(*in*, *s*) with |s| = n, we must show ∃ *in-* , m, *s-* ∈ Sm.*Init*(s- 0)∧Tr(*in-* , *s-* )∧sn−1 = s- m−1. We prove this by showing by induction that it holds whenever *in* contains instructions of cardinality at most c.

In the base case, c = 1, so all instructions are of size one or less. All of these are already atomic and thus we can take *in-* = *in* and *s-* = *s* by the definition of Tr.

For the inductive step, suppose that it holds for cardinalities up to c−1, and assume *Init*(s0) ∧ T(*in*, *s*) with |s| = n. Let *in*j = i, d be an input containing an instruction of size at most c. If |i| < c, there is nothing to be done. Thus we only consider the case where |i| = c. We know that T(sj , *in*j , sj+1) holds. By Theorem 3 and condition (5), it follows that T(-i−{a}, d,-{a}, d,sj , s, sj+1) holds for some a and s. We can thus replace *in*j in *in* by i − {a}, d followed by -{a}, d to obtain an input sequence *in*c and insert s between sj and sj+1 in *s* to obtain *s*c with final state sn−1 such that *Init*(s0) ∧ T(*in*c, *s*c). Repeating this process for each input containing an instruction of size c yields a final *in*c such that the maximum cardinality of any instruction is c−1. The property then holds by the inductive hypothesis. -

Note that if there is some instruction i ∈ I which cannot be decomposed into atomic instructions, we could always keep this instruction in Ir and still benefit from removing other complex instructions. In many cases, we can also remove the empty instruction, ie = ∅. If applying ie cannot change the state of the system, regardless of the data input, then it is considered a *stutter step* [14]. It is straightforward to check whether ie can be removed by comparing the state before and after applying ie.

## **5 Experimental Results**

We developed a prototype flow for proving the POR and RIS conditions and applying the necessary constraints. We use the IC3/PDR implementation in ABC [11], pdr, to prove condition (6) (which implies condition (2)). This requires manually writing a Verilog property for each atomic instruction.4 We implemented the **ProveRIS** algorithm in our SMT-based model checker, CoSA [26], configured with boolector [29] on the smtcomp19 branch, using CaDiCaL [4] as the underlying SAT solver.5 We check the commuting diagram for condition (3) in CoSA as well. It tries the trivial guard true by default, and allows the user to provide additional candidate guards if necessary. The set up for proofs in CoSA is automated based on user-provided annotations for the actions and enable conditions. We show our best results which used an encoding leveraging the SMT theory of arrays to represent memories for proving conditions, and a pure bitvector encoding for bounded model checking.

Our flow applies the following steps: i) read in a system description in Verilog using Yosys [38] and generate AIGER [7] for ABC (or BTOR2 [29] for other tools); ii) check condition (6) for each atomic instruction; iii) run the **ProveRIS** algorithm, and if it returns true, add constraints to rule out all but atomic instructions; and iv) check POR condition (3) for each pair of atomic instructions and add constraints for each passing pair of instructions with the associated guard. Each step depends on the previous step passing successfully. In each of our experiments described below, we successfully completed every step of this flow, though in some cases guards were required in step (iv). For POR and RIS runtimes, we always include the time to check the conditions. We tried running with POR alone, but it resulted in negligible improvements in runtime and thus we omit these results. This demonstrates the importance of RIS. We ran all experiments on a 3.5GHz Intel Xeon CPU with 16GB of RAM.

#### **5.1 Motivating Example**

First, we return to our motivating example. We compare the time to reach the bug using the SAT-based ABC [11] engines pdr and bmc, and SMT-based bounded model checking using btormc [29] and CoSA. We ran the SMT-based model checkers both with and without the SMT theory of arrays for the encoding of the memory. Both btormc and CoSA without the array encoding were able to reach the bug in 1230s and 1437s, respectively, but all other approaches timed out at two hours. In particular, pdr times out at 2 hours on the property, but can

4 This could be automated based on user-tagged actions and user-provided enable conditions.

5 GitHub Commit Hashes for Tools: Boolector/Btormc:<PHONE_NUMBER>235f33e344cbd095e70a337c45bd16 CoSA: ff3c8cee1f0834c03167b2a8ecdd1223031312b3 PySMT: 09dc303185812149550110123ad266326beb1179 Yosys: a4b59de5d48a89ba5e1b46eb44877a91ceb6fa44 ABC: 5776ad07e7247993976bffed4802a5737c456782

Table 1: Number Solved and Average Runtime Fig. 4: Runtime Comparison

prove condition (6) for every atomic instruction in less than a second. Intuitively, this makes sense because the enabledness conditions do not involve data or mem. Thus, none of the datapath falls in the cone of influence, leaving only control logic for IC3 to reason about. The remaining conditions, (3) and (5), are proven in less than three seconds. Since all the conditions pass, we apply the POR and RIS constraints, which reduces the time to hit the bug from 1437s to 46s in CoSA, including the time to check the conditions.

#### **5.2 Packet Movers**

We now evaluate our approach on data integrity properties for a variety of packet-mover circuits. Data integrity is a safety property that ensures no packets are dropped or corrupted. In practice, data integrity is often checked by instantiating a monitor, called a *scoreboard*. It provides the necessary infrastructure for formal verification. In our case, it non-deterministically tags a *magic packet* and checks that this packet exits the system when it should. Crucially, the scoreboard is a reusable module which can check data integrity of arbitrary packet movers.

Notice that existing symmetry reduction techniques will not be very effective for this scoreboard setup. For example, consider a circular pointer FIFO which maintains two incrementing pointers that index a memory for reading and writing, respectively. We cannot use scalarsets to break symmetries in the memory addresses because the pointers index the memory and are involved in arithmetic, breaking the syntactic requirements for scalarsets [28]. Furthermore, sequential memory abstraction [9] could reduce the size of the memory, but does not address the path symmetry. In addition, both these symmetry reduction techniques are focused on proofs, not bug-finding.

We evaluate our approach on two commercial library components from a major hardware company. We also implemented simpler, open-source versions of these designs. Our open-source benchmarks include: i) a circular pointer FIFO which assumes power-of-two depth but is instantiated with a non-power-of-two depth (one greater than the provided parameter); ii) a shift register FIFO which does not properly add data to the last register in the pipeline; and iii) 2-5

correct circular pointer FIFOs in parallel with a non-deterministic arbiter and credit counters for managing data flow. The reset state of the credit counter has one too many credits, so data can be pushed to a full FIFO. The single FIFOs have two actions each: one for pushing data, and one for popping data. For the arbitrated circuits, there is a separate action for pushing data onto each FIFO as well as a single request action which is enabled whenever any FIFO is non-empty. There is an inherent symmetry in all of these designs. Consider any of the FIFOs. There are two main actions: pushing data (which is enabled if the FIFO is not full); and popping data (which is enabled if the FIFO is not empty). In a state where both are enabled, pushing data followed by popping results in the same state as popping and then pushing the same data. Furthermore, the actions can be performed simultaneously, but requiring that they are performed separately should not change the reachable states (depending on the implementation), so RIS is applicable.

Our experiments vary both the parameterizable data width and depth of the packet movers, by sweeping all powers of two between 2 and 128. All benchmarks contain injected bugs and reach the bug at a deep bound relative to the depth. We used a timeout of 4 hours. We use our prototype flow for checking the conditions and CoSA for bounded model checking.6 For condition (3), we had to write one guard which is true whenever the scoreboard counter is greater than zero to handle an edge case. This same guard was used for every design, but an appropriate invariant relating the scoreboard counter to the internal state of the system being verified would also have worked. The open-source shift register FIFO required one more guard about the number of stored elements. We obtained both guards by observing counterexamples.

Table 1 compares the number of solved instances (49 total per row) within the timeout and the average runtime of commonly solved instances in seconds. Columns marked "PR" used the POR and RIS constraints. We additionally use the following abbreviations: "com" for commercial, "cp" for circular pointer, "sr" for shift register and "arb" for arbitrated. In Fig. 4 we plot the actual runtime on a log-scale for all the benchmarks with and without POR and RIS. The dotted lines show 10x and 100x improvements.

**Analysis.** There is a cluster of points in the bottom left of Fig. 4 which are solved extremely quickly by both approaches, but slightly faster without POR and RIS. These are results on benchmarks with very small parameter values, where the bug occurs at a low depth, and so the POR and RIS results are dominated by the time taken to check the conditions. However, as the parameter sizes, and runtimes, increase, it is clear that POR and RIS can result in exponential speed ups.

Recall that one concern is that RIS could extend the bound needed to reach the bug. In the shift register and arbitrated FIFO systems, it extended the bound by a few steps. However, for the bug in the open-source circular pointer FIFO, it doubled the bound needed to reach the bug. Regardless, this was more than

6 Note: CoSA's bounded model checking performance is comparable to commercial model checkers on these benchmarks.

compensated for by the symmetry-breaking of POR, as evidenced by the faster times to reach the bug. The deepest bound was 260 which occurred at FIFO depth 129.

It is interesting to note that encoding the transition systems to SMT using the theory of arrays was always slower for bounded model checking, but was noticeably faster for checking RIS and POR conditions. Perhaps this is because the state comparison is easier for the solver to reason about using array extensionality [23].

We have demonstrated that these techniques work well for packet movers. In part, this is because packet movers are often well-constrained by their environmental assumptions, and their behavior is largely independent of incoming data values. Furthermore, we typically expect the POR and RIS conditions to hold for a correct packet-mover implementation, so a failure in a condition could identify a bug.

## **6 Related Work**

Various techniques have been employed to accelerate bounded model checking. The authors of [19] use BDDs to accelerate BMC, and the techniques introduced in [35,36] exploit the structure of BMC queries to help the SAT solver. The authors of [18] take advantage of structural information with an SMT framework tailored for BMC. Our technique is similar in that we speed up bounded model checking by adding constraints to the transition system, but we obtain constraints using partial order reduction analysis.

Wang et al. [37] pioneered partial order reduction for symbolic software model checking, guaranteeing optimal reduction for two threads. Their follow-up paper, [21], extended this framework to find the optimal reduction for any number of threads. We adapted their symbolic POR technique for synchronous hardware model checking, and developed reduced instruction sets to improve the efficacy of POR in this new domain. Bhattacharya et al. used a SAT solver to directly check guarded independence conditions (as opposed to checking syntactic properties) for asynchronous rule-based languages [3]. We also check conditions directly, but in a synchronous setting.

The techniques developed by McMillan, *temporal case splitting* and *path splitting* [28], provide a framework for splitting on possible values at a given timestep. These approaches deal with system executions, but still rely on breaking data symmetries for performance. In contrast, our techniques focus on mitigating path symmetries.

The work of Bengtsson et al. [2] extended POR to timed automata using a local-time desynchronization of clocks, followed by resynchronization with an added global clock. Similarly, our techniques adapt POR by modifying the system. However, our approach targets a different domain, and only modifies the original system by adding constraints.

## **7 Conclusion**

We have presented a set of conservative conditions over transition systems and automated techniques for proving these conditions. If the conditions can be proved, then constraints can be added to the system that break path symmetries. We evaluated our approach on parameterized open-source and commercial packet-mover circuits and demonstrated significant improvements in bounded model checking performance.

Some potential future work includes improvements to the **ProveRIS** procedure, investigating applications of partial order reduction to sequentially-composed packet movers, developing more targeted condition proofs by associating actions with particular data inputs, and building an interactive tool which helps the user identify and manage reduced instruction sets and partial order reductions.

## **8 Data Availability Statement**

The experimental results and the necessary software for reproducing results in a standard Ubuntu 18.04 installation are available in the Figshare repository: https://doi.org/10.6084/m9.figshare.11874687.

## **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.

### **Revisiting Underapproximate Reachability for Multipushdown Systems***-*

S. Akshay1, Paul Gastin2, S Krishna1, and Sparsa Roychowdhury1

1 IIT Bombay, Mumbai, India 2 ENS Paris-Saclay, Paris, France

**Abstract** Boolean programs with multiple recursive threads can be captured as pushdown automata with multiple stacks. This model is Turing complete, and hence, one is often interested in analyzing a restricted class that still captures useful behaviors. In this paper, we propose a new class of bounded underapproximations for multi-pushdown systems, which subsumes most existing classes. We develop an efficient algorithm for solving the under-approximate reachability problem, which is based on efficient fix-point computations. We implement it in our tool BHIM and illustrate its applicability by generating a set of relevant benchmarks and examining its performance. As an additional takeaway BHIM solves the binary reachability problem in pushdown automata. To show the versatility of our approach, we then extend our algorithm to the timed setting and provide the first implementation that can handle timed multipushdown automata with closed guards.

**Keywords:** Multipushdown Systems · Underapproximate Reachability · Timed pushdown automata.

## **1 Introduction**

The reachability problem for pushdown systems with multiple stacks is known to be undecidable. However, multi-stack pushdown automata (MPDA hereafter) represent a theoretically concise and analytically useful model of multi-threaded recursive programs with shared memory. As a result, several previous works in the literature have proposed different under-approximate classes of behaviors of MPDA that can be analyzed effectively, such as Round Bounded, Scope Bounded, Context Bounded and Phase Bounded [18,19,27,14,20,28]. From a practical point of view, these underapproximations have led to efficient tools including, GetaFix [21], SPADE [23]. It has also been argued (e.g., see [24]) that such bounded underapproximations suffice to find several bugs in practice. In many such tools efficient fix-point techniques are used to speed-up computations.

We extend known fix-point based approaches by developing a new algorithm that can handle a larger class of bounded underapproximations than the well-known bounded context and bounded scope underapproximations for

c The Author(s) 2020

-Partly supported by UMI ReLaX, DST/CEFIPRA/INRIA project EQuaVe & TCS.

https://doi.org/10.1007/978-3-030-45190-5\_21 A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 387–404, 2020.

multi-pushdown systems while remaining efficiently implementable. Our algorithm works for a new class of underapproximate behaviors called hole bounded behaviors, which subsumes context/scope bounded underapproximations, and is orthogonal to phase bounded underapproximations. A "hole" is a maximal sequence of push operations of a fixed stack, interspersed with well-nested sequences of any stack. Thus, in a sequence α = βγ where β = [push1(push2push3 pop3pop2)push1(push3pop3)]10 and γ = push2push1pop2pop1(pop1) 20, β is a hole with respect to stack 1. The suffix γ has 2 holes (the push2 and the push1). Thus we say that α is 3-hole bounded. On the other hand, the number of context switches (and scope bound) in α is > 50. A (k-)hole bounded sequence is one such, where, at any point of the computation, the number of "open" holes are bounded at this point (by k). We show that the class of hole bounded sequences subsumes most of the previously defined classes of underapproximations and is, in fact, contained in the very generic class of tree-width bounded sequences. This immediately shows decidability of the reachability problem for our class.

Analyzing the more generic class of tree-width bounded sequences is often much more difficult; for instance, building bottom-up tree automata for this purpose does not scale very well as it explores a large (and often useless) state space. Our technique is radically different from using tree automata. Under the hole bounded assumption, we pre-compute information regarding well-nested sequences and holes using fix-point computations and use them in our algorithm. Using efficient data structures to implement this approach, we develop a tool (BHIM) for Bounded Hole reachability in Multi-stack pushdown systems.

## **Highlights of** BHIM.

• Two significant aspects of the fix-point approach in BHIM are: (i) we efficiently solve the binary reachability problem for pushdown automata. i.e., BHIM computes all pairs of states (s, t) such that t is reachable from s with empty stacks. This allows us to go beyond reachability and handle some liveness questions; (ii) we pre-compute the set of pairs of states that are endpoints of holes. This allows us to greatly limit the search for an accepting run.

• While the fix-point approach solves (binary) reachability efficiently, it does not a priori produce a witness of reachability. We remedy this situation by proposing a backtracking algorithm, which cleverly uses the computations done in the fixpoint algorithm, to generate a witness efficiently.

• BHIM is parametrized with respect to the hole bound: if non-emptiness can be checked or witnessed by a well-nested sequence (this is an easy witness and BHIM looks for easy witnesses first, then gradually increases complexity, if no easy witness is found), then it is sufficient to have the hole bound 0. Increasing this complexity measure as required to certify non-emptiness gives an efficient implementation, in the sense that we search for harder witnesses only when no easier witnesses (w.r.t this complexity measure) exist. In examples described in the experimental section, a small (less than 4) bound suffices and we expect this to be the case for most practical examples.

• Finally, we extend our approach to handle timed multi-stack pushdown systems. This shows the versatility of our approach and also requires us to solve several technical challenges which are specific to the timed setting. Implementing this approach in BHIM makes it, to the best of our knowledge, the first tool that can analyze timed multi-stack pushdown automata with closed guards.

We analyze the performance of BHIM in practice, by considering benchmarks from the literature, and generating timed variants of some of them. One of our benchmarks is a variant of the Bluetooth example [11,23], where BHIM was able to catch a known race detection error. Another interesting benchmark is a model of a parameterized multiple producer consumer example, having parameters M,N on the quantities of two items A, B produced. Here, BHIM could detect bugs by finding witnesses having just 2 holes, while, it is unlikely that existing tools working on scope/context bounded underapproximations can handle them as the number of scope/context switches is dependent on M,N (in fact, it is twice the least common multiple of M and N). In the timed setting, one of the main challenges has been the unavailability of timed benchmarks; even in the untimed setting, many benchmarks were unavailable due to their proprietary nature. Due to lack of space, proofs, technical details and parametric plots of experiments are in [4].

**Related Work**. Among other under-approximations, scope bounded [27] subsumes context and round bounded underapproximations, and it also paves path for GetaFix [21], a tool to analyze recursive (and multi-threaded) boolean programs. As mentioned earlier hole boundedness strictly subsumes scope boundedness. On the other hand, GetaFix uses symbolic approaches via BDDs, which is orthogonal to the improvements made in this paper. Indeed, our next step would be to build a symbolic version of BHIM which extends the hole-bounded approach to work with symbolic methods. Given that BHIM can already handle synthetic examples with 12-13 holes (see [4]), we expect this to lead to even more drastic improvements and applicability. For sequential programs, a summary-based algorithm is used in [21]; summaries are like our well-nested sequences, except that well-nested sequences admit contexts from different stacks unlike summaries. As a result, our class of bounded hole behaviors generalizes summaries. Many other different theoretical results like phase bounded [18], order bounded [8] which gives interesting underapproximations of MPDA, are subsumed in tree-width bounded behaviors, but they do not seem to have practical implementations. Adding real-time information to pushdown automata by using clocks or timed stacks has been considered, both in the discrete and dense-timed settings. Recently, there has been a flurry of theoretical results in the topic [10,1,2,5,6]. However, to the best of our knowledge none of these algorithms have been successfully implemented (except [6] which implements a tree-automata based technique for single-stack timed systems) for multi-stack systems. One reason is that these algorithms do not employ scalable fix-point based techniques, but instead depend on region automaton-based search or tree automata-based search techniques.

## **2 Underapproximations in MPDA**

A multi-stack pushdown automaton (MPDA) is a tuple M = (S, Δ, s0, Sf , n, Σ, Γ) where, S is a finite non-empty set of locations, Δ is a finite set of transitions, s0 ∈ S is the initial location, Sf ⊆ S is a set of final locations, n ∈ N is the number of stacks, Σ is a finite input alphabet, and Γ is a finite stack alphabet which contains ⊥. A transition t ∈ Δ can be represented as a tuple (s, op, a, s- ), where, s, s- ∈ S are respectively, the source and destination locations of the transition t, a ∈ Σ is the label of the transition, and op is one of the following operations (1) nop, or no stack operation, (2) (↓i α) which pushes α ∈ Γ onto stack i ∈ {1, 2,...,n}, (3) (↑i α) which pops stack i if the top of stack i is α ∈ Γ.

For a transition t = (s, op, a, s- ) we write src(t) = s,tgt(t) = s and op(t) = op. At the moment we ignore the action label a but this will be useful later when we go beyond reachability to model checking. A configuration of the MPDA is a tuple (s, λ1, λ2,...,λn) such that, s ∈ S is the current location and λi ∈ Γ∗ represents the current content of i th stack. The semantics of the MPDA is defined as follows: a run is accepting if it starts from the initial state and reaches a final state with all stacks empty. The language accepted by a MPDA is defined as the set of words generated by the accepting runs of the MPDA. Since the reachability problem for MPDA is Turing complete, we consider underapproximate reachability.

A sequence of transitions is called **complete** if each push in that sequence has a matching pop and vice versa. A **well-nested** sequence denoted ws is defined inductively as follows: a possibly empty sequence of nop-transitions is ws, and so is the sequence t ws t where op(t)=(↓iα) and op(t - )=(↑iα) are a matching pair of push and pop operations of stack i, ∀i ∈ {1 ...n}. Finally the concatenation of two well-nested sequences is a well-nested sequence, i.e., they are closed under concatenation. The set of all well-nested sequences defined by an MPDA is denoted WS. If we visualize this by drawing edges between pushes and their corresponding pops, well-nested sequences have no crossing edges, as in and , where we have two stacks, depicted with red and violet edges. We emphasize that a well-nested sequence can have well-nested edges from any stack. In a sequence σ, a push (pop) is called a **pending** push (pop) if its matching pop (push) is not in the same sequence σ.

**Bounded Underapproximations**. As mentioned in the introduction, different bounded under-approximations have been considered in the literature to get around the Turing completeness of MPDA. During a computation, a context is a sequence of transitions where only one stack or no stack is used. In context bounded computations the number of contexts are bounded [25]. A round is a sequence of (possibly empty) contexts for stacks 1, 2,...,n. Round bounded computations restrict the total number of rounds allowed [19,5,6]. Scope bounded computations generalize bounded context computations. Here, the context changes within any push and its corresponding pop is bounded [19,20,28]. A phase is a contiguous sequence of transitions in a computation, where we restrict pop to only one stack, but there are no restrictions on the pushes [18]. A phase bounded computation is one where the number of phase changes is bounded.

**Tree-width**. A generic way of looking at them is to consider classes which have a bound on the tree-width [22]. In fact, the notions of split-width/cliquewidth/tree-width of communicating finite state machines/timed push down systems has been explored in [3], [13]. The behaviors of the underlying system are then represented as graphs. It has been shown in these references that if the family of graphs arising from the behaviours of the underlying system (say S) have a bounded tree-width, then the reachability problem is decidable for S via, treeautomata. However, this does not immediately give rise to an efficient implementation. The tree-automata approach usually gives non-deterministic or bottomup tree automata, which when implemented in practice (see [6]) tend to blow up in size and explore a large and useless space. Hence there is a need for efficient algorithms, which exist for more specific underapproximations such as contextbounded (leading to fix-point algorithms and their implementations [21]).

#### **2.1 A new class of under-approximations**

Our goal is to bridge the gap between having practically efficient algorithms and handling more expressive classes of under-approximations for reachability of multi-stack pushdown systems. To do so, we define a bounded approximation which is expressive enough to cover previously defined practically interesting classes (such as context bounded etc), while at the same time allowing efficient decidable reachability tests, as we will see in the next section.

**Definition 1.** (Holes). Let σ be complete sequence of transitions, of length n in a MPDA, and let ws be a well-nested sequence.

As an example, consider the sequence σ in Figure 1 of transitions of a MPDA having stacks 1,2 (denoted respectively red and blue). We use superscripts for

**Figure 1.** A run σ with 2 holes (2 red patches) of the red stack and 1 hole (one blue patch) of the blue stack.

each push, pop of each stack to distinguish the ith push, jth pop and so on of each stack. There are two holes of stack 1 (red stack) denoted by the red patches, and one hole of stack 2 (blue stack) denoted by the blue patch. The subsequence ↓1 1↓2 1 ws2 of the first hole is not a maximal factor, since it can be extended by ↓3 1 ws3 in the run σ, extending the hole. Consider the position in σ marked with ↓1 2. At this position, there is an open hole of the red stack (the first red patch), and there is an open hole of the blue stack (the blue patch). Likewise, at the position ↑5 1, there are 2 open holes of the red stack (2 red patches) and one open hole of the blue stack 2 (the blue patch). The hole bound of σ is 3. The green patch consisting of ↑3 1, ↑2 1 and ws5 is a pop-hole of stack 1. Likewise, the pops ↑2 2, ↑5 1, ↑1 2 are all pop-holes (of length 1) of stacks 2,1,2 respectively.

**Definition 2.** (Hole Bounded Reachability Problem) Given a MPDA and K ∈ N, the K-hole bounded reachability problem is the following: Does there exist a K-hole bounded accepting run of the MPDA?

**Proposition 1.** The tree-width of K-hole bounded MPDA behaviors is at most (2K + 3).

With this, from [22][5][6], decidability and complexity follow. Thus,

**Corollary 1.** The K-hole bounded reachability problem for MPDA is decidable in O(|M|2K+3) where, M is the size of the underlying MPDA.

Next, we turn to the expressiveness of this class with respect to the classical underapproximations of MPDA: first, the **hole** bounded class strictly subsumes **scope** bounded which already subsumes **context** bounded and **round** bounded classes. Also **hole** bounded MPDA and **phase** bounded MPDA are orthogonal.

**Proposition 2.** Consider a MPDA M. For any K, let LK denote a set of sequences accepted by M which have number of rounds or number of contexts or scope bounded by K. Then there exists K- ≤ K such that LK is K hole bounded. Moreover, there exist languages which are K hole bounded for some constant K, which are not K round or context or scope bounded for any K- . Finally, there exists a language which is accepted by phase bounded MPDA but not accepted by hole bounded MPDA and vice versa.

Proof. We first recall that if a language L is K-round, or K-context bounded, then it is also K- -scope bounded for some K- ≤ K [20,19]. Hence, we only show that scope bounded systems are subsumed by hole bounded systems.

Let L be a K-scope bounded language, and let M be a MPDA accepting L. Consider a run ρ of w ∈ L in M. Assume that at any point i in the run ρ, #i(holes) = k- , and towards a contradiction, let, k- > K. Consider the leftmost open hole in ρ which has a pending push ↓p whose pop ↑p is to the right of i. Since k- > K is the number of open holes at i, there are at least k- > K context changes in between ↓p and ↑p. This contradicts the K-scope bounded assumption, and hence k-≤ K.

To show the strict containment, consider the visibly pushdown language [7] given by Lbh = {anbn(ap1 cp1+1bp- 1 dp- 1+1 ··· apn cpn+1bp- n dp- n+1) | n, p1, p- 1,...,pn, p- n ∈ N}. A possible word w ∈ Lbh is a3b3 a2c3b2d3 a2c3bd2 ac2bd2 with a, b representing push in stack 1,2 respectively and c, d representing the corresponding matching pop from stack 1,2. A run ρ accepting the word w ∈ Lbh will start with a sequence of pushes of stack 1 followed by another sequence of pushes of stack 2. Note that, the number of the pushes n is same in both stacks. Then there is a group G consisting of a well-nested sequence of stack 1 (equal a and c) followed by a pop of the stack 1 (an extra c), another well-nested sequence of stack 2 (equal b and d) and a pop of the stack 2 (an extra d), repeated n times. From the definition of the hole, the total number of holes required in G is 0. But, we need 1 hole for the sequence of a's and another for the sequence of b's at the beginning of the run, which creates at most 2 holes during the run. Thus, the hole bound for any accepting run ρ is 2, and the language Lbh is 2-hole bounded.

However, Lbh is not k-scope bounded for any k. Indeed, for each m ≥ 1, consider the word wm = ambm(ac2bd2)m ∈ Lbh. It is easy to see that wm is 2mscope bounded (the matching c, d of each a, b happens 2m context switches later) but not k-scope bounded for k < 2m. It can be seen that Lbh is not k-phase bounded either. Finally, L- = {(ab)ncndn | n ∈ N} with a, b and c, d respectively being push and pop of stack 1,2 is not hole-bounded but 2-phase bounded.

## **3 A Fix-point Algorithm for Hole Bounded Reachability**

In the previous section, we showed that hole-bounded underapproximations are a decidable subclass for reachability, by showing that this class has a bounded tree-width. However, as explained in the introduction, this does not immediately give a fix-point based algorithm, which has been shown to be much more efficient for other more restricted sub-classes, e.g., context-bounded. In this section, we provide such a fix-point based algorithm for the hole-bounded class and explain its advantages. Later we discuss its versatility by showing extensions and evaluating its performance on a suite of benchmarks.

We describe the algorithm in two steps: first we give a simple fix-point based algorithm for the problem of 0-hole or well-nested reachability, i.e, reachability by a well-nested sequence without any holes. For the 0-hole case, our algorithm computes the reachability relation, also called the binary reachability problem [15]. That is, we accept all pairs of states (s, s- ) such that there is a well-nested run from s with empty stack to s with empty stack. Subsequently, we combine this binary reachability for well-nested sequences with an efficient graph search to obtain an algorithm for K-hole bounded reachability.

**Binary well-nested reachability for** MPDA. Note that single stack PDA are a special case, since all runs are indeed well-nested.

1. **Transitive Closure**: Let R be the set of tuples of the form (si, sj ) representing that state sj is reachable from state si via a nop discrete transition. Such a sequence from si to sj is trivially well-nested. We take the TransitiveClosure of R using Floyd-Warshall algorithm [12]. The resulting set Rc of tuples answers the binary reachability for finite state automata (no stacks).

```
1 Function IsEmpty(M = (S, Δ, s0, Sf , n, Σ, Γ), K):
      Result: True or False
2 WR := WellNestedReach(M); \\Solves binary reachability for pushdown system
3 if some (s0, s1) ∈ WR with s1 ∈ Sf then
4 return False;
5 forall i ∈ [n] do
6 AHSi := ∅; Seti := ∅;
7 forall (s, ↓i(α), a, s1) ∈ Δ and (s1, s-

                                      ) ∈ WR do
8 AHSi := AHSi ∪ {(i, s, α, s-

                                   )}; Seti := Seti ∪ {(s, s-

                                                      )};
9 HSi := {(i, s, s-

                     ) | (s, s-

                            ) ∈ TransitiveClosure(Seti)};
10 μ := [s0]; μ.NumberOfHoles := 0;
11 SetOfListsnew := {μ}; SetOfLists := ∅;
12 do
13 SetOfLists := SetOfLists ∪ SetOfListsnew;
14 SetOfListstodo := SetOfListsnew; SetOfListsnew := ∅;
15 forall μ-
                 ∈ SetOfListstodo do
16 if μ-

                .NumberOfHoles < K then
17 forall i ∈ [n] do
                   \\ Add hole for stack i
18 SetOfListsh := AddHolei(μ-

                                        ,HSi) \ SetOfLists;
19 SetOfListsnew := SetOfListsnew ∪ SetOfListsh;
20 if μ-

                .NumberOfHoles > 0 then
21 forall i ∈ [n] do
                   \\ Add pop for stack i
22 SetOfListsp := AddPopi(μ-

                                       , M, AHSi,HSi, WR) \ SetOfLists;
23 SetOfListsnew := SetOfListsnew ∪ SetOfListsp;
24 forall μ3 ∈ SetOfListsp do
25 if μ3.last ∈ Sf and μ3.NumberOfHoles = 0 then
26 return False; \\If reached destination state
27 while SetOfListsnew 	= ∅;
28 return T rue;
```
**Algorithm 1:** Algorithm for Emptiness Checking of hole bounded MPDA

2. **Push-Pop Closure**: For stack operations, consider a push transition on some stack (say stack i) of symbol γ, enabled from a state s1, reaching state s2. If there is a matching pop transition from a state s3 to s4, which pops the same stack symbol γ from the stack i and if we have (s2, s3) ∈ Rc, then we can add the tuple (s1, s4) to Rc. The function WellNestedReach repeats this process and the transitive closure described above until a fix-point is reached. Let us denote the resulting set of tuples by WR. Thus,

**Lemma 1.** (s1, s2) ∈ WR iff ∃ a well-nested run in the MPDA from s1 to s2.

**Beyond well-nested reachability**. A naive algorithm for K-hole bounded reachability for K > 0 is to start from the initial state s0, and do a Breadth First Search (BFS), nondeterministically choosing between extending with a well-nested segment, creating hole segments (with a pending push) and closing hole segments (using pops). We accept when there are no open hole segments and reach a final state; this gives an exponential time algorithm. Given the exponential dependence on the hole-bound K (Corollary 1), this exponential blowup is unavoidable in the worst case, but we can do much better in practice. In particular, the naive algorithm makes arbitrary non-deterministic choices resulting in a blind exploration of the BFS tree.