1 Introduction
x
\(:= 1\)while x
\(\ne 0\)x
\(:= 2\)x
\(\mid \mid \) x
\(:=\) x
\(-3\) (where \(\mid \mid \) represents nondeterministic branching)-
We first consider targets consisting of a single vector (or ‘point targets’), and present the classes of invariants and systems for which invariants can and cannot be automatically computed for the reachability question. A summary of the results for linear and semi-linear invariants for these targets is given in Table 1. For completeness we also consider \(\mathbb {R},\mathbb {R}_{+}\)-(semi)-linear sets, where we enhance the picture from prior work by showing that strongest \(\mathbb {R}\)-semi-linear invariants are computable.
-
We establish the existence of strongest \(\mathbb {Z}\)-linear invariants, and show that they can be found algorithmically in polynomial time (Theorem 10).
-
If a \(\mathbb {Z}\)-linear invariant is not separating, we may instead look for an \(\mathbb {N}{}\)-semi-linear invariant (a class that generalises both \(\mathbb {Z}\)-semi-linear and \(\mathbb {N}{}\)-linear invariants), and we show that such an invariant can always be found for any unreachable point target when dealing with deterministic integer linear dynamical systems (Theorem 19).
-
However, for nondeterministic integer linear dynamical systems, computing separating \(\mathbb {N}{}\)-semi-linear invariants is an undecidable problem in arbitrary dimension (Theorem 21). Nevertheless we show how such invariants can be computed in a low-dimensional setting, in particular for affine updates in one dimension (Theorem 22). As an immediate consequence, this establishes that the multipath loop associated with the MU Puzzle belongs to a class of programs for which we can automatically synthesise \(\mathbb {N}{}\)-semi-linear invariants.
-
-
We consider the reachability problem for porous targets. That is, where the target is a linear or semi-linear set.
-
For full-dimensional5\(\mathbb {Z}\)-linear targets we show that reachability is decidable, and, in the case of unreachability that a \(\mathbb {Z}\)-semi-linear invariant can always be exhibited as a certificate (Theorem 37). If the target is not full-dimensional then the reachability problem is Skolem-hard and undecidable for deterministic and nondeterministic systems respectively.
-
Secondly, we also show that the reachability problem for low-dimensional semi-linear sets is decidable for deterministic LDS (Theorem 40). Note that the Skolem problem is decidable at low orders, so it does not present a barrier in this setting.
-
-
In Sect. 7 we present our tool porous which handles one-dimensional affine systems for both point and \(\mathbb {Z}\)-linear targets, solving both the reachability problem and producing invariants. Inter alia, this allows one to handle the multipath loop derived from the MU Puzzle in fully automated manner.
Dom | D/N | Linear | Semi-linear (SL) |
---|---|---|---|
\(\mathbb {Z}\) | Det | Strongest computable (Theorem 10) | No strongest (Section 4.2) |
Subsumed by \(\mathbb {N}\)-SL | |||
\(\mathbb {Z}\) | Non | Strongest computable (Theorem 10) | No strongest (Section 4.2) |
\(\mathbb {N}\) | Det | No strongest (Section 4.2) | No strongest (Section 4.2) |
Subsumed by \(\mathbb {N}\)-SL | But sufficient computable (Theorem 19) | ||
\(\mathbb {N}\) | Non | No strongest (Section 4.2) | 1d-affine decidable (Theorem 22) |
Undec. in general (Theorem 21) | |||
\(\mathbb {R}\) | Det | Strongest: affine relations by Karr [4] | Strongest: affine closure on |
Zariski closure (Theorem 8) | |||
\(\mathbb {R}\) | Non | Strongest: affine relations by Karr [4] | Strongest: affine closure on |
Zariski closure (Theorem 8) | |||
\(\mathbb {R}_+\) | Det | No strongest (Section 4.2) | No strongest, but sufficient |
Subsumed by \(\mathbb {R}_{+}\)-SL | Computable [5] | ||
\(\mathbb {R}_+\) | Non | No strongest (Section 4.2) | Undecidable [5] |
1.1 Related work
2 Preliminaries
-
\(x^{(0)}\in I\), and
-
\(\{M_i x \mid x \in I\}\subseteq I\) for all \(i \in \left\{ 1,\dots ,k\right\} \).
3 \(\mathbb {R}\) invariants: \(\mathbb {R}\)-linear and \(\mathbb {R}\)-semi-linear
3.1 \(\mathbb {R}\)-linear invariants
3.2 \(\mathbb {R}\)-semi-linear invariants
4 Strongest \(\mathbb {Z}\)-linear invariants
4.1 Computing the strongest \(\mathbb {Z}\)-linear invariants
-
First compute a subset \(L_0\subseteq I\) of the invariant that has the same dimension as I.Recall the set \(R_0 = \left\{ x^{(0)}, r_1,\dots ,r_{d'}\right\} \subseteq \mathcal {O}{}\), with \(d' \le d\), from Lemma 6. The resulting \(\mathbb {Z}\)-linear set \(L_0 = \left( x^{(0)} + (r_1 - x^{(0)})\mathbb {Z}+ \dots + (r_{d'} - x^{(0)})\mathbb {Z}\right) \) is then a \(d'\)-dimensional porous subset of the \(d'\)-dimensional affine hull of the orbit (\(L_0 \subseteq \textrm{Aff}(\mathcal {O}{})\)). Applying \(M_1,\dots , M_k\) can only increase the density, but not the dimension. As each \(r_i\) and \(x^{(0)}\) are in \(\mathcal {O}{}\), by Proposition 11 we can assume that each of the directions \((r_i - x^{(0)})\) must be represented in any \(\mathbb {Z}\)-linear set containing \(\mathcal {O}{}\), and we therefore have that \(L_0 \subseteq I\).
-
In the second phase, we ‘fill in’ the lattice as required to cover the whole of \(\mathcal {O}\). We compute a growing sequence \(L_0\subsetneq L_1\subsetneq \dots \subsetneq L_{m-1} = L_{m}= I\), where at each step the algorithm merely increases the density of the attendant sets in order to ‘fill in’ missing points of the invariant.To do this we repeatedly find new points which are not yet covered by \(L_i\). Supposing we find \(x'\in \mathcal {O}\setminus I\), we then use Proposition 11 to argue that we can add the vector \(x' - x^{(0)}\).
4.2 Extensions of \(\mathbb {Z}\)-linear sets without strongest invariants
5 \(\mathbb {N}\)-semi-linear invariants
5.1 Existence of sufficient (but non-minimal) \(\mathbb {N}\)-semi-linear invariants for point reachability in deterministic LDS
5.2 Undecidability of \(\mathbb {N}\)-semi-linear invariants for nondeterministic LDS
-
For \(i \le m\), the type 1 transformation \(\textsf{Simulate}_{i}\) on (s, c, d, n, k) encodes the action of reading the pair \((u^i,v^i)\) and increases the counters n and k: it simultaneously applies \(s \leftarrow \textsf {max}_i s + c[u^i]\frac{\textsf {max}_i}{n_i}-d[v^i]\frac{\textsf {max}_i}{m_i}\), \(c \leftarrow \frac{\textsf {max}_i}{n_i}c\), \(d \leftarrow \frac{\textsf {max}_i}{m_i}d\), \(n\leftarrow n+k\) and \(k\leftarrow k+1\).
-
The type 2 transformation \(\textsf{Transfer}\) on (s, c, d, n, k) gathers some of the values in order to compare them and resets d: \(s\leftarrow s - c - d\), \(c \leftarrow -s -c-d\) and \(d\leftarrow 0\).
-
The type 3 transformation \(\mathsf {Inc_s}\) increments s: \(s\leftarrow s+1\).
-
The type 3 transformation \(\mathsf {Inc_c}\) increments c: \(c\leftarrow c+1\).
-
The type 3 transformation \(\textsf{Dec}\) decreases k and n: \(n\leftarrow n-k\), \(k\leftarrow k-1\).
-
The type 3 transformation \(\mathsf {Dec_k}\) decrements k: \(k\leftarrow k-1\).
-
\(s = c[ u^{w} ]-d[ v^{w} ]\),
-
\(n=\frac{j(j-1)}{2} \) and \(k=j\),
-
\(p=a=1\).
-
\(\diamond \) Let \(z=\textsf{Simulate}_w(x)\in \mathcal {I}_1\), for some \(w\in \{1,\dots ,m\}^*\) with \(\left|w\right| \le n_0 +1\). By ordering if we apply a transformation outside \(\textsf{Transfer}\) or a \(\textsf{Simulate}_{i}\) for some i, we reach \(\mathcal {I}_3\).
-
\(\bullet \) For \(i\in \{1,\dots ,m\}\), if \(\left|w\right| \le n_0\), then \(\textsf{Simulate}_{i}z\in \mathcal {I}_1\).Else, \(\textsf{Simulate}_{i}z = \textsf{Simulate}_{wi}x=(s,c,d,n,k,p,1)\) with \(\left|w\right|=n_0+1\). But then, there exists \(n_1\leqslant n_0\) such that \(u^{wi}_{n_1}\ne v^{wi}_{n_1}\). Let \(n_2\) be the smallest such number, then assume without loss of generality that \(c\ge d\), we havesince \(u^{wi}_j=v^{wi}_j\) for \(j<n_2\). Thus,$$\begin{aligned} s&= c[ u^{wi} ]-d[ v^{wi} ]\\&= (u^{wi}_{n_2}-v^{wi}_{n_2})c4^{\vert u^{wi}\vert -n_2}+ \sum _{j=n_2+1}^{\max (\vert u^{wi}\vert ,\vert v^{wi}\vert )}(u^{wi}_j-v^{wi}_j)c4^{\vert u^wi\vert -j} \end{aligned}$$As \(c\ge d\), this shows that \(\textsf{Simulate}_{i} z\in \mathcal {I}_3\).$$\begin{aligned} \vert s\vert&\geqslant c4^{\vert u^{wi}\vert -n_2}-\frac{2c}{3} 4^{\vert u^{wi}\vert -n_2}{} & {} \text {since }\vert u^{wi}_{n_2}-v^{wi}_{n_2}\vert =1\\{} & {} {}&\text {and for } n\ge n_2, \vert u^{wi}_{n}-v^{wi}_{n}\vert \le 2\\&\geqslant \frac{1}{3} c4^{\vert u^{wi}\vert -n_2}\\&\geqslant 2c + 1{} & {} \text {since }n_2\leqslant n_0\text { and }\vert u^{wi}\vert \geqslant n_0+2. \end{aligned}$$
-
\(\bullet \) \(\textsf{Transfer}z\in \mathcal {I}_2\).
-
-
\(\diamond \) Let \(z\in \mathcal {I}_2\) and f be one of the transformations, then \(f(z) \in \mathcal {I}_2\) if f increased (resp. decreased) a negative (resp. positive) component. Otherwise \(f(z) \in \mathcal {I}_3\).
-
\(\diamond \) Let \(z=(s,c,d,n,k,p,1)\in \mathcal {I}_3\), f be one of the transformations and \(f(z) = (s',c',d',n',k',p',1)\).
-
\(\bullet \) if \(p=0\), then either \(p'\le -1\) and \(f(z)\in \mathcal {I}_3\) or z satisfies \((s\ge 1\vee c\ge 1\vee n\le -1 \vee k\le -1)\) and then f(z) satisfies \((s'\ge 1\vee c'\ge 1\vee n'\le -1 \vee k'\le -1)\), thus \(f(z)\in \mathcal {I}_3\).
-
\(\bullet \) if \(p =1\), then \(\vert s\vert -c-d \ge 1, c\ge 0 \) and \(d\ge 0\). There are three possibilities (1) \(p'=2\) and thus \(f(z) \in \mathcal {I}_3\), (2) \(f=\textsf{Transfer}\) then \(p'=0\) and either \(s' \ge 1\) or \(c' \ge 1\) and thus \(f(z)\in \mathcal {I}_3\) or (3) \(f=\textsf{Simulate}_{i}\) for \(i\le m\). In the latter case without loss of generality, assume that \(d'\geqslant c'\). We have thatsince \(\textsf {max}_i c\ge c'\), \(\textsf {max}_i d/3 \ge d'\) (as \(m_i\ge 4\)) and \(\textsf {max}_i\geqslant 4\). This shows that \(f(z)\in \mathcal {I}_3\).$$\begin{aligned} \left|s'\right|&=\vert \textsf {max}_i s+c'[ u^{i} ]-d'[ v^{i} ]\vert{} & {} \text {by applying }\textsf{Simulate}_{i}\\&\geqslant \textsf {max}_i\vert s\vert - d'\max ([ u^{i} ],[ v^{i} ])\\&\geqslant \textsf {max}_i(c+d+1)-d'\max ([ u^{i} ],[ v^{i} ]){} & {} \text {by assumption on }\vert s\vert \\&\geqslant \textsf {max}_i(c+d+1)-\tfrac{2}{3}d\textsf {max}_i{} & {} \text {since }[ u^i ]\in [0,\tfrac{2n_i}{3}]\\&= \textsf {max}_i(c+ d/3) + \textsf {max}_i \\&\geqslant c'+d' + 1{} & {} \end{aligned}$$
-
5.3 Nondeterministic one-dimensional affine updates
-
f is redundant if \(f(x)= b\), (including possibly \(b = 0\)), or if \(f(x) = x\).
-
f is a counter if \(f(x) = x + b\), \(b\ne 0\). Two counters \(f(x) = x + b\) and \(g(x) = x + c\) are opposing if \(bc<0\). Otherwise they are called codirectional.
-
f is growing if \(f(x) = ax + b\) and \(\left|a\right| \ge 2\). We say a growing function is inverting if \(a \le -2\).
-
f is pure inverting if \(f(x) = -x + b\) (including possibly \(b = 0\)).
5.3.1 Simplifying assumptions
5.3.2 Two opposing counters
5.3.3 Only pure inverters
5.3.4 No counters
5.3.5 Codirectional counters
-
If \(h_j\) is a counter, \(\Delta _j\) is constant, regardless of \(x_r\).
-
If \(h_j\) is a growing function outside of \([-B,C]\), then \(\Delta _j(x'_r) \ge \Delta _j(x_r)\) if \(x_r'< x_r <-B\).
-
\( h_j\circ \dots \circ h_1(x_r) < x_r \le -B \) for all \(j\in \{1,\dots ,n\}\) if \(d >0\), or
-
\( h_j\circ \dots \circ h_1(x_r)>x_r \ge C\) for all \(j\in \{1,\dots ,n\}\) if \(d< 0\).
-
\(i\rightarrow j\) if \(f(i) \equiv j\mod d\) for some non-inverting growing function f.
-
\(i\rightarrow j'\) if \(i + a_1 b_1 + \dots + a_{\kappa '} b_{\kappa '} \equiv j \mod d\), for some \(a_i\in \{0,\dots ,d-1\}\), where the counting functions are \(g_i(x) = x+ b_i\) for \(1\le i \le \kappa '\).
-
\(i\rightarrow i'\) for all \(i\in \{0,\dots ,d-1\}\).
5.3.6 Reachability
5.3.7 Complexity
-
Firstly we saturate using Lemma 29, Lemma 31, and Lemma 32; here counters take the form \(x+d\mathbb {Z}\) or \(x+d\mathbb {N}\), where \(d\le \mu \) and \(x\in [-B,C]\) for \(B\le 2\mu ,C\le 3\mu \). Observe that there are at most \(5\mu \) sets of the form \((x+d\mathbb {N})\) and \(\mu \) sets of the form \((x+d\mathbb {Z})\). Thus there are at most \(6\mu \) sets that can be considered in this process. Hence, using breadth-first search, this phase takes time \(O(\mu \cdot k)\).
-
Thirdly, the final saturation of \(\mathbb {N}\)-linear sets can be done in time \(O(\mu ^2\cdot k^2)\). Specifically, we proceed in rounds: in each round we consider each set of the form \((x+d\mathbb {N})\), and add the sets \((f(x)+d\mathbb {N})\) whenever this is more general than a set already in I. In each round, up to \(d\cdot k\) new \(\mathbb {N}\)-linear sets are considered; however, at the end of the round, there are only d most general sets to expand into the next round. In Lemma 34 we note that the length of any cycle-free path outside of \([-B,C]\) is bounded by at most \(d(k+1)\), thus at most \(d(k+1)\) rounds of exploration are required.
6 Porous targets
6.1 \(\mathbb {Z}\)-linear targets
6.2 Deterministic LDS and low dimension \(\mathbb {N}\)-semi-linear targets
7 The POROUS tool
7.1 Experimentation
Size | Invariant Build Time | Unreachable Instances | Invariant proof time | Reachable instances | Reachable with proofs | Reachability proof time | ||
---|---|---|---|---|---|---|---|---|
avg | max | avg | max | within \({\approx }60\)s | avg | |||
8 | 0.001 | 0.009 | 156 (10.2%) | 0.004 | 0.143 | 1368 (89.8%) | 1362 (99.6%) | 0.001 |
16 | 0.001 | 0.009 | 195 (12.8%) | 0.006 | 0.121 | 1329 (87.2%) | 1313 (98.8%) | 0.129 |
32 | 0.001 | 0.021 | 201 (13.2%) | 0.010 | 0.267 | 1323 (86.8%) | 1261 (95.3%) | 0.130 |
64 | 0.002 | 0.038 | 250 (16.4%) | 0.019 | 0.980 | 1274 (83.6%) | 1137 (89.2%) | 0.355 |
128 | 0.006 | 0.485 | 234 (15.4%) | 0.041 | 1.567 | 1290 (84.6%) | 1087 (84.3%) | 0.464 |
256 | 0.025 | 13.445 | 243 (15.9%) | 0.102 | 2.874 | 1281 (84.1%) | 989 (77.2%) | 0.895 |
512 | 0.073 | 2.708 | 232 (15.2%) | 0.299 | 6.951 | 1292 (84.8%) | 875 (67.7%) | 1.272 |
1024 | 0.562 | 224.729 | 232 (15.2%) | 0.916 | 23.836 | 1292 (84.8%) | 789 (61.1%) | 1.452 |
2048 | 2.846 | 2151.266 | 248 (16.3%) | 2.934 | 109.219 | 1276 (83.7%) | 666 (52.2%) | 2.127 |
All | 0.390 | 2151.266 | 1991 (14.5%) | 0.481 | 109.219 | 11725 (85.5%) | 9479 (80.8%) | 0.612 |