Regular Model Checking for Systems with Effectively Regular Reachability Relation

In our undecidability proofs we make use of the fact that RTSs can simulate Turing machines. More precisely, a configuration $(w_l,q,w_r)$ of a TM $M$ can be encoded as a word $w_{l}q{w}_r$. The transition function $\delta$ of $M$ can then be simulated by $\mathrm{\Delta }$ as only the letters at positions next to the head can change. If the RTS is length-preserving, one can set $ℐ:=\{q_{0}w\}{\{\mathrm{\square }\}}^{\ast }$ where $w$ is the input to $M$ and terminate if the head of $M$ gets to the last position of the configuration of the RTS; in this case, $M$ accepts $w$ iff there exists a run of the RTS (starting in a configuration of a high enough length) which reaches a configuration containing $q_f$.

If there exists an initial configuration $c_0\in ℐ$ from which reaching $L$ has probability less than 1, then there exists a bSCC reachable from $c_0$ such that neither the bSCC nor the path from $c_0$ to the bSCC intersects $L$. In other words, there exists a path $(c_0,\mathrm{\dots },c_n)$ such that $c_0\in ℐ$, $c_i\notin L$ for all $i$, and $c_n$ is in a bSCC which does not intersect $L$, i.e. $\text{Reach}(c_n)\subseteq {\text{Reach}}^{-1}(c_n)$ and $\text{Reach}(c_n)\cap L=\mathrm{\varnothing }$. Given such a path, these conditions can be checked, proving semi-decidability of the complement and thus proving that almost sure reachability is in ${\mathrm{\Pi }}_1^0$.

For hardness, we reduce from the non-emptiness problem for Turing machines. Given a TM $M$, we define $ℐ$ to be the set of input configurations of $M$ with any number of blank symbols, that is, the set of all words $wv$ where $w$ is the encoding of an input configuration of $M$, and $v\in {\{\mathrm{\square }\}}^{\ast }$ is a word of blanks. Further, we let $\mathrm{\Delta }$ simulate the transitions of $M$. Moreover, for every length, we add two special configurations $s,t$ to the RTS and add the following transitions to $\mathrm{\Delta }$: $(c,s)$ and $(s,c)$ for every configuration $c$ of $M$, $(a,t)$ for every accepting configuration $a$ of $M$, and $(s,t)$. Then $\text{Reach}=\left((C\cup \{s\})\times (C\cup \{s,t\})\right)\cup \{(t,t)\}$ where $C$ is the set of configurations of $M$, so Reach is regular. Let $L=\{s\}$ (of all lengths). If $M$ has an input $w$ which it accepts, then there exists a run of $𝒮$ starting from $q_{0}w$ (with enough blank symbols) which reaches an accepting configuration of $M$ and then goes to $t$, never visiting $s$. This run has positive probability as the number of steps until $t$ is reached is finite, and thus the probability of visiting $L$ is not 1. Conversely, if $M$ does not have an input which it accepts, then no run can reach $t$ without visiting $s$ first, and a transition to $s$ will occur eventually almost surely, i.e. the probability of visiting $L$ is 1. $◀$

For almost sure recurrent reachability, we introduce the following characterisation, which will also be useful in later sections.

Every run of $𝒮$ eventually visits a bSCC almost surely, and thus every infinite run visits $L$ infinitely often iff every reachable bSCC is non-trivial and contains a configuration in $L$. This is the case iff no terminating configuration is reachable and $L$ can be reached from every reachable configuration, or formally, $\text{Reach}(ℐ)\subseteq \overline{T}\cap {\text{Reach}}^{-1}(L)$. $◀$

