
## 32 **Martin Gebser And Joohyung Lee And Yuliya Lierler**

that Y is a loop of ΠX,Y . Since Y is unfounded by Π w.r.t. X**, by Proposition 13,**
we also have that RωΠ,X(Y ) = Y . This shows that Y **is contained in some maximal**
subset Z of X such that Z is a loop of ΠX,Z and RωΠ,X(Z) = Z.

As it is easy to check that X **is supported by Π, Proposition 19 tells us that the**
investigation of bounding loops constitutes the hard part of stability checking. But this is not due to the hardness of identifying them. In fact, the following method can be used to compute all bounding loops Z of Π w.r.t. X **in polynomial time:**
1. Let Y = X.

2. Let Z = RωΠ,X(Y ). (Note that Z = RωΠ,X(Z).)
3. If Z is a loop of ΠX,Z, then mark Z **as a bounding loop of Π w.r.t.** X.

Otherwise, proceed with Step 2 for every maximal loop Y of ΠX,Z **that is**
contained in Z.

The soundness of this approach is straightforward, given that operator R is monotone, i.e., RωΠ,X(Z) ⊆ RωΠ,X(Y ) if Z ⊆ Y **(used in Step 2), and likewise that**
ΠX,Y ⊆ ΠX,Z if Y ⊆ Z **(used in Step 3).**
For illustration, consider the following program Π4:

$$s\leftarrow p$$
$$\begin{array}{l}{{p\;;\;q\gets u}}\\ {{s\;;\;t\gets q}}\\ {{r\;;\;u\gets t}}\end{array}$$
$$s\gets{\stackrel{\mathbf{1}}{t}}$$ $$t\gets s,u$$
$$\stackrel{\mathrm{-}}{q}\leftarrow\mathrm{\boldmath~r~}$$ $$\mathrm{\boldmath~r~}\leftarrow\mathrm{\boldmath~p,q~}$$
$$u\ ;\ v\leftarrow\ .$$
p ← r s ← p p ; q ← u
q ← r s ← t s ; t ← q
r ← p, q t ← s, u r ; u ← t u ; v ← .
For X = {p, q, r, s, t, u}, it holds that (Π4)X,X = Π4 and also that X **is a loop**
of Π4. However, Y = RωΠ4,X(X) = {p, q, r, s, t} 6= X, so that X **is not a bounding**
loop of Π4 w.r.t. X. On the other hand, Y is not a loop of (Π4)X,Y **, which does**
not include the last two rules where u occurs in the head. Rather, Z = {p, q, r} and Z
′ = {s, t} are the maximal loops of (Π4)X,Y that are contained in Y **. In view of**
the rules in the second column, RωΠ4,X(Z
′) = ∅**, which shows that no subset of** Z
′
is a bounding loop of Π4 w.r.t. X. For Z = {p, q, r}, we obtain RωΠ4,X(Z) = Z**, and**
Z is also a loop of (Π4)X,Z (due to the rules in the first column). That is, Z **is the**
single bounding loop of Π4 **w.r.t.** X.

Let us compare this outcome with the ones of previous methods for **modularizing**
stability checking. Since the approach described in (Leone et al. 1997) considers maximal loops of the original program and X = {p, q, r, s, t, u} **is a (maximal) loop**
of Π4, it cannot be used to decompose X**, and the only applicable simplification is**
to remove u by means of R, that is, Y = RωΠ4,X(X) = {p, q, r, s, t}**. The approach in**
(Koch et al. 2003) considers the maximal loops of ΠX,RωΠ,X (X), which, for (Π4)X,Y ,
gives Z = {p, q, r} and Z
′ = {s, t}**. As described in (Koch et al. 2003), since the**
subprograms (Π4)X,Z and (Π4)X,Z′ **are not HCF, they are not simplified any further and used to separately check for a nonempty unfounded subset of** Z or Z
′,
respectively. Unlike this, the notion of a bounding loop allowed us to eliminate all subsets of Z
′ **as potential nonempty unfounded sets.**
Turning back to HEF programs, from Proposition 16, we derive the following proposition for a subprogram ΠX,Y associated with a bounding loop Y **of Π w.r.t.** X.

Proposition 20