Fine-Grained Complexity
of Safety Verification

arXiv:1802.05559v1 [cs.LO] 15 Feb 2018

Peter Chini, Roland Meyer, and Prakash Saivasan
TU Braunschweig
{p.chini, roland.meyer, p.saivasan}@tu-bs.de

Abstract. We study the ﬁne-grained complexity of Leader Contributor
Reachability (LCR) and Bounded-Stage Reachability (BSR), two variants of the safety veriﬁcation problem for shared memory concurrent
programs. For both problems, the memory is a single variable over a ﬁnite data domain. We contribute new veriﬁcation algorithms and lower
bounds based on the Exponential Time Hypothesis (ETH) and kernels.
LCR is the question whether a designated leader thread can reach an unsafe state when interacting with a certain number of equal contributor
threads. We suggest two parameterizations: (1) By the size of the data
domain D and the size of the leader L, and (2) by the size of the contributors C. We present two algorithms, running in O∗ ((L · (D + 1))L·D · DD ) and
O∗ (4C ) time, showing that both parameterizations are ﬁxed-parameter
tractable. Further, we suggest a modiﬁcation of the ﬁrst algorithm, suitable for practical instances. The upper bounds are complemented by
(matching) lower bounds based on ETH and kernels.
For BSR, we consider programs involving t diﬀerent threads. We restrict
to computations where the write permission changes s times between
the threads. BSR asks whether a given conﬁguration is reachable via
such a s-stage computation. When parameterized by P, the maximum
size of a thread, and t, the interesting observation is that the problem
has a large number of diﬃcult instances. Formally, we show that there
is no polynomial kernel, no compression algorithm that reduces D or s
to a polynomial dependence on P and t. This indicates that symbolic
methods may be harder to ﬁnd for this problem.

1

Introduction

We study the fine-grained complexity of two safety verification problems [1,15,26]
for shared memory concurrent programs. The motivation to reconsider these
problems are recent developments in fine-grained complexity theory [9,32,6,29].
They suggest that classifications such as NP or even FPT are too coarse to explain
the success of verification methods. Instead, it should be possible to identify the
precise influence that parameters of the input have on the verification time. Our
contribution confirms this idea. We give new verification algorithms for the two
problems that, for the first time, can be proven optimal in the sense of finegrained complexity theory. To state the results, we need some background. As
we proceed, we explain the development of fine-grained complexity theory.

There is a well-known gap between the success that verification tools see
in practice and the judgments about computational hardness that worst-case
complexity is able to give. The applicability of verification tools steadily increases
by tuning them towards industrial instances. The complexity estimation is stuck
with considering the input size (or at best assumes certain parameters to be
constant, which does not mean much if the runtime is then nk , where n is the
input size and k the parameter).
The observation of a gap between practical algorithms and complexity theory
is not unique to verification but made in every field that has to solve hard computational problems. Complexity theory has taken up the challenge to close the
gap. So-called fixed-parameter tractability (FPT) [10,12] proposes to identify parameters k so that the runtime is f (k)poly(n), where f is a computable function.
These parameters are powerful in the sense that they dominate the complexity.
For an FPT-result to be useful, function f should only be mildly exponential,
and of course k should be small in the instances of interest. Intuitively, they are
what one needs to optimize. Fine-grained complexity is the study of upper and
lower bounds on the function. Indeed, the fine-grained complexity of a problem
is written as O∗ (f (k)), emphasizing f and k and suppressing the polynomial
part. For upper bounds, the approach is still to come up with an algorithm.
For lower bounds, fine-grained complexity has taken a new and very pragmatic perspective. For the problem of n-variable 3-SAT the best known algorithm
runs in 2n , and this bound has not been been improved since 1970. The idea
is to take improvements on this problem as unlikely, known as the exponentialtime hypothesis (ETH) [29]. ETH serves as a lower bound that is reduced to
other problems [32]. An even stronger assumption about n-variable SAT, called
SETH [29,6], and a similar one about Set Cover [9] allow for lower bounds like
the absence of (2 − ε)n algorithms.
In this work, we contribute fine-grained complexity results for verification problems on concurrent programs. The first problem is reachability for
a leader thread that is interacting with an unbounded number of contributors (LCR) [26,15]. We show that, assuming a parameterization by the size of
the leader L and the size of the data domain D, the problem can be solved in
O∗ ((L · (D + 1))L·D · DD ). At the heart of the algorithm is a compression of computations into witnesses. To check reachability, our algorithm then iterates over
candidates for witnesses and checks each of them for being a proper witness. Interestingly, we can formulate a variant of the algorithm that seems to be suited
for large state spaces.
Using ETH, we show that the algorithm is (almost) optimal. Moreover, the
problem is shown to have a large number of hard instances. Technically, there is
no polynomial kernel [4,5]. Experience with kernel lower bounds is still limited.
This notion of hardness seems to indicate that symbolic methods are hard to
apply to the problem. The lower bounds that we present share similarities with
the reductions from [23,7,24].

If we consider the size of the contributors as a parameter, we obtain a singly
exponential upper bound that we also prove to be tight. The saturation based
technique that we use is inspired by thread-modular reasoning [19,20,25,28].
The second problem we study generalizes bounded context switching.
Bounded stage reachability (BSR) asks whether a state is reachable if there
is a bound s on the number of times the write permission is allowed to change
between the threads [1]. Again, we show the new form of kernel lower bound.
The result is tricky and highlights the power of the computation model.
The results are summarized by the table below. Two findings stand out,
we highlight them in gray. We present a new algorithm for LCR. Moreover, we
suggest kernel lower bounds as hardness indicators for verification problems. The
lower bound for BSR is particularly difficult to achieve.
Problem

Upper Bound
∗