By Lemma 4.2, it suffices to show that deciding whether $\text{Reach}(ℐ)\subseteq \overline{T}\cap {\text{Reach}}^{-1}(L)$ is $\mathrm{𝖯𝖲𝖯𝖠𝖢𝖤}$-complete. One can decide this in nondeterministic polynomial space by e.g. guessing a configuration $c$ letter by letter and checking on the fly that $c\in \text{Reach}(ℐ)$, $c\in \overline{T}$, and $c\notin {\text{Reach}}^{-1}(L)$. For that, one can run $c$ on the corresponding NFAs by memorizing the current set of states after each letter of $c$, and checking whether that set contains a final state of the NFA at the end. Since all involved NFAs have polynomial size (note that $\overline{T}={\mathrm{\Delta }}^{-1}(𝒞)$), this algorithm takes polynomial space, and membership in $\mathrm{𝖯𝖲𝖯𝖠𝖢𝖤}$ follows from $\mathrm{𝖭𝖯𝖲𝖯𝖠𝖢𝖤}=\mathrm{𝖯𝖲𝖯𝖠𝖢𝖤}$.

For hardness, we can reduce from the NFA subset problem, i.e., whether $𝖫(A)\subseteq 𝖫(B)$ for given NFAs $A,B$: By setting $ℐ:=𝖫(A)$, $\mathrm{\Delta }:=\{(c,c)\mid c\in 𝒞\}$, and $L:=𝖫(B)$, almost sure recurrent reachability holds iff $𝖫(A)\subseteq 𝖫(B)$. $◀$

We now consider almost sure termination, the property for which the proof is most involved. Again, we first prove a characterisation. We say that $𝒮$ terminates almost surely if for every initial configuration $c$, the set of runs starting at $c$ that end in a terminating configuration has probability 1.

$\text{Reach}(ℐ)\setminus {\text{Reach}}^{-1}(T)$ is the set of all reachable configurations $c$ such that no terminating configuration can be reached from $c$. If such a $c$ exists, then reaching it has a positive probability, and since the run cannot terminate from $c$, $𝒮$ terminates with probability less than 1. For the converse, if terminating configurations can be reached from any reachable configuration, then no reachable non-trivial bSCCs exist, i.e. every reachable bSCC is a terminating configuration. Since a run of $𝒮$ eventually reaches a bSCC almost surely, it follows that $𝒮$ terminates almost surely. $◀$

From the characterisation of Lemma 4.4, it is easy to show that the problem is $\mathrm{𝖯𝖲𝖯𝖠𝖢𝖤}$-complete in the case where an NFA for $T$ is given in the input, one can e.g. reduce from and to the NFA subset problem. For membership in $\mathrm{𝖤𝖷𝖯𝖲𝖯𝖠𝖢𝖤}$, observe that $T=\overline{{\mathrm{\Delta }}^{-1}(𝒞)}$ has an NFA of exponential size in the input. One can thus build a polynomial NFA for $\text{Reach}(ℐ)$ and an exponential NFA for ${\text{Reach}}^{-1}(T)$, guess a configuration $c$ letter by letter and check that $c\in \text{Reach}(ℐ)$ and $c\notin {\text{Reach}}^{-1}(T)$. This is a nondeterministic algorithm using exponential space, and membership follows from $\mathrm{𝖭𝖤𝖷𝖯𝖲𝖯𝖠𝖢𝖤}=\mathrm{𝖤𝖷𝖯𝖲𝖯𝖠𝖢𝖤}$.

For $\mathrm{𝖤𝖷𝖯𝖲𝖯𝖠𝖢𝖤}$-hardness, we reduce from the problem whether an exponentially space-bounded Turing machine $M=(Q,{\mathrm{\Sigma }}^{\prime },\mathrm{\Gamma },\delta ,\mathrm{\square },q_0,q_f)$ accepts the empty input. The configurations of our RTS $𝒮$ are going to be encodings of runs of $M$, and a run of $𝒮$ cannot terminate if and only if it starts with the encoding of the accepting run of $M$ on the empty input. We encode a run of $M$ as a word consisting of encodings of configurations of $M$ separated by $\mathrm{\#}$.

Let $n:=|M|$ and let $p_1$, …, $p_n$ be the first $n$ prime numbers. Then ${\sum }_{i=1}^n{p}_i$ is polynomial in $n$ by the prime number theorem while $m:={\prod }_{i=1}^n{p}_i$ is exponential in $n$; we can thus assume that the run of $M$ on the empty input uses only the first $m$ tape cells. An NFA recognizing the language of words not divisible by $p_i$ only needs $p_i$ states. Thus, by putting $n$ NFAs side by side, each of which only accepts words of length not divisible by $p_i$, one can construct an NFA of polynomial size in $n$ which only accepts words of length not divisible by $m$. This fact will be used in our reduction.

Let ${\mathrm{\Sigma }}_1:=Q\cup \mathrm{\Gamma }\cup \{\mathrm{\#}\}$ and ${\mathrm{\Sigma }}_2:=\{x^{\prime }\mid x\in {\mathrm{\Sigma }}_1\}$. We call symbols in ${\mathrm{\Sigma }}_1$ unmarked and symbols in ${\mathrm{\Sigma }}_2$ marked. We denote the symbol in position $i$ of a configuration of $𝒮$ by $x_i$. Let $\mathrm{\Sigma }:={\mathrm{\Sigma }}_1\cup {\mathrm{\Sigma }}_2$, $𝒞:={\mathrm{\Sigma }}^{\ast }$ and $ℐ:=\{\mathrm{\#}{q}_0\}{\{\mathrm{\square }\}}^{\ast }\{\mathrm{\#}\}{\mathrm{\Sigma }}_1^{\ast }\{q_f\}$, i.e. the first configuration of $M$ in an initial configuration of $𝒮$ is the empty input to $M$, and the last symbol is the accepting state of $M$. $\mathrm{\Delta }$ has three types of transitions: ${\mathrm{\Delta }}_{\mathrm{𝑚𝑎𝑟𝑘}}$, which marks some symbols, and ${\mathrm{\Delta }}_{\mathrm{𝑢𝑛𝑚𝑎𝑟𝑘}}$, which unmarks all symbols, and ${\mathrm{\Delta }}_{\mathrm{𝑒𝑛𝑑}}$, which is used to terminate certain runs. Specifically, ${\mathrm{\Delta }}_{\mathrm{𝑚𝑎𝑟𝑘}}$ nondeterministically chooses a position $i$ and a distance $k>2$ and marks the symbols at positions $i-1$, $i$, $i+1$, $i+2$, and $i+k$. For this transition to be executed, three conditions are required:

• $\mathrm{■}$

  No symbol is marked.

• $\mathrm{■}$

  There is exactly one $\mathrm{\#}$ in the subword $x_{i+1}\mathrm{\cdots }{x}_{i+k}$.

• $\mathrm{■}$

  If $x_{i-1}{x}_i{x}_{i+1}{x}_{i+2}$ is part of a configuration of $M$, then $x_k$ is not the symbol appearing in place of $x_i$ in the next configuration of $M$. In particular, if $x_i=\mathrm{\#}$, then $x_k\ne \mathrm{\#}$.

The last point can be intuitively described as the encoding of the run having a “mistake” at position $x_k$. This description only fits if ${\mathrm{\Delta }}_{\mathrm{𝑚𝑎𝑟𝑘}}$ chooses the correct distance; for other distances, even the correct run has a mistake. It will be relevant, however, that the encoding of the correct run does not have a mistake if distance $m$ is chosen.

${\mathrm{\Delta }}_{\mathrm{𝑢𝑛𝑚𝑎𝑟𝑘}}$ takes as input a configuration with exactly five marked symbols, checks that the distance between the second and the fifth is not a multiple of $m$, and unmarks all symbols. If the distance is a multiple of $m$, the transition cannot occur. As explained above, this can be done with a transducer of polynomial size in $n$.

${\mathrm{\Delta }}_{\mathrm{𝑒𝑛𝑑}}$ takes as input a configuration where the distance between any two $\mathrm{\#}$s is not a multiple of $m$, and replaces all symbols by ${\mathrm{\#}}^{\prime }$, after which the run terminates.

Observe that transitions only mark and unmark symbols and never change them. Thus every reachable configuration can be reached in at most two steps, and $\text{Reach}=\{(c,c)\mid c\in 𝒞\}\cup \mathrm{\Delta }\cup {\mathrm{\Delta }}^2$ is regular and has a transducer of polynomial size in $n$. Furthermore, a run of $𝒮$ can only terminate if either the initial configuration has $\mathrm{\#}$s at a distance not divisible by $m$, or the run reaches a configuration where the distance between the marked symbols $x_i$ and $x_{i+k}$ chosen by ${\mathrm{\Delta }}_{\mathrm{𝑚𝑎𝑟𝑘}}$ is a multiple of $m$, i.e. ${\mathrm{\Delta }}_{\mathrm{𝑚𝑎𝑟𝑘}}$ finds a mistake at a distance divisible by $m$.

If $M$ accepts the empty input, a run of $𝒮$ can start with the encoding of the accepting run of $M$. Since the run only uses the first $m$ tape cells, there exists such an encoding where the distance between two consecutive $\mathrm{\#}$ is always $m$; therefore, the run of $𝒮$ can never terminate with ${\mathrm{\Delta }}_{\mathrm{𝑒𝑛𝑑}}$. Moreover, ${\mathrm{\Delta }}_{\mathrm{𝑚𝑎𝑟𝑘}}$ can only choose distances $k\le 2m-1$ as otherwise there will be two $\mathrm{\#}$ between position $i+1$ and $i+k$. If $k\ne m$, then ${\mathrm{\Delta }}_{\mathrm{𝑢𝑛𝑚𝑎𝑟𝑘}}$ will unmark the positions in the next transition; and $k=m$ cannot be chosen because the correct run has no “mistakes” for ${\mathrm{\Delta }}_{\mathrm{𝑚𝑎𝑟𝑘}}$ to find. Hence such a run cannot terminate.

If $M$ does not accept the empty input, then there exists no run of $M$ starting with the empty input and ending with an accepting configuration. That is, every encoding of such a run in $𝒮$ must have a mistake, i.e. there must exist symbols $x_{i-1}$, $x_i$, $x_{i+1}$, $x_{i+2}$, $x_{i+lm}$ where $x_{i+lm}$ does not result from $x_{i-1}{x}_i{x}_{i+1}{x}_{i+2}$, where $l\in \mathbb{N}$ s.t. $lm$ is the distance between two consecutive $\mathrm{\#}$. Such a mistake will almost surely be eventually “found” by ${\mathrm{\Delta }}_{\mathrm{𝑚𝑎𝑟𝑘}}$, and the run will terminate. If the distance between two consecutive $\mathrm{\#}$ is not a multiple of $m$, then the run can terminate with ${\mathrm{\Delta }}_{\mathrm{𝑒𝑛𝑑}}$. In both cases, the run will almost surely eventually terminate. $◀$

One can reduce from almost sure termination by adding a new configuration $a$, setting $L:=\{a\}$, and adding transitions $(a,a)$ and $(t,a)$ for every $t\in T$. $◀$

Abstract deadlock-freedom is the problem whether $\text{PReach}(ℐ)\cap T=\mathrm{\varnothing }$. A nondeterministic algorithm can guess a configuration $c\in 𝒞$ and check that $c\notin \overline{\text{PReach}(ℐ)}$ and $c\notin \overline{T}$. Since one can construct an exponential-sized NFA for $\overline{\text{PReach}(ℐ)}$ and a polynomial-sized NFA for $\overline{T}$, this algorithm needs exponential space.

For hardness, we reduce from Abstract Safety. Given an RTS $𝒮$ and a set $L$ of unsafe configurations, we construct ${𝒮}^{\prime }$ by adding a new configuration $t$ (in the length-preserving case, adding such a configuration for each length), adding self-loops to all configurations except $t$, adding transitions $(c,t)$ for every $c\in L$, and adding $t$ to all constraints (i.e. for every constraint $\phi$, we have $(\phi ,t)\in 𝒱$). This makes $t$ the only terminating configuration while not affecting the inductivity of any constraints. It is easy to see that abstract safety holds for $𝒮$ iff abstract deadlock-freedom holds for ${𝒮}^{\prime }$. $◀$

See the full version [30]. $◀$

The first statement of Lemma 5.4 shows that our definition of a potential run coincides with the definition of abstract safety in [19]: Abstract safety holds iff no potential run reaches $L$. The second statement will be used to characterise abstract liveness.

In the rest of the section, we show that Abstract Liveness and abstract sure termination, which can be seen as a special case of Abstract Liveness, are $\mathrm{𝖤𝖷𝖯𝖲𝖯𝖠𝖢𝖤}$-complete. We start with a lemma, similar to the starting point of To and Libkin in [43].

We use Lemma 5.4. If (a) holds, then the infinite sequence $c_0,c,c,\mathrm{\cdots }$ is a potential run. If (b) holds, then ${(c_i)}_{i\in {\mathbb{N}}_0}$ is a potential run. For the converse, let ${(c_i)}_{i\in {\mathbb{N}}_0}$ be a potential run that visits $L$ infinitely often. If $c_i=c_j\in L$ for some , then $(c_i,c_i)\in {\mathrm{\Delta }}^{\prime }\cup {(\text{PReach}\setminus \mathrm{𝖨𝖽})}^2$, and since $(c_i,c_i)\in \mathrm{𝖨𝖽}$, (a) holds. Otherwise, removing all configurations not in $L$ from the sequence yields a sequence of pairwise distinct configurations in $L$, and (b) holds. $◀$

The sequence in condition (b) is called an infinite directed clique, see [12]. Note that (b) never holds for length-preserving RTSs. We prove that both (a) and (b) can be decided in $\mathrm{𝖤𝖷𝖯𝖲𝖯𝖠𝖢𝖤}$.

One can guess a configuration $c\in 𝒞$ letter by letter and check that $c\in L$, $c\notin \overline{\text{PReach}(ℐ)}$ and $(c,c)\in \mathrm{\Delta }\cup {(\text{PReach}\setminus \mathrm{𝖨𝖽})}^2$. $(c,c)\in {(\text{PReach}\setminus \mathrm{𝖨𝖽})}^2$ is equivalent to there existing a $c^{\prime }\in 𝒞$ such that $c^{\prime }\ne c$ and $(c,c^{\prime }),(c^{\prime },c)\notin \overline{\text{PReach}}$. Since an NFA for $\overline{\text{PReach}(ℐ)}$ can be built using exponential space (see Theorem 5.1), the algorithm amounts to guessing $c,c^{\prime }$ letter by letter (in parallel) and running words on NFAs of at most exponential size. To do this, one can memorize the current set of states after each letter and check whether that set contains a final state of the NFA at the end. Since all involved NFAs are at most exponential, this algorithm takes exponential space, and the result follows from $\mathrm{𝖭𝖤𝖷𝖯𝖲𝖯𝖠𝖢𝖤}=\mathrm{𝖤𝖷𝖯𝖲𝖯𝖠𝖢𝖤}$. $◀$

For (b), we first need the following lemma, based on Lemma 4 from [43].

One direction is easy: if the four conditions hold, the sequence ${(c_i)}_{i\in {\mathbb{N}}_0}$ with $c_i:={\beta }_0\mathrm{\cdots }{\beta }_{i-1}{\alpha }_i$ satisfies (b). For the other direction, we make use of the transitivity of PReach, see the proof of Lemma 4 in [43]. $◀$

See the full version [30]. $◀$

Membership in $\mathrm{𝖤𝖷𝖯𝖲𝖯𝖠𝖢𝖤}$ follows from Lemmas 5.5, 5.6, and 5.8. $\mathrm{𝖤𝖷𝖯𝖲𝖯𝖠𝖢𝖤}$-hardness follows from an easy reduction from the abstract safety problem: One can add self-loops to all configurations in $L$ to make sure that (a) holds iff $\text{PReach}(ℐ)\cap L\ne \mathrm{\varnothing }$. Since self-loops do not affect whether constraints are inductive, PReach does not change. Note that for length-preserving RTSs, abstract infinite reachability is equivalent to (a). $◀$

Abstract sure termination is the special case of abstract liveness where $L=𝒞$ and therefore also in $\mathrm{𝖤𝖷𝖯𝖲𝖯𝖠𝖢𝖤}$. The hardness proof is more involved, see the full version [30]. $◀$

The scattered subword order on configurations is defined by: for every $c,c^{\prime }\in {\mathrm{\Sigma }}^{\ast }$, we have $c⪯c^{\prime }$ if $c=q_1\mathrm{\cdots }{q}_n\in {\mathrm{\Sigma }}^{\ast }$ and $c^{\prime }=w_0{q}_1{w}_1{q}_2\mathrm{\cdots }{q}_n{w}_n$ for some words $w_0,\mathrm{\dots },w_n\in {\mathrm{\Sigma }}^{\ast }$. A set $L$ of configurations is upward-closed if $c\in L$ and $c⪯c^{\prime }$ implies $c^{\prime }\in L$. It follows from Higman’s lemma that every upward-closed set of configurations is regular [34]. An RTS $𝒮=(𝒞,\mathrm{\Delta })$ is well-structured if for every $(c_1,c_2)\in \mathrm{\Delta }$ and every $c_1^{\prime }⪰c_1$ there exists a configuration $c_2^{\prime }⪰c_2$ such that $(c_1^{\prime },c_2^{\prime })\in \text{Reach}$.

The algorithm to compute ${\text{Reach}}^{-1}(L)$ is very simple: iterate the operation $L:=L\cup {\mathrm{\Delta }}^{-1}(L)$ until a fixpoint is reached. Theorem 5.11 immediately yields:

One needs to decide whether $\text{PReach}(ℐ)\subseteq \overline{T}\cap {\text{Reach}}^{-1}(L)$, i.e. whether $\overline{\text{PReach}(ℐ)}\cup (\overline{T}\cap {\text{Reach}}^{-1}(L))$ is universal. An NFA for $\overline{\text{PReach}(ℐ)}$ can be computed (see Theorem 5.1), and the statement follows. $◀$

Broadcast protocols [22, 27] and population protocols [11] are two models in which an arbitrarily large number of identical finite-state processes interact by broadcast or rendez-vous, respectively. In both models, configurations with $n$ processes can be modeled as words of length $n$ over the alphabet of process states, and the transition function is captured by a length-preserving RTS.

In lossy channel systems (LCS) a fixed set of finite-state processes communicate through unreliable FIFO channels that can lose messages [7]. LCS are made probabilistic by attaching probabilities to message losses [37, 3]. Channels have unbounded capacity, and so they cannot be modeled by length-preserving RTSs. So we consider parameterized lossy channel systems (PLCS), a variant in which channels have bounded capacity, but the capacity is a parameter. In other words, a PLCS is an infinite collection of LCS that only differ in the capacity of their channels (1,2, …).

In any of these models, Reach is not always effectively regular. (For PLCS see [5], for population protocols it follows from the fact that Reach is not always semilinear [36], and for broadcast protocols from the undecidability of recurrent reachability [27].) These negative results justify the interest of Theorem 5.12. Moreover, for population protocols Abstract A.S. Liveness is even in $\mathrm{𝖤𝖷𝖯𝖲𝖯𝖠𝖢𝖤}$, and so not worse than AbstractSafety:

Bozzelli and Ganty show in [15] that ${\text{Reach}}^{-1}(L)$ can be computed in $\mathrm{𝖤𝖷𝖯𝖲𝖯𝖠𝖢𝖤}$ for population protocols. $\overline{\text{PReach}(ℐ)}$ can also be computed in $\mathrm{𝖤𝖷𝖯𝖲𝖯𝖠𝖢𝖤}$, see Theorem 5.1. Hardness follows from the fact that AbstractSafety is $\mathrm{𝖤𝖷𝖯𝖲𝖯𝖠𝖢𝖤}$-hard [19]. $◀$