LCR(D, L) O ((L · (D + 1))
LCR(C)

O ∗ (4C )

BSR(P, t) O ∗ (P2t )

Lower Bound
L·D

D

√
o( L·D·log(L·D)

·D ) 2

Kernel
No poly.

2o(C)

No poly.

2o(t·log(P))

No poly.

Related work Concurrent programs communicating through a shared memory
and having a fixed number of threads have been extensively studied [13,21,27,2].
The leader contributor reachability problem as considered in this paper was
introduced as parametrized reachability in [26]. In [15], it was shown to be NPcomplete when only finite state programs are involved and PSPACE-complete
for recursive programs. In [30], the parameterized pairwise reachability problem
was considered and shown to be decidable. Parameterized reachability under a
variant of round robin scheduling was proven decidable in [31].
The bounded stage restriction on the computations of concurrent programs
as considered here was introduced in [1]. The corresponding reachability problem
was shown to be NP-complete when only finite state programs are involved. The
problem remains in NEXP-time and PSPACE-hard for a combination of counters
and a single pushdown. The bouned stage restriction generalizes the concept of
bounded context switching from [33], which was shown to be NP-complete in
that paper. In [8], FPT-algorithms for bounded context switching were obtained
under various parameterization. In [3], networks of pushdowns communicating
through a shared memory were analyzed under various topological restrictions.
There have been few efforts to obtain fixed-parameter tractable algorithms
for automata and verification-related problems. FPT-algorithms for automata
problems have been studied in [18,17,34]. In [11], model checking problems for
synchronized executions on parallel components were considered and proven intractable. In [14], the notion of conflict serializability was introduced for the
TSO memory model and an FPT-algorithm for checking serializability was provided. The complexity of predicting atomicity violation on concurrent systems
was considered in [16]. The finding is that FPT-solutions are unlikely to exist.

2

Preliminaries

We introduce our model for programs, which is fairly standard and taken
from [1,26,15], and give the basics on fixed-parameter tractability.
Programs A program consists of finitely many threads that access a shared
memory. The memory is modeled to hold a single value at a time. Formally, a
(shared memory) program is a tuple A = (D , a0 , (Pi )i∈[1..t] ). Here, D is the data
domain of the memory and a0 ∈ D is the initial value. Threads are modeled as
control-flow graphs that write values to or read values from the memory. These
operations are captured by Op(D ) = {!a, ?a | a ∈ D }. We use the notation
W (D ) = {!a | a ∈ D } for the write operations and R(D ) = {?a | a ∈ D }
for the read operations. A thread Pid is a non-deterministic finite automaton
(Op(D ), Q, q 0 , δ) over the alphabet of operations. The set of states is Q with
q 0 ∈ Q the initial state. The final states will depend on the verification task.
The transition relation is δ ⊆ Q × Op(D ) ∪ {ǫ} × Q. We extend it to words and
w
also write q −
→ q ′ for q ′ ∈ δ(q, w). Whenever we need to distinguish between
different threads, we add indices and write Qid or δid .
The semantics of a program is given in terms of labeled transitions between
configurations. A configuration is a pair (pc, a) ∈ (Q1 × · · · × Qt ) × D . The
program counter pc is a vector that shows the current state pc(i) ∈ Qi of each
thread Pi . Moreover, the configuration gives the current value in memory. We
call c0 = (pc 0 , a0 ) with pc 0 (i) = qi0 for all i ∈ [1..t] the initial configuration. Let C
denote the set of all configurations. The transition relation among configurations
→ ⊆ C × (Op(D ) ∪ {ǫ}) × C is obtained by lifting the transition relations of the
threads. To define it, let pc 1 = pc[i = qi ], meaning thread Pi is in state qi and
otherwise the program counter coincides with pc. Let pc 2 = pc[i = qi′ ]. If thread
?a

?a

Pi tries to read with the transition qi −→ qi′ , then (pc 1 , a) −→ (pc 2 , a). Note that
the memory is required to hold the desired value. If the thread has the transition
ǫ
ε
!b
!b
→ qi′ yields (pc 1 , a) −
→ (pc 2 , a). The
→ qi′ , then (pc 1 , a) −
→ (pc 2 , b). Finally, qi −
qi −
w
program’s transition relation is generalized to words, c −
→ c′ . We call such a
sequence of consecutive labeled transitions a computation. To indicate that there
is a word that justifies a computation from c to c′ , we write c →∗ c′ . We may
w
use an index −
→i to indicate that the computation was induced by thread Pi .
w
Where appropriate, we also use the program as an index, −
→A .
Fixed-Parameter Tractability We wish to study the fine-grained complexity
of safety verification problems for the above programs. This means our goal is to
identify parameters of these problems that have two properties. First, in practical
instances they are small. Second, assuming that these parameters are small, show
that there are efficient verification algorithms. Parametrized complexity makes
precise the idea of being efficient relative to a parameter.
A parameterized problem L is a subset of Σ ∗ × N. The problem is
fixed-parameter tractable if there is a deterministic algorithm that, given

(x, k) ∈ Σ ∗ × N, decides (x, k) ∈ L in time f (k)·|x|O(1) . We use FPT for the class
of all fixed-parameter tractable problems and say a problem is FPT to mean it
is in that class. Note that, f is a computable function that only depends on the
parameter k. It is common to denote the runtime by O∗ (f (k)) and suppress the
polynomial part. We will be interested in the precise dependence on the parameter, in upper and lower bounds on the function f . This study is often referred
to as fine-grained complexity.
Lower bounds on f are obtained by the Exponential Time Hypothesis (ETH).
It assumes that there is no algorithm solving n-variable 3-SAT in 2o(n) time. The
reasoning is as follows: If f drops below a certain bound, ETH would fail.
While many parameterizations of NP-hard problems were proven to be
fixed-parameter tractable, there are problems that are unlikely to be FPT.
Such problems are hard for the complexity class W[1]. The appropriate
notion of reduction for a theory of relative hardness in parameterized
complexity is called parameterized reduction.

3

Leader Contributor Reachability

We consider the leader contributor reachability problem for shared memory programs. The problem was introduced in [26] and shown to be NP-complete in [15]
for the finite-state case.1 We contribute two new verification algorithms that
target two parameterizations of the problem. In both cases, our algorithms establish fixed-parameter tractability. Moreover, with matching lower bounds we
prove them to be optimal even in the fine-grained sense.
An instance of the leader contributor reachability problem is given by a
shared memory program of the form A = (D , a0 , (PL , (Pi )i∈[1..t] )). The program
has a designated leader thread PL and several contributor threads P1 , . . . , Pt . In
addition, we are given a set of unsafe states for the leader. The task is to check
whether the leader can reach an unsafe state when interacting with a number of
instances of the contributors. It is worth noting that the problem can be reduced
to having a single contributor. Let the corresponding thread PC be the union
of P1 , . . . , Pt (constructed using an initial ǫ-transition). We base our complexity
analysis on this simplified formulation of the problem.
For the definition, let A = (D , a0 , (PL , PC )) be a program with two threads.
Let FL ⊆ QL be a set of unsafe states of the leader. For t ∈ N, define the program
At = (D , a0 , (PL , (PC )i∈[1..t] )) to have t copies of PC . Further, let C f be the set
of configurations where the leader is in an unsafe state (from FL ). The problem
of interest is as follows:
Leader Contributor Reachability (LCR)
Input:
A program A = (D , a0 , (PL , PC )) and a set of states FL ⊆ QL .
Question: Is there a t ∈ N such that c0 →∗At c for some c ∈ C f ?
1

The problem is called parameterized reachability in these works. We renamed it to
avoid confusion with parameterized complexity.

We consider two parameterizations of LCR. First, we parameterize by D, the
size of the data domain D , and L, the number of states of the leader PL . We
denote the parameterization by LCR(D, L). While for LCR(D, L) we obtain an
FPT-algorithm, it is not likely that LCR(D) and LCR(L) admit the same. These
parameterizations are W[1]-hard. For details, we refer to the Appendix.
The second parameterization that we consider is LCR(C), a parameterization
by the number of states of the contributor PC . We prove that the parameter is
enough to obtain an FPT-algorithm.
3.1

Parameterization by Memory and Leader

We give an algorithm that solves LCR in time O∗ ((L·(D+1))L·D ·DD ), which means
LCR(D, L) is FPT. We then show how to modify the algorithm to solve instances
of LCR as they are likely to occur in practice. Interestingly, the modified version
of the algorithm lends itself to an efficient implementation based on off-the-shelf
sequential model checkers. We conclude with lower bounds for PR(D, L).
Upper Bound We give an algorithm for the parameterization LCR(D, L). The
key idea is to compactly represent computations that may be present in an
instance of the given program. To this end, we introduce a domain of so-called
witness candidates. The main technical result, Lemma 4, links computations
and witness candidates. It shows that reachability of an unsafe state holds in
an instance of the program if and only if there is a witness candidate that
is valid (in a precise sense). With this, our algorithm iterates over all witness
candidates and checks each of them for being valid. To state the overall result,
L·D
let Wit (L, D ) = (L · (D + 1)) · DD · L be the number of witness candidates and let
3
2
2
Valid (L, D, C ) = L · D · C be the time it takes to check validity of a candidate.
Note that it is polynomial.
Theorem 1. LCR can be solved in time O(Wit (L, D ) · Valid (L, D, C )).
Let A = (D , a0 , (PL , PC )) be the program of interest and FL be the set of
unsafe states in the leader. Assume we are given a computation ρ showing that
PL can reach a state in FL when interacting with a number of contributors. We
explain the main ideas to find an efficient representation for ρ that still allows
for the reconstruction of a similar computation. To simplify the presentation, we
assume the leader never writes !a and immediately reads ?a the same value. If
this is the case, the read can be replaced by ǫ.
In a first step, we delete most of the moves in ρ that were carried out by
the contributors. We only keep first writes. For each value a, this is the write
!a
transitions fw (a) = c −→ c′ where a is written by a contributor for the first time.
The reason we can omit subsequent writes of a is the following: If fw (a) is carried
out by contributor P1 , we can assume that there is an arbitrary number of other
contributors that all mimicked the behavior of P1 . This means whenever P1 did
a transition, they copycatted it right away. Hence, there are arbitrarily many
contributors pending to write a. Phrased differently, the symbol a is available

for the leader whenever PL needs to read it. The idea goes back to the Copycat
Lemma stated in [15]. The reads of the contributors are omitted as well. We will
make sure they can be served by the first writes and the moves done by PL .
After the deletion, we are left with a shorter expression ρ′ . We turn it into a
word w over the alphabet QL ∪D⊥ ∪ D̄ with D⊥ = D ∪{⊥} and D̄ = {ā | a ∈ D }.
!a/?a/ε

Each transition c −−−−−→L c′ in ρ′ that is due to the leader moving from q to
q ′ is mapped (i) to q.a.q ′ if it is a write and (ii) to q.⊥.q ′ otherwise. A first
a
write fw (a) = c −
→ c′ of a contributor is mapped to ā. We may assume that
the resulting word w is of the form w = w1 .w2 with w1 ∈ ((QL .D⊥ )∗ .D̄)∗ and
w2 ∈ (QL .D⊥ )∗ .FL . Note that w can still be of unbounded length.
In order to find a witness of bounded length, we compress w1 and w2 to
w1′ and w2′ . Between two first writes ā and b̄ in w1 , the leader can perform an
unbounded number of transitions, represented by a word in (QL .D⊥ )∗ . Hence,
there are states q ∈ QL repeating between ā and b̄. We contract the word between
the first and the last occurrence of q into just a single state q. This state now
represents a loop on PL . Since there are L states in the leader, this bounds the
number of contractions. Furthermore, we know that the number of first writes is
bounded by D, each symbol can be written for the first time at most once. Thus,
the compressed string w1′ is in the language ((QL .D⊥ )≤L .D̄)≤D .
The word w2 is of the form w2 = q.u for a state q ∈ QL and a word u.
We truncate the word u and only keep the state q. Then we know that there is
a computation leading from q to a state in FL where PL can potentially write
any symbol but read only those symbols which occurred as a first write in w1′ .
Altogether, we are left with a word of bounded length.
Definition 2. The set of witness candidates is E = ((QL .D⊥ )≤L .D̄)≤D .QL .

To characterize computations in terms of witness candidates, we define the
notion of validity. This needs some notation. Consider a word w = w1 . . . wℓ
over some alphabet Γ . For i ∈ [1..ℓ], we set w[i] = wi and w[1..i] = w1 . . . wi . If
Γ ′ ⊆ Γ , we use w ↓Γ ′ for the projection of w to the letters in Γ ′ .
Consider a witness candidate w ∈ E and let i ∈ [1..|w|]. We use D̄(w, i)
for the set of all first writes that occurred in w up to position i. Formally,
D̄ (w, i) = {a | ā is a letter in w[1..i] ↓D̄ }. We abbreviate D̄(w, |w|) as D̄(w). Let
q ∈ QL and S ⊆ D . Recall that the state represents a loop in PL . The set of all
letters written within a loop from q to q when reading only symbols from S is
v1 !av2
−−→L q}.
Loop(q, S) = {a | a ∈ D and ∃v1 , v2 ∈ (W (D ) ∪ R(S))∗ : q −−
The definition of validity is given next. The three requirements are made
precise in the text below.
Definition 3. A witness candidate w ∈ E is valid if it satisfies the following
properties: (1) First writes are unique. (2) The word w encodes a run in PL . (3)
There are supportive computations on the contributors.
(1) If w ↓D̄ = c¯1 . . . c¯ℓ , then the c¯i are pairwise different.
!a

i
(2) Let w ↓QL ∪D⊥ = q1 a1 q2 a2 . . . aℓ qℓ+1 . If ai ∈ D , then qi −−→
L qi+1 ∈ δL
ε
→L qi+1 .
is a write transition of PL . If ai = ⊥, then we have an ε-transition qi −

?a

Alternatively, there is a read qi −→L qi+1 of a symbol a ∈ D̄(w, pos(ai )) that
already occurred within a first write (the leader does not read the own writes).
0
Here, we use pos(ai ) to access the position of ai in w. State q1 = qL
is initial. There is a run from qℓ+1 to a state qf ∈ FL . During this run, reading is
restricted to symbols that occurred as first writes in w. Formally, there is a
v
→L qf .
v ∈ (W (D ) ∪ R(D̄ (w)))∗ such that qℓ+1 −
u!a

0
(3) For each prefix vā of w with ā ∈ D̄ there is a computation qC
−−→C q on
PC so that the reads in u can be obtained from v. Formally, let u′ = u ↓R(D) .
Then there is an embedding of u′ into v, a monotone map µ : [1..|u′ |] → [1..|v|]
that satisfies the following. Let u′ [i] = ?a with a ∈ D . The read is served in one of
the following three ways. We may have v[µ(i)] = a, which corresponds to a write
of a by PL . Alternatively, v[µ(i)] = q ∈ QL and a ∈ Loop(q, D̄ (w, µ(i))). This
amounts to reading from a leader’s write that was executed in a loop. Finally,
we may have a ∈ D̄(w, µ(i)), corresponding to reading from another contributor.

Lemma 4. There is a t ∈ N so that c0 →∗At c with c ∈ C f if and only if there
is a valid witness candidate w ∈ E.
Our algorithm iterates over all witness candidates w ∈ E and tests whether w
L·D
is valid. The number of candidates Wit (L, D) is given by (L · (D + 1)) ·DD ·L. This
is due to the fact that we can force a witness candidate to have maximum length
via inserting padding symbols. The number of candidates constitutes the first
factor of the runtime stated in Theorem 1. The polynomial factor Valid (L, D, C)
is due to the following Lemma.
Lemma 5. Validity of w ∈ E can be checked in time O(L3 · D 2 · C 2 ).
Practical Algorithm We improve the above algorithm so that it should work
well on practical instances. The idea is to factorize the leader along its strongly
connected components (SCCs), the number of which is assumed to be small in real
programs. Technically, our improved algorithm works with valid SCC-witnesses.
They symbolically represent SCCs rather than loops in the leader. To state the
complexity, we define the straight line depth, the number of SCCs the leader may
visit during a computation. The definition needs a graph construction.
Let V ⊆ D̄ ≤D contain only words that do not repeat letters. Let
r = c̄1 . . . c̄ℓ ∈ V and i ∈ [0..ℓ]. By PL ↓i we denote the automaton obtained
from PL by removing all transitions that read a value outside {c1 , . . . , ci }. Let
SCC(PL ↓i ) denote the set of all SCCs in this automaton. We construct the directed graph G(PL , r) as follows. The vertices are the SCCs of all PL ↓i , i ∈ [0..ℓ].
There is an edge between S, S ′ ∈ SCC(PL ↓i ), if there are states q ∈ S, q ′ ∈ S ′
with q → q ′ in PL ↓i . If S ∈ SCC(PL ↓i−1 ) and S ′ ∈ SCC(PL ↓i ), we only get an
edge if we can get from S to S ′ by reading ci . Note that the graph is acyclic.
The depth d(r) of PL relative to r is the length of the longest path in G(PL , r).
The straight line depth is d = max{d(r) | r ∈ V}. The number of SCCs s is
the size of SCC(PL ↓0 ). With these values at hand, the number of SCC-witness
candidates (the definition of which can be found in the appendix) can be bounded

by WitSCC (s, D, d) ≤ (s · (D + 1))d · DD · 2D+d . The time needed to test whether a
candidate is valid is ValidSCC (L, D, C, d) = L2 · D · C2 · d2 .
Theorem 6. LCR can be solved in time O(WitSCC (s, D, d)·ValidSCC (L, D, C, d)).
For this algorithm, what matters is that the leader’s state space is strongly
connected. The number of states has limited impact on the runtime.
Lower bound We prove that the algorithm
from Theorem 1 is only a root√
factor away from being optimal: A 2o( L·D·log(L·D)) -time algorithm for LCR would
contradict ETH. We achieve the lower bound by a reduction from k × k Clique,
the problem of finding a clique of size k in a graph the vertices of which are
elements of a k × k matrix. Moreover, the clique has to contain one vertex from
each row. Unless ETH fails, the problem cannot be solved in time 2o(k·log(k)) [32].
Technically, we construct from an instance (G, k) of k × k Clique an instance
(A = (D , a0 , (PL , PC )), FL ) of LCR such that D = O(k) and L = O(k). Furthermore, we show that G contains the desired clique of size k if and only if there
∗
f
is a t ∈ N such that c0 →
t c with c ∈ C . Suppose we had an algorithm for
√A
LCR running in time 2o( L·D·log(L·D)) . Combined with√ the reduction, this would
2
2
yield an algorithm for k × k Clique with runtime 2o( k ·log(k )) = 2o(k·log k) . But
unless ETH fails, such an algorithm cannot exist.
Proposition 7. LCR cannot be solved in time 2o(

√
L·D·log(L·D))

unless ETH fails.

We assume that the vertices V of G are given by tuples (i, j) with i, j ∈ [1..k],
where i denotes the row and j denotes the column. In the reduction, we need the
leader and the contributors to communicate on the vertices of G. However, we
cannot store tuples (i, j) in the memory as this would cause a quadratic blow-up
D = O(k 2 ). Instead, we communicate a vertex (i, j) as a string row(i). col(j). We
distinguish between row- and column-symbols to avoid stuttering, the repeated
reading of the same symbol. With this, it cannot happen that a thread reads a
row-symbol twice and takes it for a column.
The program starts its computation with each contributor choosing a vertex
(i, j) to store. For simplicity, we denote a contributor storing (i, j) by P(i,j) . Note
that there can be copies of P(i,j) .
Since there are arbitrarily many contributors, the chosen vertices are only a
superset of the clique we want to find. To cut away the false vertices, the leader
PL guesses for each row the vertex belonging to the clique. To this end, the
program performs for each i ∈ [1..k] the following steps: If (i, ji ) is the vertex
of interest, PL first writes row(i) to the memory. Each contributor that is still
active reads the symbol and moves on for one state. Then PL communicates the
column by writing col(ji ). Again, the active contributors P(i′ ,j ′ ) read.
Now we distinguish three cases: (1) If i′ 6= i, the contributor P(i′ ,j ′ ) stores a
vertex of a different row. The computation in P(i′ ,j ′ ) can only go on if (i′ , j ′ ) is
connected to (i, ji ) in G. Otherwise it will stop. (2) If i′ = i and j ′ = ji , then
P(i′ ,j ′ ) stores exactly the vertex guessed by PL . In this case, P(i′ ,j ′ ) can continue

its computation. (3) If i′ = i and j ′ 6= j, thread P(i′ ,j ′ ) stores a different vertex
from row i. The contributor has to stop its computation.
After k such rounds, there are only contributors left that store vertices
guessed by PL . Furthermore, each two of these vertices are connected. Hence,
they form a clique. To transmit this information to PL , each P(i,ji ) writes #i to
the memory, a special symbol for row i. After PL has read the string #1 . . . #k ,
it moves to its final state. A formal construction can be found in the Appendix.
Absence of a Polynomial Kernel A kernelization of a parameterized problem
is a compression algorithm. Given an instance, it returns an equivalent instance
the size of which is bounded by a function only in the parameter. From an
algorithmic perspective, kernels put a bound on the number of hard instances of
the problem. Indeed, the search for small kernels is a key interest in algorithmics,
similar to the search for fast FPT-algorithms. Even more, it can be shown that
kernels exist if and only if a problem admits an FPT-algorithm [10].
Let Q be a parameterized problem. A kernelization of Q is an algorithm
that transforms, in polynomial time, a given instance (B, k) into an equivalent
instance (B ′ , k ′ ) such that |B ′ | + k ′ ≤ g(k), where g is a computable function. If
g is a polynomial, we say that Q admits a polynomial kernel.
Unfortunately, for many problems the community failed to come up with
polynomial kernels. This lead to the contrary approach, namely disproving their
existence [22,4,5]. Such a result constitutes an exponential lower bound on the
number of hard instances. Like computational hardness results, such a bound
is seen as an indication of general hardness of the problem. Technically, the
existence of a polynomial kernel for the problem of interest is shown to imply
NP ⊆ coNP/poly. But this inclusion is unlikely as it would cause a collapse of
the polynomial hierarchy to the third level [35].
In order to link the occurrence of a polynomial kernel for LCR(D, L) with the
above inclusion, we follow the framework developed in [5]. Let Γ be an alphabet.
A polynomial equivalence relation is an equivalence relation R on Γ ∗ with the
following properties: Given x, y ∈ Γ ∗ , it can be decided in time polynomial in
|x| + |y| whether (x, y) ∈ R. Moreover, for n ∈ N there are at most polynomially
many equivalence classes in R restricted to Γ ≤n .
The key tool for proving kernel lower bounds are cross-compositions: Let
L ⊆ Γ ∗ be a language and Q ⊆ Γ ∗ × N be a parameterized language. We say
that L cross-composes into Q if there exists a polynomial equivalence relation
R and an algorithm C, the cross-composition, with the following properties: C
takes as inputP
ϕ1 , . . . , ϕI ∈ Γ ∗ , all equivalent under R. It computes in time
I
polynomial in ℓ=1 |ϕℓ | a string (y, k) ∈ Γ ∗ × N such that (y, k) ∈ Q if and only
if there is an ℓ ∈ [1..I] with ϕℓ ∈ L. Furthermore, k ≤ p(maxℓ∈[1..I] |ϕℓ | + log(I))
for a polynomial p.
It was shown in [5] that a cross-composition of any NP-hard language into
a parameterized language Q prohibits the existence of a polynomial kernel for
Q unless NP ⊆ coNP/poly. In order to make use of this result, we show how to
cross-compose 3-SAT into LCR(D, L). This yields the following:

Theorem 8. LCR(D, L) does not admit a poly. kernel unless NP ⊆ coNP/poly.
The difficulty of finding a cross-composition is in the restriction on the size
of the parameters. This affects D and L: Both parameters are not allowed to
depend polynomially on I, the number of given 3-SAT-instances. We resolve
the polynomial dependence by encoding the choice of a 3-SAT-instance into the
contributors via a binary tree.
Proof (Idea). Assume some encoding of Boolean formulas as strings over a finite
alphabet. We use the polynomial equivalence relation R defined as follows: Two
strings ϕ and ψ are equivalent under R if both encode 3-SAT-instances, and the
numbers of clauses and variables coincide.
Let the given 3-SAT-instances be ϕ1 , . . . , ϕI . Every two of them are equivalent
under R. This means that all ϕℓ have the same number of clauses m and use
ℓ
the same set of variables {x1 , . . . , xn }. We assume that ϕℓ = C1ℓ ∧ · · · ∧ Cm
.
We construct a program proceeding in three phases. First, it chooses an
instance ϕℓ , then it guesses a valuation for all variables, and in the third phase
it verifies that the valuation satisfies ϕℓ . While the second and the third phase
do not cause a dependence of the parameters on I, the first phase does. It is not
possible to guess a number ℓ ∈ [1..I] and communicate it via the memory as this
would provoke a polynomial dependence of D on I.
To implement the first phase without a polynomial dependence, we transmit
the indices of the 3-SAT-instances in binary. The leader guesses and writes tuples
(u1 , 1), . . . , (ulog(I) , log(I)) with uℓ ∈ {0, 1} to the memory. This amounts to
choosing an instance ϕℓ with binary representation bin(ℓ) = u1 . . . ulog(I) .
It is the contributors’ task to store this choice. Each time, the leader writes
a tuple (ui , i), the contributors read and branch either to the left, if ui = 0, or
to the right, if ui = 1. Hence, in the first phase, the contributors are binary trees
with I leaves, each leaf storing the index of an instance ϕℓ . Since we did not
assume that I is a power of 2, there may be computations arriving at leaves that
do not represent proper indices. In this case, the computation deadlocks.
The size of D and PL in the first phase is O(log(I)). This satisfies the sizerestrictions of a cross-composition.
For guessing the valuation in the second phase, the system communicates on
tuples (xi , v) with i ∈ [1..n] and v ∈ {0, 1}. The leader guesses such a tuple for
each variable and writes it to the memory. Any participating contributor is free
to read one of the tuples. After reading, it stores the variable and the valuation.
In the third phase, the satisfiability check is performed as follows: Each contributor that is still active has stored in its current state the chosen instance
ϕℓ , a variable xi , and its valuation vi . Assume that xi when evaluated to vi
satisfies Cjℓ , the j-th clause of ϕℓ . Then the contributor loops in its current state
while writing the symbol #j . The leader waits to read the string #1 . . . #m . If
PL succeeds, we are sure that the m clauses of ϕℓ were satisfied by the chosen
valuation. Thus, ϕℓ is satisfiable and PL moves to its final state. For details of
the construction, we refer to the Appendix.
⊓
⊔

3.2

Parameterization by Contributors

We show that the size of the contributors C has a wide influence on the complexity
of LCR. We give an algorithm singly exponential in C, provide a matching lower
bound, and prove the absence of a polynomial kernel.
Upper Bound Our algorithm is based on saturation. We keep the states reachable by the contributors in a set and saturate it. This leads to a more compact
representation of the program. Technically, we reduce LCR to a reachability
problem on a finite automaton. The result is as follows.
Proposition 9. LCR can be solved in time O(4C · L4 · D 3 · C 2 ).
The main observation is that keeping one set of states for all contributors suffices to represent a computation. Let S ⊆ QC be the set of states
reachable by the contributors in a given computation. By the Copycat Lemma
[15], we can assume for each q ∈ S an arbitrary number of contributors
that are currently in state q. This means that we do not have to distinguish
between different contributor instances.
Formally, we reduce the search space to QL × D × P(QC ). Instead of storing
explicit configurations, we store tuples (qL , a, S), where qL ∈ QL , a ∈ D , and
S ⊆ QC . Between such tuples, the transition relation is as follows. Transitions
of the leader change the state and the memory as expected. The contributors
also change the memory but saturate S instead of changing the state. Formally,
if there is a transition from q ∈ S to q ′ , we add q ′ to S.
Lemma 10. There is a t ∈ N so that c0 →∗At c with c ∈ C f if and only if there
0
0
is a run from (qL
, a0 , {qC
}) to a state in FL × D × P(QC ).
The dominant factor in the complexity estimation of Proposition 9 is the
time needed to construct the state space. It takes time O(4C · L4 · D 3 · C 2 ). For
the formal construction and the proof of Lemma 10, we refer to the Appendix.
Lower Bound and Absence of a Polynomial Kernel We present two lower
bounds for LCR. The first is based on ETH: We show that there is no 2o(C) -time
algorithm for LCR unless ETH fails. This indicates that the above algorithm is
asymptotically optimal. Technically, we give a reduction from n-variable 3-SAT
to LCR such that the size of the contributor in the constructed instance is O(n).
Then a 2o(C) -time algorithm for LCR yields a 2o(n) -time algorithm for 3-SAT,
a contradiction to ETH.
With a similar reduction, one can cross-compose 3-SAT into LCR(C). This
shows that the problem does not admit a polynomial kernel. The precise constructions and proofs can be found in the Appendix.
Proposition 11.
a) LCR cannot be solved in time 2o(C) unless ETH fails.
b) LCR(C ) does not admit a polynomial kernel unless NP ⊆ coNP/poly.

4

Bounded-Stage Reachability

The bounded-stage reachability problem is a simultaneous reachability problem. It
asks whether all threads of a program can reach an unsafe state when restricted
to s-stage computations. These are computations where the write permission
changes s times. The problem was first analyzed in [1] and shown to be NPcomplete for finite-state programs. We give matching upper and lower bounds in
terms of fine-grained complexity and prove the absence of a polynomial kernel.
Let A = (D , a0 , (Pi )i∈[1..t] ) be a program. A stage is a computation in A
where only one of the threads writes. The remaining threads are restricted to
reading the memory. An s-stage computation is a computation that can be split
into s parts, each of which forming a stage.
Bounded-Stage Reachability (BSR)
Input:
A program A = (D , a0 , (Pi )i∈[1..t] ), a set C f ⊆ C, and s ∈ N.
Question: Is there an s-stage computation c0 →∗A c for some c ∈ C f ?
We focus on a parameterization of BSR by P, the maximum number of states
of a thread, and t, the number of threads. Let it be denoted by BSR(P, t). We
prove that the parameterization is FPT and present a matching lower bound. The
main result in this section is the absence of a polynomial kernel for BSR(P, t).
The result is technically involved and reveals hardness of the problem.
Parameterizations of BSR involving D and s, the number of stages, are not
interesting for fine-grained complexity theory. We can show that BSR is NP-hard
even for constant D and s. This immediately rules out FPT-algorithms in these
parameters. For details, we refer to the Appendix.
Upper Bound We show that BSR(P, t) is fixed-parameter tractable. The idea
is to reduce to reachability on a product automaton. The automaton stores the
configurations, the current writer, and counts up to the number of stages s. To
this end, it has O∗ (Pt ) many states. Details can be found in the Appendix.
Proposition 12. BSR can be solved in time O∗ (P 2t ).
Lower Bound By a reduction from k × k Clique, we show that a 2o(t·log(P)) -time
algorithm for BSR would contradict ETH. The above algorithm is optimal.
Proposition 13. BSR cannot be solved in time 2o(t·log(P)) unless ETH fails.
The reduction maps an instance of k × k Clique to an equivalent instance
(A = (D , a0 (Pi )i∈[1..t] ), C f , s) of BSR. Moreover, it keeps the parameters small.
We have that P = O(k 2 ) and t = O(k). As a consequence, a 2o(t·log(P)) -time
algorithm for BSR would yield an algorithm for k × k Clique running in time
2
2o(k·log(k )) = 2o(k·log(k)) . But this contradicts ETH.

Proof (Idea). For the reduction, let V = [1..k] × [1..k] be the vertices of G. We
define D = V ∪ {a0 } to be the domain of the memory. We want the threads to
communicate on the vertices of G. For each row we introduce a reader thread
Pi that is responsible for storing a particular vertex of the row. We also add
one writer, Pch , that is used to steer the communication between the Pi . Our
program A is given by (D , a0 , ((Pi )i∈[1..k] , Pch )).
Intuitively, the program proceeds in two phases. In the first phase, each Pi
non-deterministically chooses a vertex from the i-th row and stores it in its state
space. This constitutes a clique candidate (1, j1 ), . . . , (k, jk ) ∈ V . In the second
phase, thread Pch starts to write a random vertex (1, j1′ ) of the first row to the
memory. The first thread P1 reads (1, j1′ ) from the memory and verifies that the
read vertex is actually the one from the clique candidate. The computation in
P1 will deadlock if j1′ 6= j1 . The threads Pi with i 6= 1 also read (1, j1′ ) from the
memory. They have to check whether there is an edge between the stored vertex
(i, ji ) and (1, j1′ ). If this fails in some Pi , the computation in that thread will
also deadlock. After this procedure, the writer Pch guesses a vertex (2, j2′ ) and
writes it to the memory. Now the verification steps repeat. In the end, after k
repetitions of the procedure, we can ensure that the guessed clique candidate is
indeed a clique. The details are in the Appendix.
⊓
⊔
Absence of a Polynomial Kernel We show that BSR(P, t) does not admit a
polynomial kernel. To this end, we cross-compose 3-SAT into BSR(P, t).
Theorem 14. BSR(P, t) does not admit a poly. kernel unless NP ⊆ coNP/poly.
In the present setting, coming up with a cross-composition is non-trivial. Both
parameters, P and t, are not allowed to depend polynomially on the number I
of given 3-SAT-instances. Hence, we cannot construct an NFA that distinguishes
the I instances by branching into I different directions. This would cause a
polynomial dependence of P on I. Furthermore, it is not possible to construct
an NFA for each instance as this would cause such a dependence of t on I. To
circumvent the problems, some deeper understanding of the model is needed.
Proof (Idea). Let ϕ1 , . . . , ϕI be given 3-SAT-instances, where each two are equivalent under R, the polynomial equivalence relation of Theorem 8. Then each ϕℓ
ℓ
has m clauses and n variables {x1 , . . . , xn }. We assume ϕℓ = C1ℓ ∧ · · · ∧ Cm
.
In the program that we construct, the communication is based on 4-tuples of
the form (ℓ, j, i, v). Intuitively, such a tuple transports the following information:
The j-th clause in instance ϕℓ , Cjℓ , can be satisfied by variable xi with valuation
v. Hence, our data domain is D = ([1..I] × [1..m] × [1..n] × {0, 1}) ∪ {a0 }.
For choosing and storing a valuation of the xi , we introduce so-called variable
threads Px1 , . . . , Pxn . In the beginning, each Pxi non-deterministically chooses a
valuation for xi and stores it in its states.
We further introduce a writer Pw . During a computation, this thread guesses
exactly m tuples (ℓ1 , 1, i1 , v1 ), . . . , (ℓm , m, im , vm ) in order to satisfy m clauses
of potentially different instances. Each (ℓj , j, ij , vj ) is written to the memory by

Pw . All variable threads then start to read the tuple. If Pxi with i 6= ij reads it,
then the thread will just move one state further since the suggested tuple does
not affect the variable xi . If Pxi with i = ij reads the tuple, the thread will only
continue its computation if vj coincides with the value that Pxi guessed for xi
ℓ
and, moreover, xi with value vj satisfies clause Cj j .
Now suppose the writer did exactly m steps while each variable thread did
exactly m + 1 steps. This proves the satisfiability of m clauses by the chosen
valuation. But these clauses can be part of different instances: It is not ensured
that the clauses were chosen from one formula ϕℓ . The major difficulty of the
cross-composition lies in how to ensure exactly this.
We overcome the difficulty by introducing so-called bit checkers Pb , where
b ∈ [1.. log(I)]. Each Pb is responsible for the b-th bit of bin(ℓ), the binary
representation of ℓ, where ϕℓ is the instance we want to satisfy. When Pw writes
a tuple (ℓ1 , 1, i1 , v1 ) for the first time, each Pb reads it and stores either 0 or
1, according to the b-th bit of bin(ℓ1 ). After Pw has written a second tuple
(ℓ2 , 2, i2 , v2 ), the bit checker Pb tests whether the b-th bit of bin(ℓ1 ) and bin(ℓ2 )
coincide, otherwise it will deadlock. This will be repeated any time Pw writes a
new tuple to the memory.
Assume, the computation does not deadlock in any of the Pb . Then we can
ensure that the b-th bit of bin(ℓj ) with j ∈ [1..m] never changed during the
computation. This means that bin(ℓ1 ) = · · · = bin(ℓm ). Hence, the writer Pw
has chosen clauses of just one instance ϕℓ and with the current valuation, it is
possible to satisfy the formula. Since the parameters are bounded, P ∈ O(m)
and t ∈ O(n + log(I)), the construction constitutes a proper cross-composition.
For a formal construction and proof, we refer to the Appendix.
⊓
⊔

5

Conclusion

We have studied several parameterizations of LCR and BSR, two safety verification problems for shared memory concurrent programs. For LCR, we identified
the parameters D, L, and C. Our first algorithm showed that LCR(D, L) is FPT.
Then, we used a modification of the algorithm to obtain a verification procedure
valuable for practical instances. The main insight was that due to a factorization along strongly connected components, the impact of L can be reduced to a
polynomial factor in the time complexity. We also proved the absence of a polynomial kernel for LCR(D, L) and presented a lower bound which is a root-factor
away from the upper bound. For LCR(C) we gave a tight upper and lower bound.
The parameters of interest for BSR are P and t. We have shown that
a parameterization by both parameters is FPT and gave a matching lower
bound. The main contribution was to prove it unlikely that a polynomial
kernel exists for BSR(P, t). The proof relies on a technically involved crosscomposition that avoids a polynomial dependence of the parameters on the
number of given 3-SAT-instances.

References
1. M. F. Atig, A. Bouajjani, K. N. Kumar, and P. Saivasan. On bounded reachability
analysis of shared memory systems. In FSTTCS, volume 29 of LIPIcs, pages 611–
623. Schloss Dagstuhl, 2014.
2. M. F. Atig, A. Bouajjani, and S. Qadeer. Context-bounded analysis for concurrent
programs with dynamic creation of threads. In TACAS, volume 5505 of LNCS,
pages 107–123. Springer, 2009.
3. M. F. Atig, A. Bouajjani, and T. Touili. On the reachability analysis of acyclic
networks of pushdown systems. In CONCUR, volume 5201 of LNCS, pages 356–
371. Springer, 2008.
4. H. L. Bodlaender, R. G. Downey, M. R. Fellows, and D. Hermelin. On problems
without polynomial kernels. JCSS, 75(8):423–434, 2009.
5. H. L. Bodlaender, B. M. P. Jansen, and S. Kratsch. Kernelization lower bounds
by cross-composition. SIDAM, 28(1):277–305, 2014.
6. C. Calabro, R. Impagliazzo, and R. Paturi. The complexity of satisﬁability of small
depth circuits. In IWPEC, volume 5917 of LNCS, pages 75–85. Springer, 2009.
7. J. F. Cantin, M. H. Lipasti, and J. E. Smith. The complexity of verifying memory
coherence. In SPAA, pages 254–255. ACM, 2003.
8. P. Chini, J. Kolberg, A. Krebs, R. Meyer, and P. Saivasan. On the complexity
of bounded context switching. In ESA, volume 87 of LIPIcs, pages 27:1–27:15.
Schloss Dagstuhl, 2017.
9. M. Cygan, H. Dell, D. Lokshtanov, D. Marx, J. Nederlof, Y. Okamoto, R. Paturi,
S. Saurabh, and M. Wahlström. On problems as hard as CNF-SAT. ACM TALG,
12(3):41:1–41:24, 2016.
10. M. Cygan, F. V. Fomin, L. Kowalik, D. Lokshtanov, D. Marx, M. Pilipczuk,
M. Pilipczuk, and S. Saurabh. Parameterized algorithms. Springer, 2015.
11. S. Demri, F. Laroussinie, and P. Schnoebelen. A parametric analysis of the state
explosion problem in model checking. In STACS, volume 2285 of LNCS, pages
620–631. Springer, 2002.
12. R. G. Downey and M. R. Fellows. Fundamentals of Parameterized Complexity.
Springer, 2013.
13. A. Durand-Gasselin, J. Esparza, P. Ganty, and R. Majumdar. Model checking
parameterized asynchronous shared-memory systems. In CAV, volume 9206 of
LNCS, pages 67–84. Springer, 2015.
14. C. Enea and A. Farzan. On atomicity in presence of non-atomic writes. In TACAS,
volume 9636 of LNCS, pages 497–514. Springer, 2016.
15. J. Esparza, P. Ganty, and R. Majumdar. Parameterized veriﬁcation of asynchronous shared-memory systems. In CAV, volume 8044 of Lecture Notes in Computer Science, pages 124–140. Springer, 2013.
16. A. Farzan and P. Madhusudan. The complexity of predicting atomicity violations.
In TACAS, volume 5505 of LNCS, pages 155–169. Springer, 2009.
17. H. Fernau, P. Heggernes, and Y. Villanger. A multi-parameter analysis of hard
problems on deterministic ﬁnite automata. JCSS, 81(4):747–765, 2015.
18. H. Fernau and A. Krebs. Problems on ﬁnite automata and the exponential time
hypothesis. In CIAA, volume 9705 of LNCS, pages 89–100. Springer, 2016.
19. C. Flanagan, S. N. Freund, and S. Qadeer. Thread-modular veriﬁcation for sharedmemory programs. In ESOP, volume 2305 of LNCS, pages 262–277. Springer, 2002.
20. C. Flanagan and S. Qadeer. Thread-modular model checking. In SPIN, volume
2648 of LNCS, pages 213–224. Springer, 2003.

21. M. Fortin, A. Muscholl, and I. Walukiewicz. Model-checking linear-time properties
of parametrized asynchronous shared-memory pushdown systems. In CAV, volume
10427 of LNCS, pages 155–175. Springer, 2017.
22. L. Fortnow and R. Santhanam. Infeasibility of instance compression and succinct
PCPs for NP. JCSS, 77(1):91–106, 2011.
23. F. Furbach, R. Meyer, K. Schneider, and M. Senftleben. Memory model-aware
testing - A uniﬁed complexity analysis. In ACSD, pages 92–101. IEEE, 2014.
24. P. B. Gibbons and E. Korach. Testing shared memories. SIAM J. Comput.,
26(4):1208–1244, 1997.
25. A. Gotsman, J. Berdine, B. Cook, and M. Sagiv. Thread-modular shape analysis.
In PLDI, pages 266–277. ACM, 2007.
26. M. Hague. Parameterised pushdown systems with non-atomic writes. In FSTTCS,
volume 13 of LIPIcs, pages 457–468. Schloss Dagstuhl, 2011.
27. M. Hague and A. W. Lin. Synchronisation- and reversal-bounded analysis of multithreaded programs with counters. In CAV, volume 7358 of LNCS, pages 260–276.
Springer, 2012.
28. L. Holı́k, R. Meyer, T. Vojnar, and S. Wolﬀ. Eﬀect summaries for thread-modular
analysis - sound analysis despite an unsound heuristic. In SAS, volume 10422 of
LNCS, pages 169–191. Springer, 2017.
29. R. Impagliazzo and R. Paturi. On the complexity of k-sat. JCSS, 62(2):367–375,
2001.
30. V. Kahlon. Parameterization as abstraction: A tractable approach to the dataﬂow
analysis of concurrent programs. In LICS, pages 181–192. IEEE, 2008.
31. S. La Torre, P. Madhusudan, and G. Parlato. Model-checking parameterized concurrent programs using linear interfaces. In CAV, volume 6174 of LNCS, pages
629–644. Springer, 2010.
32. D. Lokshtanov, D. Marx, and S. Saurabh. Slightly superexponential parameterized
problems. In SODA, pages 760–776. SIAM, 2011.
33. S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software.
In TACAS, volume 3440 of LNCS, pages 93–107. Springer, 2005.
34. T. Wareham. The parameterized complexity of intersection and composition operations on sets of ﬁnite-state automata. In CIAA, volume 2088 of LNCS, pages
302–310. Springer, 2000.
35. C. K. Yap. Some consequences of non-uniform conditions on uniform classes. TCS,
26:287–300, 1983.

A

Proofs for Section 3

W[1]-hardness of LCR(D) and LCR(L)
We prove the W[1]-hardness of LCR(D) and LCR(L). Both results rely on a reduction from k-Clique, the problem of finding a clique of size k in a given graph. It is
known that k-Clique is W[1]-complete [12]. After reducing it to our problems via
a parameterized reduction, we can state that LCR(D) and LCR(L) are W[1]-hard.
The correct notion of a reduction in parameterized complexity are parameterized reductions. Given parameterized problems L, L′ ⊆ Σ ∗ × N, we say that L is
reducible to L′ via a parameterized reduction if there is an algorithm that transforms an input (x, k) to an input (x′ , k ′ ) in time g(k) · nO(1) so that (x, k) ∈ L
if and only if (x′ , k ′ ) ∈ L′ . Here, g is a computable function and k ′ is computed
by a function only dependent on k.
Proposition 15. Both parameterizations, LCR(D) and LCR(L), are W[1]-hard.
We first reduce k-Clique to LCR(L) and elaborate on the idea of the reduction. Technically, we construct from an instance (G, k) of k-Clique an instance
(A = (D , a0 , (PL , PC )), FL ) of LCR with L = O(k).
In the required program A, we operate in three phases. In the first phase (the
selection phase), the leader chooses randomly k vertices of the graph and writes
them to the memory. More precise, it writes a sequence (v1 , 1).(v2 , 2) . . . (vk , k)
with vi vertices of G. During this phase, the contributors non-deterministically
choose to store a suggested vertex (vi , i) in their state space.
In the second phase, the leader again writes a sequence of vertices using
different symbols: (w1# , 1)(w2# , 2) . . . (wk# , k). Note that the vertices wi do not
have to coincide with the vertices from the selection phase. It is then the contributor’s task to verify the sequence. To this end, each of the contributors
reads all values (wi# , i) in the sequence. More precise, for each i, the program
does the following: If a contributor, storing (vi , i) reads the value (wi# , i), the
computation on the contributor can only continue if wi = vi . If a contributor,
storing (vj , j) with j 6= i reads (wi# , i), the computation can only continue if
vj 6= wi (we select distinct vertices) and if there is an edge between vj and wi
(we select adjacent vertices).
Finally, in the third phase, we need to ensure that there was at least one
contributor storing (vi , i) and that the above checks were all positive. To this
end, a contributor that has successfully gone through the second phase and
stores (vi , i), writes the symbol #i to the memory. The leader pends to read the
sequence #1 . . . #k . This ensures the selection of k different vertices with each
two sharing an edge.
Note that the number of states of PL is linear in k, L = O(k). This means that
the parameter L of the constructed instance only depends on the parameter k of
the given instance. Hence, the reduction is indeed a parameterized reduction.

Formal Construction We denote by V the vertices of G and by E the edges.
Set the data domain D = {(v, i), (v # , i), #i | v ∈ V, i ∈ [1..k]} ∪ {a0 }. The
leader PL is given by the tuple PL = (Op(D ), QL , q 0 , δL ) with set of states
i
QL = {qVi , qVi # , q#
| i ∈ [1..k]} ∪ {q 0 }. The transition relation δL is defined by
the following rules. (First Phase) For each i ∈ [1..k] and v ∈ V , we add the
!(v,i)

rule qVi−1 −−−→L qVi . We identify the vertex qV0 by q 0 . (Second Phase) For each
!(v # ,i)

i ∈ [1..k] and v ∈ V , we add qVi−1
−−−→L qVi # . Here, we denote by qV0 # the
# −
?#i

i−1
i
vertex qVk . (Third Phase) For each i ∈ [1..k], add q#
−−→L q#
. Here, we assume
0
k
k
q# = qV # . Further, we set FL = {q# } to be the final state of interest.
0
The contributor is defined by PC = (Op(D ), QC , qC
, δC ). The states are
j
f
0
given by QC = {q(v,i) | i ∈ [1..k], j ∈ [0..k]} ∪ {qC , qC }. We define the transition
relation by the following rules. (First Phase) For each i ∈ [1..k] and v ∈ V we
?(v,i)

0
0
have qC
−−−→C q(v,i)
. (Second Phase) For i ∈ [1..k], j ∈ [0..k] and v, w ∈ V we
?(w,j)

j
j−1
if (1) j = i and v = w, or if (2) i 6= j, v 6= w, and there
have q(v,i)
−−−−→C q(v,i)
is an edge between v and w in E. (Third Phase) For any i ∈ [1..k] and v ∈ V ,
!#i

f
k
add the rule q(v,i)
−−→C qC
. The correctness is shown in the next lemma.

Lemma 16. There is a t ∈ N so that c0 →∗At c with c ∈ C f if and only if there
is a clique of size k in G.
Proof. We first assume that G contains a clique of size k. Let it be the vertices
v1 , . . . , vk . We construct a computation on At with t = k that leads from c0
to a configuration c in C f . The program contains k contributors, denoted by
P1 , . . . , Pk . We proceed in three phases, as described above.
In the first phase, the leader writes the values (v1 , 1), . . . , (vk , k) to the memory. Contributor Pi reads value (vi , i) and stores it in its state space. We get:
!(v1 ,1)

0
0
c0 −−−−→L (qV1 , qC
, . . . , qC
, (v1 , 1))
?(v1 ,1)

0
0
0
, qC
, . . . , qC
, (v1 , 1))
−−−−→1 (qV1 , q(v
1 ,1)
!(v2 ,2)

0
0
0
−−−−→L (qV2 , q(v
, qC
, . . . , qC
, (v2 , 2))
1 ,1)
?(v2 ,2)

0
0
0
0
, qC
, . . . , qC
, (v2 , 2))
, q(v
−−−−→2 (qV2 , q(v
2 ,2)
1 ,1)
?(vk ,k)

0
0
, (vk , k)) = c0 .
, . . . , q(v
. . . −−−−→k (qVk , q(v
1 ,1)
k ,k)

After reaching c0 , the leader starts the second phase. It writes (v1# , 1) and each
contributor reads it:
!(v # ,1)

1
0
0
−→L (qV1 # , q(v
, . . . , q(v
, (v1# , 1))
c0 −−−
1 ,1)
k ,k)

?(v # ,1)

0
0
1
, (v1# , 1))
, . . . , q(v
, q(v
−−−1−−→1 (qV1 # , q(v
2 ,2)
1 ,1)
k ,k)
?(v # ,1)

1
1
, (v1# , 1)) = c1 .
, . . . , q(v
. . . −−−1−−→k (qV1 # , q(v
1 ,1)
k ,k)

Note that P1 can read (v1# , 1) and move since it stores exactly (v1 , 1). Any Pi
with i 6= 1 can read (v1# , 1) and continue its computation since vi 6= v1 and
the two vertices share an edge. Similarly, one can continue the computation:
k
k
c1 →∗At ck = (qVk # , q(v
, . . . , q(v
, (vk# , k)).
1 ,1)
k ,k)
In the third phase, contributor Pi writes the symbol #i to the memory. The
leader waits to read the complete string #1 . . . #k . This yields the following
computation:
!#1

f
k
k
, #1 )
, . . . , q(v
ck −−→1 (qVk # , qC
, q(v
2 ,2)
k ,k)
?#1

f
k
1
k
, #1 )
, . . . , q(v
−−→L (q#
, qC
, q(v
2 ,2)
k ,k)
?#k

f
f
k
. . . −−→L (q#
, qC
, . . . , qC
, #k ) ∈ C f .

For the other direction, let a t ∈ N and a computation ρ = c0 →∗At c with
c ∈ C f be given. We denote by ρL the part of the computation that is carried
out by the leader PL . Then we can factor ρL into ρL = ρ1 .ρ2 .ρ3 with
!(v1 ,1)

!(v2 ,2)

!(vk ,k)

ρ1 = q 0 −−−−→L qV1 −−−−→L . . . −−−−→L qVk ,
!(w # ,1)

!(w # ,k)

!(w # ,2)

ρ2 = qVk −−−1−−→L qV1 # −−−2−−→L . . . −−−k−−→L qVk # ,
?#1

?#2

?#k

1
k
ρ3 = qVk # −−→L q#
−−→L . . . −−→L q#
.

We show that wi = vi for any i ∈ [1..k] and that vi 6= vj for i 6= j. Furthermore,
we prove that each two vertices vi , vj share an edge. Hence, v1 , . . . , vk form a
clique of size k in G.
Since PL is able to read the symbols #1 , . . . , #k in ρ3 , there are at least k
contributors writing them. But a contributor can only write #i in its computation if it reads (and stores) the symbol (vi , i) from ρ1 . Hence, there is at least
one contributor storing (vi , i). We denote it by Pvi .
The computation ρ2 starts by writing (w1# , 1) to the memory. The contributors Pvi have to read it in order to reach a state where they can write the symbol
#i . Hence, Pv1 reads (w1# , 1). By the definition of the transition relation of Pv1 ,
this means that w1 = v1 . Now let Pvi with i 6= 1. This contributor also reads
(w1# , 1) = (v1# , 1). By definition this implies that vi 6= v1 and the two vertices
share an edge.
By induction, we get that wi# = vi , the vi are distinct and each two of the
vi share an edge.
⊓
⊔
To prove the W[1]-hardness of LCR(D), let us consider the size of the data
domain in the above construction: It is |V | · k, where V is the set of vertices
of G. The factor |V | appears since leader and contributors communicate on the
pure vertices. But we can overcome this by transmitting the vertices in binary.
Let t = log(|V |) and bin : V → {0, 1}t be a binary encoding of the vertices.
Instead of a single symbol (v, i) with v ∈ V and i ∈ [1..k], the leader will write
a string #.(α1 , i).#.(α2 , i).# . . . (αt , i).# to the memory, where t = log(|V |),

α1 .α2 . . . αt = bin(v), and # is a special padding symbol. We need the padding
in order to prevent the contributors from reading a symbol (αj , i) multiple times.
Note that the new data domain contains only O(k) many symbols.
The idea of the program over the changed data domain is similar to the
idea above: It proceeds in three phases. In the first phase, the leader chooses
the vertices of a clique candidate. This is done by repeatedly writing a string
#.(α1 , i).#.(α2 , i).# . . . (αt , i).# to the memory, for each i ∈ [1..k]. Like above,
the contributors non-deterministically decide to store a written vertex. To this
end, a contributor that wants to store the i-th suggested vertex has a binary
tree branching on the symbols (0, i) and (1, i). Leaves of the tree correspond
to binary encodings of vertices. Hence, a particular vertex can be stored in the
contributor’s states. Note, as we did not assume |V | to the a power of 2, there
might be leaves of the tree that do not correspond to encodings of vertices. If a
computation reaches such a leaf it will deadlock.
In the second phase, the leader again writes the binary encoding of k vertices
to the memory. But this time, it uses a different set of symbols: Instead of 0
and 1, the leader uses 0# and 1# to separate Phase two from Phase one. The
contributors need to compare the suggested vertices as in the above construction.
To this end, a contributor storing the vertex (v, i) proceeds in k stages. In stage
j 6= k it can only read the encodings of those vertices which are connected to v.
Hence, if the leader suggests a wrong vertex, the computation will deadlock. In
stage i, the contributor can only read the encoding of the stored vertex v. This
allows a verification of the clique as above.
The last phase is identical to the last phase of the above construction. The
contributors write the symbols #i , while the leader waits to read the string
#1 . . . #k . This constitutes a proper clique. The formal construction and proof
are omitted as they are quite similar to the above case.
Proof of Lemma 4
Proof. For the ⇒ direction, we will assume that there is a t ∈ N such that
π = c0 →∗At c, c ∈ C f .w.l.o.g, we will assume that the last move in this run is
by the leader. Let σ be the sequence of transitions that appear in this run. We
will show how to construct the required valid witness string from σ.
We iterate through the transitions that appear in σ and mark the very first
write transition that belongs to the contributor. Inductively, we mark the next
write transition that belongs to the contributor if it writes a value that is different
from the values appearing in the previously marked transitions. We repeat this
process till we cannot mark any more transitions. Notice that the number of
such marked transitions are at-most D. We now delete all the transitions of the
contributor that are not marked. For each of the marked transitions, if it is of
the form (q, !a, q ′ ), then we replace is by ā. Notice that the resulting sequence
looks like σ1 c̄1 σ2 c̄2 . . . c̄n σn+1 .
Now for each of the subsequence σ1 , . . . , σn we do the following. We iterate through the transitions from left to right. For any such transition of
the form (q, a, q ′ ) we identify the longest non-trivial sub-sequence of the form

(q, a, q ′ ) . . . (q ′′ , b, q) and delete it. If there is no such sub-sequence, we move on to
the next transition. The resulting string σi′ obtained after such an operation will
be of size at-most L. If the starting transition of σn+1 is of the form (q, op, q ′ ),
we simply replace it by q. In the resulting string, all other transitions of the form
(q, !a, q ′ ) are replaced by qa and transitions of the form (q, ǫ, q ′ ) and (q, ?a, q ′ )
are replaced by q⊥. The resulting string is clearly a witness-string. We still need
to prove that it satisfies the validity-properties.
Notice that the property-1 is satisfied because of the way we marked the
contributors transitions. We do not mark the same value written by contributor
twice.
The property 2 is satisfied since we started with a valid run that reaches a
final state of the leader. From this we replaced the last segment σn+1 by the
first state appearing in this segment. Since σn+1 reached the final state, there
is a run from such a state to the final state. Also notice that we only deleted
transition sequences from a state that reached the same state. This amounts to
finding a shorter run. From this we can conclude that the adjacent states are
associated by a transition.
Property 3 is satisfied since for every write transition, the set of values read is
either from the witness string ( which is guaranteed to be written by the leader)
or the part that was shrunk ( which is guaranteed to be part of the loop in the
leader) or a write of value from a contributor whose value was already marked.
Now using these we can easily construct the required mapping as follows. The
required contributor run is simply the run of the contributor till the first write
in π. For any value that is written by leader, which was not shrunk, we map
such a position to its corresponding write in the witness string. If the value read
was from a write in a loop, we simple map such a position to the state in the
witness string where the loop appeared. Finally if it was a value written by a
contributor, then clearly such a value appears in the witness string as a barred
symbol. We find a position in the witness string after such a barred symbol that
has a state, such that the monotonicity is maintained. Notice that the transition
of the contributor in the run π clearly appears after the position associated with
the barred symbol and hence such a position that maintains monotonicity can
always be found.
For the ⇐ direction, we will assume a valid witness string w and show that
there is a t such that c0 →∗At c for some c ∈ C f . Firstly let w ↓D̄ = c1 . . . cn , by
property 1 it is clear that there are no repetitions in this sequence. Further from
property 2 we get a sequence of transitions of the form σ1 , . . . σn+1 such that
0 σ=σ1 σ2 ...σn+1
qL
−−−−−−−−−→ q f for some q f ∈ QfL .
Furthermore, corresponding to each ci , because of property 3 we have a
!ci
ui
qn+1 and a mapping µi . Let u′i be a
qn −→
computation of the form πi = qc0 −→
sequence of values read by the contributor (i.e. values obtained by disregarding
writes and ǫ moves). Further let ρi = σ1 . . . σ|u′i | be a partition of the sequence
of transitions in the run πi , where σ1 is the sequence of transitions up to the
first read, σ2 is the sequence up to the second read and so on.

We now compute (over approximate) the total number of contributor processes that will be required. Notice that each value ci written by the contributor can either be read by the leader or other contributors. We claim that we
need at most tci = L × (|u′1 | + · · · + |u′n |) + |σ| many processes for each ci . Let
t = tc1 + tc2 + · · · + tcn . We will explain the significance of such a number as we
proceed.
The run that we wish to construct starts from the initial configuration c0 ,
the run is constructed inductively. During the construction, we will employ the
variables x1 , . . . , xn which are initialised to zero in the beginning. These variables
will be used to index into the strings u′i and ρi . Similarly we will also employ
another variable x that will index into the string w.
Note that we start with t many contributors, we will use tci many for each
value ci . We will partition these contributors according to the value they will be
producing. We will refer to the set of contributors that will be generating value
ci by Sci . The size of each Sci initially will be tci . Given any configuration c in
τ
At , we will use c −
→Sci c′ to mean that all processes in the set Sci executes the
process τ and moves to the next state. We extend this definition to a sequence of
transitions σ. Similarly we will use c Sci c′ to mean exactly one of the process
in Sci writes the value ci onto the shared memory and such a process is removed
from Sci .
The run that we will inductively construct will maintain the following invariants.
1. If w[x] = c̄i , then we require that set of all processes in Sci have executed
ρi and all of them can write to shared memory the value ci . This is ensured
by maintaining the invariant for all i, µi (xi ) ≥ x or xi = |ui |.
2. The number of processes in Sci needs to be adequate for rest of the computation. This is ensured by maintaining the invariant |Sci | ≥ (k1 + · · · +
kn ).|QL | + k, where ki = |ui | = xi , k = |σ| − x.
3. For each ci , all processes in Sci are in the same state.
We now describe the inductive procedure for constructing the run. For this we
will assume already constructed run of the form c0 →∗At c for some x, x1 , . . . xn
and show how to extend such a run to c0 →∗At c →∗At c′ for new values of the
variables of the form x + 1, x′1 , . . . x′n with xi ≤ x′i for all i ∈ [1..n].
– Suppose w[x] ∈ {⊥} then if the corresponding move is an epsilon move,
the required run is obtained by performing such an operation and x is incremented by 1. Suppose the move that reads ci from a contributor, then
!c
we perform first a c i c1 and then perform the required read operation
and increment x. Notice that we remove atmost one process from Sci but
increment x, this would decreasr k atleast by one, ensuring invariant 2 is
maintained. Invariant 3 is maintained since
removes the contributor that
moved from Sci .
– Suppose w[x] = a ∈ D , then we first execute the transition in σ that writes
!a
such an a to the shared memory i.e. extend the run as c0 →∗At c −→ c1 . Then

σx

i
for each i ∈ [1..n] suppose µi (xi ) = x, we extend the run as c0 →∗At c1 −−→
Si
c2 and increment xi . We do this operation until no more µi (xi ) = x. Finally,
we increment x by 1. The invariant 1 is satisfied since µi given to us is
guaranteed to be monotonic. Invariant 2 is satisfied since we do not use
and the invariant 3 is satisfied since we make the same moves (or no move)
for all the processes in Sci
– Suppose w[x] = c̄i then clearly xi = |ui | (this is because µi maps positions
of ui to positions in w that occur before the first appearance of c̄i ), this also
means that all the states in Sci have executed ρi and hence are in a state

from where they can execute !ci . We extend the run as follows c0 →∗At c

!ci

?c

i
c′ and increment x. Notice that we have reduced size of Sci by atmost
c1 −−→
1 and incremented x by 1 and hence invariant 2 is maintained.
– Suppose w[x] = q ∈ QL , this is the most complicated case. For each i ∈ [1..n],
suppose µi (xi ) = x then we know that ui [xi ] ∈ Loop(q, D̄ (w, x)) or it reads
a value written by a contributor. If the value is written by a contributor, we
perform the appropriate
followed by the sequence σxi for all the processes
in Sci and increment xi . Otherwise, we also know that there is a loop in PL
that satisfies such a read request by the contributor. Since µi (xi ) = x, clearly
xi < |ui | from this we know that there are atleast L many contributors in
each Scj , j ∈ [1..n], to execute such a loop we need atmost |QL | many of
them. Now we extend the required run as follows for each µi (xi ) = x, we

v!a

σx

v′

i
→ c′ where v!av ′ is the loop to
perform c0 (t) →∗At c −−→ c1 −−→
S ci c 2 −
be executed. After such an operation, we increment xi by 1. We perform
this operation till no more µi (xi ) = x. Notice that invariant 2 is satisfied
since we use up at-most L many contributor writes but also increment xi
each time. The invariant 3 is maintained since each time we move all the
processes through a −
→Sci move.

Now the required run is obtained by iterating the above procedure till x = |w|.
This completes the proof
⊓
⊔
Proof of Lemma 5
Proof. It is clear that Property (1) can be checked in time O(L · D).
We claim that Property (2) can be tested in time O(L3 · D2 ). To this end, we
check for every adjacent pair of states q, q ′ and letter a ∈ D between them if
there is a transition of type (q, !a, q ′ ) ∈ δL . Similarly if ⊥ is the symbol between
q and q ′ . Then we look for a transition (q, ǫ, q ′ ) or (q, ?ci , q ′ ) for an i. Each such
transition can be found in time |δL | ≤ L2 · D. Finally, checking whether there is
a run from the last state of w to a state in FL , can be decided in time O(L2 ), as
it is just a reachability query on an NFA.
Property (3) can be checked in time O(C2 · L3 · D2 ). We reduce to reachability
in a finite state automata N constructed as follows. The states of N are given
0
by QN = QC × [1..|v|] ∪ {f }. The initial state is (qC
, 1).

We set up the transition relation: For all (q, !a, q ′ ) ∈ δC , we add the transitions (q, i) →N (q ′ , i). For each read transitions (q, ?a, q ′ ) ∈ δC and state (q, i),
we add the transition (q, i) →N (q ′ , i) if one of the following three options hold:
If v[i] = a. If v[i] = p ∈ QL and a ∈ Loop(p, D̄(w, i)). If a ∈ D̄ (w, i). Further, we add (q, i) →N (q, i + 1). Finally, for all states (q, i) in N such that
(q, !cj , q ′ ) ∈ δC , we add the transition (q, i) →N f . This ends the computation
since cj was written.
Now we have that Property (3) is satisfied if and only if there is a computation
0
(qC
, 1) →∗N f . The construction of N is the dominant factor and takes time
O(C2 · L3 · D2 ).
If we now combine the three results, we get that validity can be tested in
time O(L3 · D 2 · C 2 ).
⊓
⊔
Formal Definition of SCC-witness Candidates and Validity
We give a formal definition of SCC-witness candidates. Let
r = c̄1 . . . c̄ℓ ∈ V. We denote by C(r) the set of all strings in
kℓ
k0
such
(SCC(P
PL ↓0 ).(D ∪ {⊥})) .c̄1 . . . c̄ℓ .(SCC(PL ↓ℓ ).(D ∪ {⊥})) .(SCC(PL ↓ℓ )
ki ≤ d − 1. The set of SCC-witness candidates is the union
that
i∈[0..ℓ]
S
C = r∈V C(r). A SCC-witness candidate w ∈ C is called valid if it satisfies the
following properties:
1. The sequence in w without the barred symbol induces a valid run in the
leader. For this we need to find appropriate entry and exit states in each SCC
such that the exit state of each SCC is connected to its adjacent SCC through
a transition. Let v = scc11 a11 . . . scc1k1 a1k1 scc21 a21 . . . scc2k2 a2k2 . . . scc1ℓ be the
sequence obtained by projecting out the barred symbols. Further for any
symbol α appearing in v, let pos(α) denote the position of α in v. For any
i ∈ [1..|v|], We will also use D̄ (v, i) to refer the the set of all barred symbols
appearing before the position i: D̄ (v, i) = {a | ā appears in v[1..i]}. Now
corresponding to any sub-sequence of v of the form scc1 ascc2 that appears
in v, one of the following is true.
– If a ∈ D , then we can find states q ∈ scc1 , q ′ ∈ scc2 such that there is
a
a transition of the form q −
→ q ′ in PL .
– If a = ⊥ then, then we can find states q ∈ scc1 , q ′ ∈ scc2 such that there
ǫ/?c

is a transition of the form q −−−→ q ′ in PL for some c ∈ D̄ (v, pos(a)).
0
We also require that qL
∈ scc11 . Finally we require that from any state q in
1
the final scc sccℓ , a run to the final state only involving writes, internal or a
σ
read of the barred symbol occurring in w. That is a run of the form q −
→ qf
such that σ ∈ (W (D ) ∪ R(D̄ (v, |v|)))∗ .
2. We can construct supportive computations on the contributors. For each
0 u!a
prefix vā of w with ā ∈ D̄ there is a computation qC
−−→C q on PC to some
q ∈ QC such that the reads within u can be obtained from w. Formally, let
u′ = u ↓R(D) . Then there is an embedding of u′ into v, a map µ : [1..|u′ |] →
[1..|v|] with µ(i) ≤ µ(j) for i < j and v[µ(i)] ∈
/ D̄ ∪ {⊥}. Hence, u′ is

U
only mapped to elements from i∈[0..ℓ] SCC(PL ↓i ) ∪ D . Let u′ [i] =?a with
a ∈ D . Then either v[µ(i)] = a, which corresponds to a write of a by PL ,
or v[µ(i)] = scc ∈ SCC(PL ↓i ) for some i ∈ [0..ℓ]. In the latter case, we
have a ∈ D (scc), this corresponds to the letter being a write by the leader
through the scc or write of a value by a contributor that was already seen.
3. Let w be of the form v1 c̄1 v2 c̄2 . . . vℓ c̄ℓ scc1ℓ , then the scc dont repeat in each
of v1 , v2 . . . vℓ .
We refer to the above Properties as (SCC) validity. Instead of stating a
characterization of computations in terms of SCC-witnesses directly, we relate
the SCC-witnesses to the witnesses as defined in Section 3.1.
Lemma 17. There is a valid SSC-witness candidate in C if and only if there is
a valid witness candidate in E.
Proof. First we will prove the ⇒ direction. For this, we will assume a valid
witness string w ∈ E. Further let w = v0 c̄1 v1 c̄2 . . . vk−1 c̄k q. Now consider the
decomposition (vi′ = scci1 . . . scciki ) of each vi according to their SCC in PL ↓i .
This we do by taking the maximum subsequence and replace it with the SCC to
which it belongs. We can be sure that none of the SCC in this sequence repeats
(otherwise they will already form a bigger SCC). Secondly notice that such a
SCC sequence will be a path in the SCC graph G(PL , c̄1 c̄2 . . . c̄k ). This implies
that the decomposition thus obtained is a scc-witness. However we need it to be
a valid scc-witness. The fact that such a scc-witness satisfies property-1 of the
scc-validity property follows from the fact that we started with a valid-witness
that satisfies property-2 of the validity-property, this already provides us with
the requires states in the adjacent scc and a transition relation between them.
Proving property-2 of the scc-validity is slightly more complicated. For this,
we need to construct a run in the contributor for each prefix that ends in a
barred symbol and show that there is an appropriate mapping from this run
to the scc-witness string. But notice that since we started with a valid-witness
string, we are guaranteed a computation in the contributor and a mapping from
such a run into the witness string. For this, let us fix one such prefix to be
u·!c
α′ c̄j . Let the corresponding prefix of w be αc̄j . Let qc0 −−→ q be such a run and
′
′
′
µ : [1..|u |] 7→ [1..|α |] (where u is obtained from u by deleting all the values that
do not correspond to a read transition) be the corresponding mapping. We construct from this mapping, another mapping µ′ : [1..|u′ |] 7→ [1..|α|]. Observe that
α = v0 c̄1 v1 c̄2 v2 . . . c̄j , let α′ = v0′ c̄1 v1′ c̄2 v2′ . . . c̄j , where vi′ are the corresponding
decomposition of vi into SCC. The required mapping µ′ is constructed as follows.
Suppose the original mapping µ mapped a value in [1..|u|] to a state or letter
that got replaced by an SCC then we let µ′ to map such a position to the SCC that
replaced the state. If the original mapping mapped the position in [1..|u′ |] to a
letter that survied, then we also let µ′ to do the same. That is, suppose for some
vi = q1 a1 . . . qk ak if its corresponding decomposition be scc1 ai1 . . . sccj ak and
µ(i) = j, where j is a position into the string vi . If j points to one of ai1 . . . ak
(the letters that survived the decomposition), then we let µ′ (i) = j ′ , where j ′

is the position of such a letter in α′ . If j points to a state or a letter in D that
was decomposed into scci , then µ′ (i) gets the value of the position of scci in α′ .
The correctness of such a mapping follows from the following reasoning. Clearly
µ′ thus constructed is monotonic since µ already was. Suppose µ′ maps a position in u′ to a letter, such a letter is guaranteed to be the same since it was
the same for the mapping µ. Suppose µ mapped a position in u′ to a letter a
that got decomposed into scci , then clearly a ∈ D (scci ). Suppose µ mapped a
position i in u′ to a state q that got decomposed into scci , we observe that for
any a ∈ Loop(q, D̄ (w, µ(i))), we also have a ∈ D (scci ). With this, we get the
result for one direction of the proof.
For the (⇐) direction, we will assume a valid scc-witness w and
show how to construct a valid witness from this. Let w be of the
form scc11 a11 . . . scc1k1 a1k1 c̄1 scc21 a21 . . . scc2k2 a2k2 c̄2 . . . c̄ℓ scc1ℓ . From the scc-validity
0
property-1, we have qL
∈ scc11 . Further for every subsequence of the form
scc1 ascc2 , we have the states q1 ∈ scc1 and q2 ∈ scc2 such that there is
b
→ q2 , where b is either ǫ/!c or in ?a dependa transition of the form q1 −
ing on the type of a. We will call the state q1 the exit state of scc1 and q2
the entry state of scc2 . From this, corresponding to each sccij , there are entry and exit states enij , exij . In each such scc, corresponding to its entry and
exit states, there is also a shortest path between them. That is, corresponding to scc of the form sccij ∈ SCC(PL ↓i ) there is a shortest path of the form
a

(i,j) a

(i,j)

a

(i,j)

(i,j)

(i,j) ak+1

2
1
k
enij −→
−−−→PL↓i exij . To get the valid
. . . −→
−→
PL↓i qk
PL↓i q2
PL↓i q1
witness string, we replace each scc in the valid scc-witness by its shortest path
as follows. There is one exception to this replacement, the final scc occuring in
the scc-witness is simply replaced by its entry state. The scc sccij is replaced by

a string of the form enij b1 q1 b2 q2 . . . exij , where bi = a if ai =!a and bi = ⊥
otherwise. Let w′ = v0 c̄1 v1 c̄2 . . . c̄ℓ qℓ be the string thus obtained. Notice that in
each vi , none of the states repeat, this is because none of the SCC repeats in w
and SCC partitions the state space. We still need to show that the string thus
obtained satisfies the validity properties.
Property-1 of validity is satisfied since all the barred symbols in valid sccwitness do not repeat. Property-2 is satisfied because between any adjacent SCC
in w, there is a valid move by definition. Further the way we constructed the
valid witness, we replaced each scc in the scc-witness by a valid shortest path
in that scc. Finally, by definition there is also a run to final state from any state
in the final scc .
Finally we need to prove that property-3 of validity holds. For this, we need
to show existence of an appropriate computation in the contributor along with
a mapping to the witness string for every prefix of w′ such that the prefix ends
in a barred symbol. Let us fix one such prefix to be σ = v0 c̄1 . . . vj c̄j+1 , let the
corresponding prefix in w be σ ′ = v0′ c̄1 . . . vj′ c̄j+1 . From the scc-validity property,
u·!cj+1

we already have a computation of the form qc0 −−−−→ q and a mapping µ from
positions of u′ (u′ is the projection of u onto only read operation) to positions in
σ ′ . We provide a mapping from the positions in u′ to positions in σ as follows.

If µ maps a position to a symbol in D , then µ′ maps such a position to the
corresponding position of the same letter in σ ′ . Otherwise, the position is mapped
to the first state of the shortest path of the corresponding SCC. If a letter is in
D (scc), then one can always find a loop that visits such a letter. Hence such a
mapping satisfies the validity property.
⊓
⊔
As above, the algorithm iterates over all SCC-witness candidates and each is
tested to be valid. The validity check can be performed in polynomial time, as
shown in the below lemma.
Lemma 18. Validity of w ∈ C can be checked in time O(L2 · D · C 2 · d2 ).
Proof. Checking whether a SCC-witness candidate w satisfies Property (1) can
be tested in time O(d ·L2 ·D). For this, between any two SCC in w of the form the
scc1 ascc2 , we need to check if there are states q1 ∈ scc1 and q2 ∈ scc2 such that
q1 → q2 . This can easily be done in time O(|δL |) ≤ O(L2 · D). This operation, we
need to perform between every pair of adjacent SCC, there are at most d many
such adjacent pairs. Hence overall the time required to check whether there are
proper transitions between each scc is O(d · L2 · D) Checking whether there is a
path from the final SCC to the final state reduces to reachability in an automata
and can be easily done in time O(L2 ).
Property (2) can be tested in time O(d2 · L2 · D · C2 ). This can be achieved
by reducing the problem to reachability in a NFA. The idea is similar to the one
we saw in proof of lemma-5. The automaton we construct will have the states of
the contributor and an index into the given witness string.
For constructing this automaton, we need to check for any given scc and a
letter a ∈ D , whether a ∈ D (scc). This can easily be achieved in time O(L2 ) by
reducing it to reachability problem in a graph. We add a transition of the form
?a
(c1 , i) −
→ (c2 , i) if there is a transition of the form c1 −→PC c2 , i refers to scc in
w and a ∈ scc. So for each i, we go through each transition in δC and perform
the scc-check. This takes time O(d · C2 · D · L2 ).
Finally, the size of such an automaton is simply O(C × d) and we need to
perform a reachability check which is quadratic and hence in O(C2 × d2 ) . From
this, we get the required complexity.
Finally, it is obvious that Property (3) can be checked in time O(d). This
completes the proof.
⊓
⊔
Comparison between introduced Methods
Compared to the formerly introduced witnesses, there are less candidates to test.
We have that WitSCC (s, D, d) ≤ Wit (L, D).
Lemma 19. WitSCC (s, D, d) ≤ Wit (L, D).
Proof. For this, we show how to construct an injective function from every string
in WitSCC (s, D, d) to strings in Wit (L, D). This would already give us the result. The idea here is to represent each scc by an unique state present in that

scc. For this, we will assume an arbitrary ordering on the states of the leader
QL . Recall that the scc partitions the states space of the leader, hence for any
scc1 , scc2 ∈ SCC(PL ↓i ), for some i we have scc1 ∩scc2 = ∅. Now given any string
w = scc11 a11 . . . scc1k1 a1k1 c̄1 scc21 a21 . . . scc2k2 a2k2 c̄2 . . . c̄ℓ scc1ℓ ∈ WitSCC (s, D, d), let
f (w) = v be obtained by replacing each sccij by the minimum state qji in that
scc. Since no two scc share a state, clearly v ∈ Wit (L, D). Quite clearly such a
mapping is injective since each of the replacing states uniquely represents the
scc.
⊓
⊔
A Bound on the Number of SCC-witness Candidates
We will here show that WitSCC (s, D, d) ≤ (s · (D + 1))d · DD · 2D+d . For this, we note
that for any w ∈ WitSCC (L, D, d), the size of such a string is bounded by 2d + D.
Further if we remove the last appearing SCC from w, all other SCC appearing
there has an letter from D ∪ {⊥} appearing next to it. Hence if we consider such
a pair as a single cell and the symbols from D̄ as a single cell, there are at-most
d + D many cells. Now if we fix the positions and the value of the barred symbols
in the sequence of cells, then each of the unoccupied cells (d many of them) have
d
at-most s · (D + 1) choices. Hence there
 are (s · (D + 1)) many such strings. Now
for any fixed v ∈ V, there are D+d
many
ways
to
pick
D positions from D + d
D
positions. This is upper bounded by 2D+d . Since we have DD many strings in V,
we get that WitSCC (s, D, d) ≤ (s · (D + 1))d · DD · 2D+d .
Formal Construction and Proof of Proposition 7
The domain of the memory is D = {row(i), col(i), #i | i ∈ [1..k]} ∪ {a0 }. The
0
contributor threads are defined by PC = (Op(D ), QC , qC
, δC ) with set of states
(r,ℓ) (c,ℓ′ )
f
′
0
}. Intuitively, we use
QC = {q(i,j) , q(i,j) | i, j, ℓ ∈ [1..k], ℓ ∈ [0..k]} ∪ {qC , qC
(r,ℓ)

(c,ℓ′ )

the states q(i,j) , q(i,j) to indicate that the contributor has chosen (i, j) to store
and to count the number of vertices that the contributor has read so far. More
(r,ℓ)
precise, the state q(i,j) reflects that the last symbol read was row(ℓ), the row
(c,ℓ)

of the ℓ-th vertex. The state q(i,j) indicates that the last read symbol was the
column-symbol belonging to the ℓ-th vertex. Note that this can be any column
and thus different from col(ℓ).
The transition relation δC is defined by the following rules. We have a rule
?a0

(c,0)

0
to choose a vertex: qC
−−→C q(i,j) for any i, j ∈ [1..k]. To read the ℓ-th row(c,ℓ−1) ? row(ℓ)

symbol, we have q(i,j)

(r,ℓ)

−−−−−→C q(i,j) for any ℓ ∈ [1..k]. For reading the ℓ-th
(r,ℓ)

col(j ′ )

(c,ℓ)

column-symbol, we get the transition q(i,j) −−−−→C q(i,j) , but only if one of
the following is satisfied: (1) We have that i 6= ℓ and there is an edge between
(ℓ, j ′ ) and (i, j) in G. Intuitively, the contributor stores a vertex (i, j) from a
row, different than ℓ. But then it can only continue its computation if (i, j) and
(ℓ, j ′ ) share an edge. (2) We have that i = ℓ and j ′ = j. This means that the

contributor stores the vertex that it has read. Note that with this, we rule out
all contributors storing other vertices from the i-th row.
(c,k) !#i

f
for
To end the computation in a contributor, we get the rule q(i,j) −−→C qC
any i, j ∈ [1..k]. The rule writes #i to the memory, reflecting the correctness of
the clique in row i.
0
The leader PL is given by the tuple PL = (Op(D ), QL , qL
, δL ) with set of
(r,i) (c,i) (#,i)
0
| i ∈ [1..k]} ∪ {qL }. Unlike for the contributor,
states QL = {qL , qL , qL
(r,i)
the state qL indicates that the last written symbol was row(i), the row of the
(c,i)
i-th vertex guessed by PL . State qL reflects that the last written symbol was
(#,i)
the column-symbol belonging to the i-th vertex. The remaining states qL
are
used to receive the verification symbols and count up to k.
The transition relation δL is described by the below rules. For transmit(c,i−1)

!row(i)

(r,i)

−−−−→L qL for i ∈ [1..k]. Note that
ting the row-symbols we have qL
(c,0)
0
we identify qL as qL . For writing the column-symbols we have the rules
(r,i) !col(j)

qL

(c,i)

−−−−→L qL

, where i, j ∈ [1..k]. After sending k row- and column-symbols,
(#,i−1) ?#i

(#,i)

we receive the symbols #i via the following transitions: qL
−−→L qL
for
(c,k)
(#,0)
the state qL .
i ∈ [1..k]. Here, we denote by qL
(#,k)
We further set FL = {qL }, the state after receiving all #-symbols. Then
our program is defined to be A = (D , a0 , (PL , PC )). Note that the parameters
are D = L = 3k + 1. The correctness of the construction is proven in the following
lemma.
Lemma 20. There is a t ∈ N so that c0 →∗At c with c ∈ C f if and only if there
is a clique of size k in G with one vertex from each row.
Proof. First assume that G contains the desired clique and let (1, j1 ), . . . , (k, jk )
be its vertices. For t = k we construct a computation from c0 to a configuration
in C f . We have k copies of the contributor PC in the system At . We shall denote
them by P1 , . . . , Pk .
The computation starts with Pi choosing the vertex (i, ji ) to
0
store, it performs the step qC
i

?a0

−−→i
(c,0)

(c,0)

q(i,ji ) . Hence, we get as a
(c,0)

0
computation on At : c0 →∗At (qL
, q(1,j1 ) , . . . , q(k,jk ) , a0 ) = c0 . Then PL
writes the symbol row(1) and each contributor reads it. We get
(r,1)
(r,1) (r,1)
c0 →∗At (qL , q(1,j1 ) , . . . , q(k,jk ) , row(1)) = c(r,1) . After transmitting the first
row to all contributors, PL then communicates the first column by writing
col(j1 ) to the memory. Again, each contributor reads it. Note that P1 can
read col(j1 ) since it stores exactly the vertex (1, j1 ). A contributor Pi with
i 6= k can also read col(j1 ) since Pi stores (i, ji ), a vertex which shares an
edge with (1, j1 ) due to the clique-assumption. Hence, we get the computation
(c,1)
(c,1) (c,1)
c(r,1) →∗At (qL , q(1,j1 ) , . . . , q(k,jk ) , col(j1 )) = c1 .
Similarly, we can construct a computation leading to a configuration c2 . By
(c,k)
(c,k) (c,k)
iterating this process, we get c0 →∗At ck = (qL , q(1,j1 ) , . . . , q(k,jk ) , col(jk )).

Then each contributor Pi can write the symbol #i . This is done in ascending
order: First, P1 writes #1 and PL reads it. Then, it is P2 ’s turn and it writes #2 .
Again, the leader reads the symbol. After k rounds, we reach the configuration
(#,k) f
f
, . . . , qC
, #k ) which lies in C f .
(qL , qC
1
k
Now let a t ∈ N together with a computation ρ = c0 →∗At c with c from C f
be given. Let ρL be the subcomputation of ρ carried out by PL . Technically, the
projection of ρ to PL . Then ρL has the form ρL = ρ1L .ρ2L with
! row(1)

ρ2L

=

(c,k) ?#1
qL −−→L

(c,1) ! row(2)

(r,1) ! col(j1 )

0
−−−−→L qL
ρ1L = qL

(#,1) ?#2
qL
−−→L

...

! col(jk )

(c,k)

−−−−→L . . . −−−−−→L qL

−−−−−→L qL

and

?#k

(#,k)
−−→L qL .

We show that the vertices (1, j1 ), . . . , (k, jk ) form a clique in G.
Since in ρ2L , the leader is able to read the symbols #1 up to #k , there must
be at least k contributors writing them. Due to the structure of PC , it is not
possible to write different #i symbols. Hence, we get one contributor for one
symbol and thus, t ≥ k.
Let PCi be a contributor writing #i . Then PCi stores the vertex (i, ji ), it
?a0

(c,0)

0
−−→i q(i,ji ) . Assume PCi stores the vertex (i′ , j ′ ).
performs the initial move qC
i
Since the thread writes #i in the end, we get i′ = i due to the structure of PCi .
(r,i)

? col(ji )

(c,i)

During the computation ρ, the thread performs the step q(i,j ′ ) −−−−−→i q(i,j ′ )
since PL writes the symbol col(ji ) to the memory and the computation on PCi
does not deadlock. Note that we use the following: The leader writes row(i) before
col(ji ). This ensures that col(ji ) is indeed the column of the i-th transmitted
vertex and the above transition is correct. However, the contributor PCi can only
do the transition if j ′ = ji . Thus, we get that (i′ , j ′ ) = (i, ji ).
Let P(i,ji ) denote a contributor that writes #i during ρ. Since the contributor
P(i,ji ) stores the vertex (i, ji ), the leader PL has written row(i) and col(ji ) to
the memory. Now let P(i′ ,ji′ ) be another contributor with i′ 6= i. Then also this
(r,i)

? col(ji )

(c,i)

thread needs to perform the step q(i′ ,j ′ ) −−−−−→i q(i′ ,j ′ ) since the computation
i
i
does not end on P(i′ ,ji′ ) at this point. But by definition, the transition can only
be carried out if there is an edge between (i, ji ) and (i′ , ji′ ). Hence, each two
vertices of (1, j1 ), . . . , (k, jk ) share an edge.
⊓
⊔
Formal Construction and Proof of Theorem 8
We define the polynomial equivalence relation R in more detail. Assume some
encoding of Boolean formulas over some finite alphabet Γ . Let F ⊆ Γ ∗ be the
encodings of proper 3-SAT-instances. We say that two encodings ϕ, ψ ∈ Γ ∗ are
equivalent under R if either ϕ, ψ ∈ F and the formulas have the same number
of clauses and variables or if ϕ, ψ are both not in F . Then R is a polynomial
equivalence relation.
We define D to be the union of the sets {(u, ℓ) | u ∈ {0, 1}, ℓ ∈ [1.. log(I)]},
{(xi , v) | i ∈ [1..n], v ∈ {0, 1}}, {#j | j ∈ [1..m]}, and {a0 }. Thus, we have that
D = O(log(I)+n+m), which does not exceed the bounds of a cross-composition.

(b,0)

The leader is defined by the tuple PL = (Op(D ), QL , qL , δL ) with set
(b,ℓ) (x,i) (#,j)
of states QL = {qL , qL , qL
| ℓ ∈ [0.. log(I)], i ∈ [1..n], j ∈ [1..m]}.
Hence, we have L = O(log(I) + n + m). The transition relation is defined by
the following rules: For transmitting the bits in the first phase, we have for each
(b,ℓ−1) !(u,ℓ)

(b,ℓ)

ℓ ∈ [1.. log(I)] the transition qL
−−−→L qL with u ∈ {0, 1}. For choosing
the evaluation of variables in the second phase, we have for i ∈ [1..n] the rule
(x,i−1) !(xi ,v)

(x,0)

(b,log(I))

(x,i)

to
by qL
−−−−→L qL with v ∈ {0, 1}. We denote the state qL
qL
connect the phases. In the third phase, PL wants to read the symbols #j . Thus,
(#,j−1) ?#j

(#,j)

we get for any j ∈ [1..m] the transition qL
−−→L qL
(x,n)
(#,0)
the state qL . We set FL = {q (#,m) }.
by qL

. Here we denote

ε
The contributor PC is defined by PC = (Op(D ), QC , qC
, δC ). The set of
states QC is the union of {q w | w ∈ {0, 1}≤log(I) }, {q (ch,ℓ) | ℓ ∈ [1..I]},
ℓ
and {q(x
| ℓ ∈ [1..I], i ∈ [1..n], v ∈ {0, 1}}. Intuitively, the states q w with
i ,v)
≤log(I)
w ∈ {0, 1}
form the nodes of the tree of the first phase. The remaining
states are needed to store the chosen instance, a variable, and its evaluation.

The transition relation δC contains rules for the three phases. In the first
phase, PC reads the bits chosen by the leader. According to the value of the
?(u,|w|+1)

bit, it branches to the next state: q w −−−−−−−→C q w.u for u ∈ {0, 1} and
w ∈ {0, 1}≤log(I)−1 . Then we get an ε-transition from those leaves of the tree
ε
that encode a proper index, lying in [1..I]. We have the rule q w −
→C q (ch,ℓ) if
w = bin(ℓ) and ℓ ∈ [1..I]. For the second phase, we need transitions to store a
?(xi ,v)

ℓ
variable and its evaluation: q (ch,ℓ) −−−−→C q(x
for ℓ ∈ [1..I], i ∈ [1..n], and
i ,v)
!#j

ℓ
ℓ
−−→C q(x
v ∈ {0, 1}. In the third phase, the contributor loops. We have q(x
i ,v)
i ,v)
if xi evaluated to v satisfies clause Cjℓ .

The program A is defined to be A = (D , a0 , (PL , PC )) and the LCR-instance
of interest is thus (A, FL ). The correctness of the construction is shown in the
following lemma. Hence, all requirements of a cross-composition are met.

Lemma 21. There is a t ∈ N so that c0 →∗At c with c ∈ C f if and only if there
is an ℓ ∈ [1..I] such that ϕℓ is satisfiable.

Proof. We first assume that there is an ℓ ∈ [1..I] such that ϕℓ is satisfiable. Let
v1 , . . . , vn be the evaluation of the variables x1 , . . . , xn that satisfies ϕℓ . Further,
we let bin(ℓ) = u1 . . . ulog(I) be the binary representation of ℓ. Set t = n. Then
the program At has n copies of the contributor. Denote them by P1 , . . . , Pn .
Intuitively, Pi is responsible for variable xi .
We construct a computation of At from c0 to a configuration in C f . We
proceed as in the aforementioned phases. In the first phase, PL starts to guess

the first bit of bin(ℓ). This is read by all the contributors. We get a computation
!(u1 ,1)

(b,1)

, q ε , . . . , q ε , (u1 , 1))

?(u1 ,1)

(b,1)

, q u1 , q ε , . . . , q ε , (u1 , 1))

?(u1 ,1)

(b,1)

c0 −−−−→L (qL
−−−−→1 (qL

. . . −−−−→n (qL

, q u1 , . . . , q u1 , (u1 , 1)) = c(b,1) .

To extend the computation, we let PL guess the remaining bits, while the contributors read and store. Hence, we get
(b,log(I))

c0 →∗At c(b,log(I)) = (qL

, q bin(ℓ) , . . . , q bin(ℓ) , (ulog(I) , log(I))).

Before the second phase starts, the contributors perform an ε-transition to
the state q (ch,ℓ) . This is possible since bin(ℓ) encodes a proper index in [1..I].
(b,log(I)) (ch,ℓ)
,q
, . . . , q (ch,ℓ) , (ulog(I) , log(I))) = c(x,0) .
We get c(b,log(I)) →∗At (qL
In the second phase PL chooses the correct evaluation for the variables, it
writes (xi , vi ) for each variable xi . Contributor Pi reads (xi , vi ) and stores it.
Hence, we get the computation
!(x1 ,v1 )

(x,1)

, q (ch,ℓ) , . . . , q (ch,ℓ) , (x1 , v1 ))

?(x1 ,v1 )

(x,1)

ℓ
, q(x
, q (ch,ℓ) , . . . , q (ch,ℓ) , (x1 , v1 ))
1 ,v1 )

!(x2 ,v2 )

(x,2)

ℓ
, q (ch,ℓ) , . . . , q (ch,ℓ) , (x2 , v2 ))
, q(x
1 ,v1 )

?(x2 ,v2 )

(x,2)

ℓ
ℓ
, q(x
, q(x
, q (ch,ℓ) , . . . , q (ch,ℓ) , (x2 , v2 ))
1 ,v1 )
2 ,v2 )

c(x,0) −−−−−→L (qL
−−−−−→1 (qL
−−−−−→L (qL
−−−−−→2 (qL
?(xn ,vn )

(x,n)

. . . −−−−−→n (qL

ℓ
ℓ
, (xn , vn )) = c(x,n) .
, . . . , q(x
, q(x
n ,vn )
1 ,v1 )

In the last phase, the contributors write the symbols #j . Since ϕℓ is satisfied
by the evaluation v1 , . . . , vn , there is a variable i1 ∈ [1..n] such that xi1 evaluated
to vi1 satisfies clause C1ℓ . Hence, due to the transition relation δC , we can let
Pi1 write the symbol #1 . After that, the leader reads it and moves to the next
state. This amounts to the computation
!#1

(x,n)

?#1

(#,1)

c(x,n) −−→i1 (qL

−−→L (qL

ℓ
ℓ
, #1 )
, . . . , q(x
, q(x
n ,vn )
1 ,v1 )
ℓ
ℓ
, #1 ) = c(#,1) .
, . . . , q(x
, q(x
n ,vn )
1 ,v1 )

Similarly, we can extend the computation to reach the configuration
(#,m) ℓ
ℓ
, #m ) which lies in C f . This proves the first
c(#,m) = (qL
, q(x1 ,v1 ) , . . . , q(x
n ,vn )
direction.
Now we assume the existence of a t ∈ N such that there is a computation ρ
from c0 to a configuration in C f . Let ρL be the subcomputation of ρ carried out

by the leader PL . Then ρL can be split into ρL = ρ1L .ρ2L .ρ3L such that
(b,0) !(u1 ,1)

ρ1L = qL
ρ2L =
ρ3L =

!(ulog(I) ,log(I))

(b,1) !(u2 ,2)

−−−−→L qL

(b,log(I))

−−−−→L . . . −−−−−−−−−−→L qL

!(xn ,vn )
(b,log(I)) !(x1 ,v1 )
(x,1) !(x2 ,v2 )
qL
−−−−−→L qL
−−−−−→L . . . −−−−−→L
?#m
(x,n) ?#1
(#,1) ?#2
(#,m)
qL
−−→L qL
−−→L . . . −−−→L qL
.

(x,n)

qL

,

,

Let ℓ be the natural number such that bin(ℓ) = u1 . . . ulog(I) . We show that
ℓ ∈ [1..I] and ϕℓ is satisfied by evaluating the variables xi to vi .
In ρ3L , the leader can read the symbols #1 , . . . , #m . This means that there
is at least one contributor writing them. Let PC be a contributor writing such
a symbol. Then, after PL has finished ρ1L , the contributor PC is still active
ε
and performs the step q bin(ℓ) −
→C q (ch,ℓ) . This is true since PC did not miss a bit
transmitted by PL and PC has to reach a state where it can write the #-symbols.
Thus, we get that ℓ ∈ [1..I] and PC stores ℓ in its state space.
We denote the number of contributors writing a #-symbol in ρ by t′ ≥ 1.
Each of these contributors gets labeled by C(j) = {#j1 , . . . , #jkj }, the set of
#-symbols it writes during the computation ρ. Hence, we have the contributors
PC(1) , . . . , PC(t′ ) and since each symbol in {#1 , . . . , #m } is written at least once,
we have:
′

{#1 , . . . , #m } =

t
[

C(j).

(1)

j=1

Now we show that each PC(j) with C(j) = {#j1 , . . . , #jkj } stores a tuple
(xi , vi ) such that xi evaluated to vi satisfies the clauses Cjℓ1 , . . . , Cjℓk . We already
j

know that PC(j) is in state q (ch,ℓ) after PL has executed ρ1L . During PL executing
ρ2L , the contributor PC(j) has to read a tuple (xi , vi ) since it has to reach a
state where it can write the #-symbols. More precise, PC(j) has to perform a
?(xi ,vi )

ℓ
for some i. Then the contributor writes the
transition q (ch,ℓ) −−−−−→C(j) q(x
i ,vi )
symbols #j1 , . . . , #jkj while looping in the current state. But by the definition
of the transition relation for the contributors, this means that xi evaluated to vi
satisfies the clauses Cjℓ1 , . . . , Cjℓk .
j

By Equation (1) we can deduce that every clause in ϕℓ is satisfied by the
chosen evaluation. Hence, ϕℓ is satisfiable.
⊓
⊔
Formal Construction and Proof of Proposition 9
Formally, the required finite state system is N = (QN , q0 , δN ) (we omit the
alphabet here), with states QN = QL × D × 2QC . The initial state is given by
0
0
q0 = (qL
, a0 , {qC
}). The idea behind the construction is to simulate the moves
of the leader exactly and to simulate the moves of the contributor by saturating
the set of states that the contributors can reach. For this, for every move of

?a/ǫ

the leader of the form q −−−→PL q ′ ∈ δL , for all S ⊆ QC we have moves of
the form (q, a, S) −
→N (q ′ , a, S) in N . Similarly for every move of the form
!a

q −→PL q ′ ∈ δL , we have for all S ⊆ QC , b ∈ D we have moves of the form
(q, b, S) −
→N (q ′ , a, S) in N . For every move of the contributor of the form
?a/ǫ

q −−−→PC q ′ ∈ δC , for all p ∈ QL and S ⊆ QC : q ∈ S we have moves of the form
(p, a, S) −
→N (p, a, {q ′ } ∪ S) in N and for every move of the contributor of the
!a

form q −→PC q ′ ∈ δC , for all p ∈ QL , b ∈ D and S ⊆ QC : q ∈ S we have moves
of the form (p, b, S) −
→N (p, a, S ∪ {q ′ }).
Before we prove the correctness of the above construction, we introduce
a few notations. Given any configuration c of At , for any q ∈ QL we let
#Q (c, q) be the number of contributor processes in c that are currently in
state q. Further, let QC (c) be the set of all contributor states that appear in
c: QC (c) = {q | #Q (c, q) > 0}. We will use QL (c), D (c) to refer to the state of
leader and the value in shared memory respectively. The correctness of the above
construction follows from the following lemma which states that corresponding
to any configuration that is reachable from the initial configuration through a
parametrized computation, there is a state in the finite state system N which is
reachable from the initial state such that state of leader and the memory value in
the state coincides with the configuration, set of contributor states in the state
of the finite state system includes the set of states of the contributors in the
configuration.
Lemma 22. There is a t ∈ N so that c0 →∗At c with c ∈ C f if and only if
q0 →∗N (q, a, S), where q = QL (c), a = D (c) and S is such that QC (c) ⊆ S.
Proof. For ⇒ direction, we will induct on the length of the computation to show
that for t ∈ N, corresponding to any computation of the form c0 →At c, there is
an appropriate computation in N .
Base case: In this case, the length of the computation is 0. Notice that the
0
0
initial state of the finite state system N is of the form q0 = (qL
, a0 , {qC
}). Hence
the required run is the zero length run involving q0 .
Inductive case: Suppose we have an appropriate run for every computation
in A of length at-most ℓ, we will prove the same is true for computations of
length ℓ + 1. Let c0 →∗At c be any computation of length ℓ + 1. Then such
a computation can be split up as c0 →∗At c′ →At c, where c0 →∗At c′ is a
computation of length ℓ. By induction hypothesis, there is a computation in N
of the form q0 →∗N (q ′ , a′ , S ′ ) such that q ′ = QL (c′ ), a′ = D (c′ ) and S ′ is such
that QC (c′ ) ⊆ S ′ .
If the c′ → c was move of the leader, then in our N , we have a corresponding
move which does not modify the subset S but updates the state and memory
value appropriately. Using such a move will give us the appropriate run.
If the c′ → c was move of the contributor, let the move be of the form
?a/ǫ

p −−−→ p′ . From induction hypothesis, we have that p ∈ S ′ . By construction, we
have a transition of the form (q ′ , a′ , S ′ ) −
→N (q ′ , a′ , p′ ∪ S ′ ). Further the states of

contributor in c are either S ′ ∪ {p′ } or S ′ \ {p} ∪ {p′}, in both cases, it is covered
by S ′ ∪ {p′ }. From this we get the required run.
The case when the transition is a write is similar.
For ⇐ direction, we will inductively prove something stronger. We will prove
that for every computation of the form q0 →∗N (q, a, S), there is a t ∈ N and a
computation c0 →∗At c such that q = QL (c), a = D (c) and QC (c) = S. This we
will prove by inducting on the length of the run. For this, we will crucially use
the copy cat lemma that was proved in [15]. The copy cat lemma states that if
there is computation in the given program such that a state q is reached in the
contributor, then there is also another computation where we can have as many
contributors in q as we wish. We formally restate this lemma in our setting.
Lemma 23 (Copy cat lemma [15]). If there is a computation of the form
c0 →∗At c for some t ∈ N such that #Q (c, q) > 0 for some q ∈ QC , then for
all k ∈ N, we have a computation of the form c0 →∗At+k d, where d is such that
#Q (q, d) = #Q (q, c) + k and for all q ′ 6= q we have #Q (q ′ , d) = #Q (q ′ , c).
Base case: In this case, the length of the computation is 0. In this case, the
required run simply involves the configuration c0 for some t ∈ N.
Inductive case: Suppose we have an appropriate run for every computation
in N of length at-most ℓ, we will prove the same is true for computations of
length ℓ + 1. Consider any computation in N of the form q0 →∗N (q, a, S) that
involves ℓ + 1 moves. The such a run can be split into q0 →∗N (q ′ , a′ , S ′ ) →N
(q, a, S) where q0 →∗N (q ′ , a′ , S ′ ) is a computation involving ℓ steps. Now invoking
the induction hypothesis, we have a t ∈ N and a computation in the program
of the form c0 →∗At c′ such that q ′ = QL (c′ ), a′ = D (c′ ) and QC (c′ ) = S ′ .
Suppose the move (q ′ , a′ , S ′ ) −
→N (q, a, S) involved only the leader state and
the memory value, then such a move was possible because of a transition in
the leader process PL . This transition is enabled from the configuration c′ since
we have that QL (c′ ) = q ′ , D (c′ ) = a. Applying this transition will give us the
required run.
Suppose the move was of the form (q, a, S ′ ) −
→N (q, a, {p′ } ∪ S ′ ), then such a
transition was added to N because of some transition in δC . Let us suppose the
corresponding transition was τ = (p, ?a, p′ ) ∈ δC (the other cases are similar).
The run obtained by applying induction hypothesis, is of the form c0 →∗At c′
such that #Q (c′ , p) > 0. Now applying the copy cat lemma to such a run, we
also obtain a run of the form c0 →∗At+1 d such that for all r 6= p we have
#Q (d, r) = #Q (c′ , r) and #Q (d, p) > 1. Notice that this new run also satisfies
the required properties. Further in this run, there are at least two contributors
in the required state p. Now applying the transition τ to one of these contributor
gives us the required extension of the run.
⊓
⊔
Discussion on the Complexity
Notice that the automaton N that we constructed has at most O(2C · L · D) many
states. We add at most O(4C · L2 · D2 ) edges. Adding each edge can consume time

O(C2 · L2 · D). Hence, the over all construction can take time O(4C · C2 · L4 · D3 ).
Checking reachability in N can consume at most time O(4C · L2 · D2 ). Hence, the
cost of such an operation is bounded by O(4C · C2 · L4 · D3 ).

Formal Construction and Proof of Proposition 11
For the reduction in Part a), let ϕ be a given 3-SAT-instance. We assume ϕ to
have the variables x1 , . . . , xn and clauses C1 , . . . , Cm . The construction of an
LCR-instance relies on the following idea: The leader PL will guess an evaluation
for each variable, starting with x1 . To this end, it will write a tuple of the form
(x1 , v1 ), with v1 ∈ {0, 1}, to the memory. A contributor will read the tuple and
stores it in its state space. This is repeated for each variable. After the guessingphase, the contributors can write the symbols #j , depending on whether the
currently stored variable with its evaluation satisfies clause Cj . As soon as the
leader has read the complete string #1 . . . #m , it moves to its final state, showing
that the guessed evaluation satisfied all the clauses.
For the formal construction, let the domain of the memory be the
set D = {(xi , v) | i ∈ [1..n], v ∈ {0, 1}} ∪ {#j | j ∈ [1..m]} ∪ {a0 }. We define the
(x,0)
leader to be the tuple PL = (Op(D ), QL , qL , δL ), where the states are given by
(x,i)
(#,j)
QL = {qL | i ∈ [0..n]} ∪ {qL
| j ∈ [1..m]}. The transition relation δL is de(x,i−1) !(xi ,v)

(x,i)

fined as follows. We have rules for guessing the evaluation: qL
−−−−→L qL
for each i ∈ [1..n] and v ∈ {0, 1}. And we have rules for verifying that the guessed
(#,j−1) ?#j

(#,j)

for j ∈ [1..m]. Note that we identify
−−→L qL
evaluation is correct: qL
(x,n)
(#,0)
(#,m)
the state qL
by qL . We further set FL = {qL
}.
The contributor PC is defined by PC = (Op(D ), QC , q 0 , δC ) with set of states
QC = {q(xi ,v) | i ∈ [1..n], v ∈ {0, 1}} ∪ {q 0 }. Then we have C = 2n + 1 = O(n).
The transition relation contains the following rules. For storing a read evaluation
?(xi ,v)

we have: q 0 −−−−→C q(xi ,v) , for i ∈ [1..n], v ∈ {0, 1}. And for satisfying clauses,
!#j

we get a rule q(xi ,v) −−→C q(xi ,v) if variable xi evaluated to v satisfies clause Cj .
The program A is defined as the tuple A = (D , a0 , (PL , PC )) and the LCRinstance is (A, FL ). The correctness of the construction is proven in the following
lemma.
Lemma 24. There is a t ∈ N so that c0 →∗At c with c ∈ C f if and only if ϕ is
satisfiable.
Proof. Let ϕ be satisfiable, by the evaluation v1 , . . . , vn . We show how to construct the desired computation. First set t = n, so we have n copies of PC . Let
these denoted by P1 , . . . , Pn .

The leader PL first guesses the correct evaluation of the variables. Each Pi
will store the evaluation for variable xi .
!(x1 ,v1 )

(x,1)

, q 0 , . . . , q 0 , (x1 , v1 ))

?(x1 ,v1 )

(x,1)

, q(x1 ,v1 ) , q 0 , . . . , q 0 , (x1 , v1 ))

c0 −−−−−→L (qL

−−−−−→1 (qL
?(xn ,vn )

(x,n)

. . . −−−−−→n (qL

, q(x1 ,v1 ) , . . . , q(xn ,vn ) , (xn , vn )) = c(x,n) .

Since v1 , . . . , vn is a satisfying assignment, there is an index i1 ∈ [1..n] such that
xi1 evaluated to vi1 satisfies clause C1 . Hence, the corresponding contributor
Pi1 can write the symbol #1 . This is then read by the leader. The process gets
repeated for #2 , . . . , #m . Hence, we get
!#1

(x,n)

c(x,n) −−→i1 (qL

, q(x1 ,v1 ) , . . . , q(xn ,vn ) , #1 )

?#1

(#,1)
−−→L (qL , q(x1 ,v1 ) , . . . , q(xn ,vn ) , #1 )
?#m

(#,m)

. . . −−−→L (qL

, q(x1 ,v1 ) , . . . , q(xn ,vn ) , #1 ) = c(#,m) ,

with c(#,m) ∈ C f .
For the other direction, let a t ∈ N and a computation ρ from c0 to a configuration in C f be given. Let ρL denote the subcomputation of ρ carried out by
the leader PL . Then ρL has the form ρL = ρ1L .ρ2L with
(x,0) !(x1 ,v1 )

ρ1L = qL

(x,n) ?#1

ρ2L = qL

(x,1) !(x2 ,v2 )

−−−−−→L qL

(#,1) ?#2

−−→L qL

!(xn ,vn )

(x,n)

−−−−−→L . . . −−−−−→L qL
?#m

(#,m)

−−→L . . . −−−→L qL

,

.

We show that v1 , . . . , vn is a satisfying assignment for ϕ.
Since PL can read the symbol #1 during ρ2L , there is a contributor Pℓ writing
the symbol. But this can only happen if Pℓ has stored a tuple (xi , vi ), written
by PL during ρ1L , and if xi evaluated to vi satisfies clause C1 . Since all symbols
#1 , . . . #m are read by PL , we get that each clause in ϕ is satisfiable by the
evaluation chosen by PL during ρ1L .
⊓
⊔
For Part b) of the proposition, we change the above construction slightly. Let
ϕ1 , . . . , ϕI be the given 3-SAT-instances, each pair equivalent under R, where R
is the polynomial equivalence relation from Theorem 8. Then each formula has
the same number of clauses m and uses the set of variables {x1 , . . . , xn }. We
ℓ
.
assume ϕℓ = C1ℓ ∧ · · · ∧ Cm
First, we let the leader chose an evaluation of the variables x1 , . . . , xn as
above. The contributors are used to store it. Then, instead of writing just #j ,
the contributors can write the symbols #ℓj to mention that the currently stored
variable with its evaluation satisfies clause Cjℓ . The leader can now branch into
one of the I instances. It waits to read a string #ℓ1 . . . #ℓm for a certain ℓ ∈ [1..I].
If it can succeed, it moves to its final state.

To realize the construction, we need to slightly change the structure of the
leader, extend the data domain and add more transitions to the contributors. The
parameter C will not change in this construction, it is still O(n). Hence, the sizerestrictions of a cross-composition are met. The correctness of the construction
is similar to Lemma 24, the only difference is the fact that PL also chooses the
instance ϕℓ that should be satisfied.

B

Proofs for Section 4

NP-hardness of BSR with constant Memory and Stages
We can easily show that even for constant memory the single stage bounded
reachability problem is NP-hard. For this, we first fix a 3-SAT formula Ψ =
C1 ∧ C2 ∧ · · · ∧ Cm whose satisfiability we are interested in. It is well known that
satisfiability of 3-SAT is NP-hard We will further assume that such a formula
has n variables {x1 , . . . xn }. We will now show how to reduce the satisfiability
problem of the given 3-SAT formula to an bounded-stage reachability problem (involving at-most 1-stages) on an program A = (D , a0 , (Px1 , . . . , Pxn , Pv )),
where D = {#, 0, 1}.
Here we have one process called the verifier Pv and one process per each
variable Px1 . . . Pxn . Before we provide the actual construction, we provide an
encoding of the set {x1 , ¬x1 , . . . xn , ¬xn } in binary. For any n, i ∈ N, we let
binn (i) ∈ ({0, 1}.#)log(n)+1 to be the log(n) + 1 length binary encoding of the
digit i with # separating each such digit (for e.g. bin8 (1) = 0#0#0#1#). Now
xi is simply encoded as 1# binn (i) and ¬xi is encoded as 0# binn (i), we will
denote this by Enc(xi ) and Enc(¬xi ) respectively.
The process Pv is defined as follows. It iterates over each of C1 , . . . , Cm . For
each Ci = (xi ∨yi ∨zi ), xi , yi , zi ∈ {x, ¬x1 , . . . , xn , ¬xn } it writes on to the shared
memory one of Enc(xi ), Enc(yi ) or Enc(zi ). For this it has states of the form [1..m]
(i.e. one state per each clause) and between such states it has transitions of the
!Enc(x)

form i −−−−→ i + 1 for each x ∈ {xi , yi , zi }. Here !Enc(x) indicates write of
each symbol in Enc(x) on to the shared memory, this can easily be achieved
by |Enc(x)| many intermediary states. Notice that the process Pv needs at-most
O(m × log(n)) many states. Notice that exactly m many variables are written
to the shared memory.
The processes Pxi associated with the variable xi does the following. Initially
it selects a valuation for the variable xi and stores it in the state. It includes the
states of the form {0, 1} × [1..m]. Here {0, 1} is used to store the valuation and
[1..m] is to count precisely the number of variable-values it read from the shared
memory. Now from any state of the form (i, j), i ∈ {0, 1}, j ∈ [1..m − 1], for all
?Enc(x)

x 6∈ {xi , ¬xi }, there is a transition of the form (i, j) −−−−→ (i, j + 1). That is, for
any variable that is not of its type, it simply skips and only counts how many of
them occurred. Suppose that the variable read from the memory was of type xi
,then it checks that the valuation it guessed matches the one that it reads from
the memory. For this, from any state of the form (0, j), j ∈ [1..m − 1], we have

?Enc(¬xi )

a transition of the form (0, j) −−−−−−→ (0, j + 1) and from the state of the form
?Enc(xi )

(1, j), j ∈ [1..m − 1], we have a transition of the form (1, j) −−−−−→ (1, j + 1).
We have skipped the intermediate states that arrange the reading of the string
Enc(x). But this can be arranged by at most |Enc(x)| many states.
It is easy to see that the given formula has a satisfying assignment if and
only if the verification process Pv chooses for each of the clause the right variable
that makes it true, each of the variable processes guess the right valuation for
the variable, read all the values output by Pv without any loss and reaches the
state (i, m). Notice that if a verification process Pxi indeed reaches such a state
then it means it has not missed any of the values output and also that each time
Pv guessed consistently the correct valuation for the variable xi . Further such a
computation requires at-most 1-stage since only the process Pv writes.
Formal Construction and Proof of Proposition 12
The idea here is to reduce BSR to the reachability problem on an NFA N of size
at most O(Pt · poly(k, n, D)). The states of the NFA N are the product of the
states of each Pi along with the current stage number, currently active process
and the last value written to the memory i.e. it is of the form QN = Q1 ×
. . . Qt × [0..t] × [0..k] × D . The currently active process records the information
about who is allowed to write in that stage. The initial state of N is given by
0
qN
= (q10 , . . . qt0 , 0, 0, a0 ).
From any state of the form (q1 , . . . , qn , i, j, a), i ∈ [0..t], j ∈ [0..k], for all
?a/ǫ

moves of the form qℓ −−−→Pℓ qℓ′ for some ℓ ∈ [1..t], we have a corresponding move of the form (q1 , . . . , qn , i, j, a) −
→N (q1 , . . . , qℓ−1 , qℓ′ , . . . , qn , i, j, a), this
freely simulates any read move within a stage.
Similarly from any state of the form (q1 , . . . , qn , i, j, a), a ∈ Σ, i ∈ [1..t], j ∈
!b

→Pi qi′ , we have a corresponding move of
[1..k], for all moves of the form qi −
the form (q1 , . . . , qn , i, j, a) −
→N (q1 , . . . , qi−1 , qi′ , . . . , qn , i, j, b). These set of transitions allow the currently active process Pi during any stage to write values to
shared memory.
Finally from any state of the form (q1 , . . . , qn , i, j, a), i ∈ [0..t], j ∈ [0..k−1] we
have moves of the form (q1 , . . . , qn , i, j, a) −
→N (q1 , . . . , qn , m, j + 1, a), for all m ∈
[1..t]. The correctness of such a construction is guaranteed by the following easy
to see lemma. The complexity follows from the fact that reachability is quadratic
and size of the automata that we construct is at-most O(Pt · poly(k, n, D)).
Lemma 25. There is an ℓ-stage computation c0 →∗A c if and only if there is
0
a computation of the form qN
→∗N qN for some qN ∈ {(q1 , . . . , qn , i, ℓ, a) | i ∈
[0..t], a ∈ D , (q1 , . . . , qn ) = c}.
Proof. (⇒) For this direction, we will assume an ℓ-stage computation of the form
0
c0 →∗A c and show that there is a computation in N of the form qN
→∗N qN .
0
∗
∗
Since cA →A cA is an ℓ-stage computation, it can be split as c0 →A c1 →∗A
c2 · · · →∗A cℓ+1 , where c0 = c0 , cℓ+1 = c and each of πi = ci −
→A ci+1 is an

1-stage computation. Further for i ∈ [1..ℓ], let pi be the writer corresponding
to the stage πi . It is easy to see that corresponding to every move in the subcomputation of the form (q1 , . . . , qt , a) →A (q1′ , . . . , qt′ , b), there is a move of
the form (q1 , . . . , qt , pi , j, a) −
→A (q1′ , . . . , qt′ , pi , j, b) for all j ∈ [1..k]. Given a
configuration c = (q1 , . . . , qt , a), we let µ(c, p, j) = (q1 , . . . , qt , p, j, a). Given a
computation π, we let µ(π, x, y) to be the sequence obtained by replacing each
configuration c occurring in π by µ(c, x, y). It is easy to see that µ(π0 , 0, 0),
µ(π1 , p1 , 1), . . . , µ(πℓ , pℓ , ℓ) are all valid sub-computations in N . This is because
we have for every move in the program, a corresponding move in the N we
construct. Combining these sub-computations will give us the required run in
N . For combining these sub-computations, we use the transition of the form
(q1 , . . . , qn , i, j, a) −
→N (q1 , . . . , qn , m, j + 1, a), for all m ∈ [1..t] that was finally
added in the construction.
(⇐) For this direction, we will assume a computation of the form π =
0
qN
→∗N qN , where qN = (q1 , . . . , qn , i, ℓ, a) for some i ∈ [1..t], a ∈ Σ.
Clearly such a computation can be split as follows π = (q10 , . . . , qt0 , 0, 0, r) −
→N
(q11 , . . . , qt1 , 0, 0, a1 ) −
→N . . . (q11 , . . . , qt1 , i1 , 1, a1 ) −
→N (q12 , . . . , qt2 , i1 , 1, a2 ) −
→N
(q12 , . . . , qt2 , i2 , 2, a2 ) −
→N . . . −
→N (q1ℓ+1 , . . . , qtℓ+1 , iℓ , ℓ, aℓ+1 ).
Let π0 = (q10 , . . . , qt0 , 0, 0, r) −
→N (q11 , . . . , qt1 , 0, 0, a1 ) and πj =
j+1
j+1
j
j
(q1 , . . . , qt , ij , j, aj ) −
→N (q1 , . . . , qt , ij , j, aj+1 ).
It is easy to see that corresponding to every move of the form
(q1 , . . . , qn , i, j, a) −
→N (q1′ , . . . , qn′ , i, j, a′ ), there is a move of the form
′
(q1 , . . . , qn , a) −
→ (q1 , . . . , qn′ , a′ ) such that it is either an read or internal move
of some process or a write move of process Pi . Notice that the transition in N
was added because of existence of one such move in the program. Using this
fact, it is easy to see that corresponding to each πi , i ∈ [0..ℓ], there is a 1-stage
sub-computation in A. Concatenating these sub-computations will now give us
the required run.
⊓
⊔
Formal Construction and Proof of Proposition 13
For the formal construction, we define for i ∈ [1..k] the NFA Pi to be the tuple
ℓ
Pi = (Op(D ), Qi , qi0 , δi ) with Qi = {qij | j ∈ [1..k]} ∪ {qij
| j, ℓ ∈ [1..k]} ∪ {qi0 }.
ℓ
The states qij are used to store one of the k vertices of the i-th row, the states qij
are needed to check the edge relations to other rows and to perform the equality
check. The transition relation δi is given by the following rules: For choosing
?a0

and storing a vertex of the i-th row we have qi0 −−→i qij for any j ∈ [1..k].
For checking the edge relations to vertices from a different row, we have for
?(ℓ,m)

ℓ−1
ℓ
ℓ, j ∈ [1..k] the rule qij
−−−−→i qij
if ℓ 6= i and if there is an edge between (i, j)
0
and (ℓ, m) in G. Note that we identify qij as qij
. Finally, to test the equivalence
?(i,j)

i−1
i
in the case of the same row we have qij
−−−→i qij
for j ∈ [1..k].
The writer Pch is given by Pch = (Op(D ), Q, q0 , δ), where Q = {q0 , . . . , qk }
!(i,j)

and δ is given by the rules qi−1 −−−→ch qi for i, j ∈ [1..k]. Altogether, we define
the program A to be A = (D , a0 , ((Pi )i∈[1..k] , Pch )) and the set of configurations

k
k
, . . . , qkj
, qk , a) | j1 , . . . , jk ∈ [1..k], a ∈ D }. The
we want to reach as C f = {(q1j
1
k
correctness of the construction follows by the lemma below.

Lemma 26. There is a 1-stage computation c0 →∗A c for a c ∈ C f if and only
if there is a clique of size k in G with one vertex from each row.
Proof. First note that any computation in A is a 1-stage computation since the
only thread that can write to the memory is Pch .
Let a clique of size k in G be given. It consists of the vertices
(1, j1 ), . . . , (k, jk ). Then it is easy to construct a computation of A starting in
k
k
, . . . , qkj
, qk , (k, jk )) ∈ C f : The system just
(q10 , . . . , qk0 , q0 , γ) and ending in (q1j
1
k
guesses the right vertices (1, j1 ) up to (k, jk ) and then performs the edge-tests
which are all positive since the vertices form a clique.
For the other direction, let a computation ρ leading to
k
k
, . . . , qkj
(q1j
, q0 , (k, jk )) be given. Then we show that the vertices
1
k
(1, j1 ), . . . , (k, jk ) form a clique. Since the Pi can only start their computations on the initial memory symbol a0 , they have to perform a step before
Pch changes the memory content. Thus, we can split ρ into ρ = ρ1 .ρ2 where ρ1
contains only moves of the Pi on reading a0 , in any order. We may assume the
following form for ρ1 :
?a0

0
, q20 , . . . , qk0 , q0 , a0 )
(q10 , . . . , qk0 , q0 , a0 ) −−→1 (q1j
1
?a0

0
0
, . . . , qkj
, q0 , a0 ).
. . . −−→k (q1j
1
k

Note that the computation ρ1 corresponds to the choice of the vertices
(1, j1 ), . . . , (k, jk ) as a clique-candidate.
After ρ1 , the thread Pch needs to write the symbol (1, j1 ) to the memory since
otherwise, P1 would deadlock. But then each Pi with i 6= 1 needs to do a step
on reading (1, j1 ) and this only happens if (i, ji ) and (1, j1 ) share an edge. Then
the computation ρ2 goes on with Pch writing (2, j2 ) since otherwise, P2 would
deadlock. The other threads again perform a verification step on reading (2, j2 ).
k
k
, . . . , qkj
, q0 , (k, jk )) in the
Since the computation reaches the configuration (q1j
1
k
end, we can ensure that all chosen vertices indeed share an edge.
⊓
⊔
Formal Construction and Proof of Theorem 14
Let ϕ1 , . . . , ϕI be given 3-SAT-instances, each two equivalent under R. We asℓ
sume that each ϕℓ has the form: ϕℓ = C1ℓ ∧ · · · ∧ Cm
and the set of variables
used by the 3-SAT-instances is {x1 , . . . , xn }. We define the data domain to be
D = [1..I] × [1..m] × [1..n] × {0, 1} ∪ {a0 }.
For each i ∈ [1..n], we introduce a thread Pxi = (Op(D ), Qxi , qx0i , δxi ), where
j
j
j
stores the chosen
| j ∈ [0..m]} ∪ {qx0i }. Each state q(x
, q(x
Qxi = {q(x
i ,v)
i ,0)
i ,1)
evaluation v of xi and the number j of clauses that were already satisfied. We
have |Qxi | = 2(m + 1) + 1. The transition relation δxi contains the following
?a0

0
for v ∈ {0, 1}.
rules: For choosing an evaluation of xi we have qx0i −−→xi q(x
i ,v)

For checking the satisfiability of clauses we have for ℓ ∈ [1..I], j ∈ [1..m], and
?(ℓ,j,i,v)

j
j−1
if clause Cjℓ is satisfied by variable xi under
v ∈ {0, 1}: q(x
−−−−−→xi q(x
i ,v)
i ,v)
evaluation v. If the requested variable is not xi , the thread Pxi just performs
?(ℓ,j,i′ ,v ′ )

j−1
j
a counting step: q(x
for i′ 6= i, ℓ ∈ [1..I], j ∈ [1..m], and
−−−−−−→xi q(x
i ,v)
i ,v)
′
v ∈ {0, 1}.
0
Next, we introduce the writer-thread Pw = (Op(Σ), Qw , qw
, δw ) with
0
m
Qw = {qw , . . . , qw }. Thus, we have |Qw | = m + 1. The writer picks m clauses
of probably different instances that need to be satisfied. To this end, it will not
only guess the clause but also the instance that contains the clause, the variable
that should satisfy it, and the evaluation of the variable. This will then be discarded or verified by the variable-threads. The transitions that we need in δw
!(ℓ,j,i,v)

j−1
j
are thus of the form qw
−−−−−→w qw
for any ℓ ∈ [1..I], j ∈ [1..m], i ∈ [1..n],
and v ∈ {0, 1}. Writing (ℓ, j, i, v) to the memory reflects the claim that clause
Cjℓ gets satisfied by variable xi under evaluation v.
The last type of threads that we introduce are the bit-checkers.
For each b ∈ [1.. log(I)] we define Pb = (Op(Σ), Qb , qb0 , δb ) where
j
j
Qb = {q(b,0)
, q(b,1)
| j ∈ [1..m]} ∪ {qb0 }. Hence, we have that |Qb | = 2m + 1. The
task of bit-checker Pb is to verify that along the instances ϕℓ1 , . . . , ϕℓm guessed
by the writer, the b-th bit of bin(ℓj ) for j ∈ [1..m] does not change. To this
end, we construct δb the following way: Initially, Pb stores the b-th bit of the
first guessed instance. We add for ℓ ∈ [1..I], i ∈ [1..n], and v ∈ {0, 1} the rule
?(ℓ,1,i,v)

1
qb0 −−−−−−→b q(b,u)
if the b-th bit of bin(ℓ) is u ∈ {0, 1}. For the comparison
with further guessed instances we have for j ∈ [2..m], ℓ ∈ [1..I], i ∈ [1..n], and
?(ℓ,j,i,v)

j−1
j
v, u ∈ {0, 1} the rule q(b,u)
if the b-th bit of bin(ℓ) is u.
−−−−−→b q(b,u)
We define the program A as A = (D , a0 , (Pw , (Pxi )i∈[1..n] , (Pb )b∈[1.. log(I)] )).
We want the writer and the bit-checkers to perform exactly m steps and the
variable-threads to move exactly m + 1 steps. Intuitively, this amounts to the
satisfiability of m clauses that all belong to the same instance. Hence, the set of
configurations C f that we want to reach is the following:
m
m
m
m m
, a) | vi , uℓ ∈ {0, 1}, a ∈ Σ}.
, . . . , q(log(I),u
, q(1,u
{(qw
, q(x1 ,v1 ) , . . . , q(x
1)
n ,vn )
log(I) )

Since Pw is the only thread which is allowed to write, we are interested in
reaching C f within a 1-stage computation. Hence, the BSR-instance of interest
is the tuple (A, C f , 1). Note that the parameters obey the bounds of a crosscomposition: P = 2(m + 1) + 1 and t = 1 + n + log(I). It is thus left to show
that the above construction is correct. This is proven in the following lemma.
Lemma 27. There is a 1-stage computation from c0 →∗A c for a c ∈ C f if and
only if there is an ℓ ∈ [1..I] such that ϕℓ is satisfiable.
Proof. First assume that there is an ℓ ∈ [1..I] such that ϕℓ is satisfiable. Let v1 , . . . , vn be the evaluation of x1 , . . . , xn that satisfies ϕℓ and let
bin(ℓ) = u1 . . . ulog(I) be the binary representation of ℓ. We construct a 1-stage

computation of A from c0 to the configuration
m
m
m
m m
, (ℓ, m, xz , vz )),
, . . . , q(log(I),u
, q(1,u
c = (qw
, q(x1 ,v1 ) , . . . , q(x
1)
n ,vn )
log(I) )
ℓ
where xz is a variable in Cm
.
The computation starts with choosing the right evaluation for the vari?a0

0
. This leads to the
ables: Each Pxi performs the move qx0i −−→xi q(x
i ,vi )
0
∗
0
0
0
0
0
computation c →A (qw , q(x1 ,v1 ) , . . . , q(xn ,vn ) , q1 , . . . , qlog(I)
, γ) = c0 . Then Pw
writes the tuple (ℓ, 1, i′ , vi′ ) to the memory, where xi′ is a variable in clause
C1ℓ . Furthermore, xi′ evaluated to vi′ satisfies the clause. This is read by
?(ℓ,1,i′ ,v ′ )

i
0
1
. Note that
all Pxi and each performs the step q(x
−−−−−−−
→xi q(x
i ,vi )
i ,vi )
′
due to the definition of δxi , in both cases, i 6= i and i = i′ , the move
can indeed be done. The bit-checkers Pb also read the tuple. Each Pb does

?(ℓ,1,i′ ,v ′ )

i
1
the following step: qb0 −−−−−−−
→b q(b,u
since ub is the b-th bit of bin(ℓ).
b)
If we put the individual moves together, this leads to a new configuration
1
1
1
1
1
c0 →∗A (qw
, q(x
, . . . , q(x
, q(1,u
, . . . , q(log(I),u
, (ℓ, 1, i′ , vi′ )) = c1 .
1 ,v1 )
n ,vn )
1)
log(I) )
Similarly, we can construct a computation that leads to a configuration c2 .
If we go on with the construction, we get a computation that leads to c.
For the other direction, let ρ be a 1-stage computation of A, ending in
m m
m
m
m
the configuration (qw
, q(x1 ,v1 ) , . . . , q(x
, q(1,u
, . . . , q(log(I),u
, a) = c. Let
n ,vn )
1)
log(I) )
ℓ ∈ [1..I] be such that bin(ℓ) = u1 . . . ulog(I) . We show that ϕℓ is satisfiable.
More precise, ϕℓ is satisfied under xi evaluating to vi .
Since Pxi can start its computation only on reading a0 , we get that each Pxi

?a0

0
. Note that the chosen vi is indeed the one
performs the step qx0i −−→xi q(x
i ,vi )
appearing in c. Hence, we get as an initial part of ρ the computation ρ0 = c0 →A
0
0
0
0
, a0 ) = c0 .
, q10 , . . . , qlog(I)
, . . . , q(x
(qw
, q(x
n ,vn )
1 ,v1 )
The computation can then only continue if Pw changes the content of the
memory. The thread guesses and writes (ℓ, 1, i′ , vi′ ) to the memory. He has to
choose the index ℓ, and thus the instance ϕℓ , since otherwise there would be a
m
. The bit-checkers Pb read (ℓ, 1, i′ , vi′ ) and store
bit-checker Pb not reaching q(b,u
b)
?(ℓ,1,i′ ,v ′ )

i
1
ub in their states: qb0 −−−−−−−
→b q(b,u
. Now all Pxi have to perform a step since
b)
the computation does not deadlock. This means that especially Pxi′ performs a
step on reading (ℓ, 1, i′ , vi′ ). By definition, this is only possible if xi′ is a variable
that evaluated to vi′ satisfies clause C1ℓ . Hence, we have that under evaluating
each xi to vi , clause C1ℓ is satisfied. If we combine all the moves done, we get
another part ρ1 of the computation ρ that leads from c0 to the configuration
1
1
1
1
1
, q(1,u
, . . . , q(log(I),u
, (ℓ, 1, i′ , vi′ )) = c1 .
, . . . , q(x
(qw
, q(x
1 ,v1 )
n ,vn )
1)
log(I) )
Similarly, one proves that the second part of ρ, the computation ρ2 shows
that C2ℓ is satisfiable under evaluating each xi to vi . Hence, by induction we get
that ϕℓ is satisfiable.
⊓
⊔

