1

2

Monadic Decomposability of Regular Relations
Pablo Barceló

4

Department of Computer Science, University of Chile & IMFD Chilepbarcelo@dcc.uchile.cl5Chih-Duo Hong3

7

Department of Computer Science, University of Oxford, United Kingdom
chih-duo.hong@st-hughs.ox.ac.uk

8Xuan-Bach Le

6

10

Department of Computer Science, University of Oxford, United Kingdom
bachdylan@gmail.com

11

Anthony W. Lin

913Technische Universität Kaiserslautern, Germany
anthony.lin@cs.uni-kl.de

14

Reino Niskanen

12

15
16

17

18
19
20
21
22
23
24
25
26
27
28
29
30
31

32
33
34

Department of Computer Science, University of Oxford, United Kingdom
reino.niskanen@cs.ox.ac.uk

Abstract
Monadic decomposibility — the ability to determine whether a formula in a given logical theory canbe decomposed into a boolean combination of monadic formulas — is a powerful tool for devising adecision procedure for a given logical theory. In this paper, we revisit a classical decision problem
in automata theory: given a regular (a.k.a. synchronized rational) relation, determine whether it isrecognizable, i.e., it has a monadic decomposition (that is, a representation as a boolean combinationof cartesian products of regular languages). Regular relations are expressive formalisms which,using an appropriate string encoding, can capture relations definable in Presburger Arithmetic. In
fact, their expressive power coincide with relations definable in a universal automatic structure;equivalently, those definable by finite set interpretations in WS1S (Weak Second Order Theory of
One Successor). Determining whether a regular relation admits a recognizable relation was known to
be decidable (and in exponential time for binary relations), but its precise complexity still hitherto
remains open. Our main contribution is to fully settle the complexity of this decision problem bydeveloping new techniques employing infinite Ramsey theory. The complexity for DFA (resp. NFA)
representations of regular relations is shown to be NLOGSPACE-complete (resp. PSPACE-complete).
2012 ACM Subject Classification Theory of computation → Regular languages; Theory of computation → Transducers; Theory of computation → Complexity classes; Theory of computation →Logic and verification; Theory of computation → Automated reasoning

36

Keywords and phrases Transducers, Automata, Synchronized Rational Relations, Ramsey Theory,
Variable Independence, Automatic Structures

37

Digital Object Identifier 10.4230/LIPIcs.ICALP.2019.98

38

Related Version A full version of the paper is available at https://arxiv.org/abs/1903.00728.

35

42

Funding Barceló is funded by the Millennium Institute for Foundational Research on Data (IMFD)
and Fondecyt grant 1170109. Le, Lin, and Niskanen are supported by the European ResearchCouncil (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant
agreement no 759969).

43

Acknowledgements We thank Leonid Libkin for the useful discussion.

39
40
41

EA

TC S

© Pablo Barceló, Chih-Duo Hong, Xuan-Bach Le, Anthony W. Lin and Reino Niskanen;
licensed under Creative Commons License CC-BY
46th International Colloquium on Automata, Languages, and Programming (ICALP 2019).
Editors: Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi;
Article No. 98; pp. 98:1–98:14
Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

98:2

Monadic Decomposability of Regular Relations

1

44

45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88

Introduction

Monadic decompositions for computable relations have been studied in many different guises,
and applied to many different problem domains, e.g., see [17, 25, 38, 12, 27, 28, 37]. The notionof “monadic decomposability” essentially captures the intuitive notion that the components ina given n-ary relation R ⊆ U n are sufficiently independent from (i.e. not tightly coupled, orinterdependent, with) each other. Some examples are in order. Given two subsets X, Y ⊆ U ,then X × Y is an instance of relations whose two components are completely independent
from each other. On the other hand, the equality relation {(x, x) : x ∈ U } is an example
of relations whose two components are tightly coupled. In this paper, we will adopt thecommonly studied notion of component-independence1 (e.g. [25, 38, 7, 37]) in a relation
R ⊆ U n that lies between the extremes as exemplified in the above examples, i.e., that R is
Sr
expressible as a finite union i=1 Xi,1 × · · · × Xi,n of products, where each Xi,j is expressible
in the same language L (e.g. a logic or a machine model) wherein R is expressed.
Why should one care about monadic decomposable relations? The main reason is that
applying appropriate monadic restrictions could make an undecidable problem decidable,
and in general turn a difficult problem into one more amenable to analysis. Several examples
are in order. Firstly, the well-known cartesian abstractions in abstract interpretation [17]overapproximate the set R ⊆ U n of reachable states at a certain program point by a relation
R0 ⊆ X1 × · · · × Xm such that R ⊆ R0 . Having R0 instead of R sometimes allows a static
analysis tool to prove correctness properties about a program that is otherwise difficult to dowith only R. Another example includes restrictions to monadic predicates in undecidable
logics that result in decidability, e.g., monadic first-order logic and extensions ([9, 10, 4]), as
well as monadic second-order theory of successors [10]. Monadic decomposability also foundapplications in more efficient variable elimination in constraint logic programming (e.g. [23]),
as well as constraint processing algorithms for constraint database queries (e.g. [25, 24]).
Finally, monadic decompositions in the context of SMT (Satisfiability Modulo Theories),whose study was recently initiated in [38], have numerous applications, including constraint
solving over strings [38, 14].
The focus of this paper is to revisit a classical problem of determining monadic decomposability of regular relations, which are also known as synchronized rational relations [20, 6, 8].
The study of classes of relations over words definable by different classes of multi-tape (finite)
automata is by now a well-established subfield of formal language theory. This study was
initiated by Elgot, Mezei, and Nivat in the 1960s [18, 30]; also see the surveys [7, 15]. In
particular, we have a strict hierarchy of classes of relations as follows: recognizable relations,synchronized rational relations, deterministic rational relations, and rational relations. All
these classes over unary relations (i.e. languages) coincide with the class of regular languages.
Rational relations are relations R ⊆ (Σ∗ )n definable by multi-tape automata, where the tapeheads move from left to right (in the usual way for finite automata) but possibly at different
speeds (e.g. in a transition, the first head could stay at the same position, whereas thesecond head moves to the right by one position). Deterministic rational relations are simply
those rational relations that can be described by deterministic multi-tape automata. So far,the heads of the tapes can move at different speeds. Regular relations (a.k.a. synchronizedrational relations) are those relations that are definable by multi-tape automata, all of whose
heads move to the right in each transition. Unlike (non)deterministic rational relations,
regular relations are extremely well-behaved, e.g., they are closed under first-order operations

1

Also called variable-independence.

P. Barceló et al.

126

and, therefore, have decidable first-order theories [22]. Regular relations are also known
to coincide with those relations that are first-order definable over a universal automatic
structure [6, 8]; equivalently, those relations that are definable by finite-set interpretations in
the weak-monadic theory of one successor (WS1S) [16]. Finally, the weakest class of relationsin the hierarchy are recognizable relations: those relations that are definable as a finite unionof products of regular languages or, equivalently, relations that can be defined as a boolean
combination of regular constraints (i.e. atomic formulas of the form x ∈ L, where L is aregular language, asserting that the word x is in L). Recognizable relations are, therefore,
those relations definable by multi-tape automata that exhibit monadic decomposability.
One of the earliest results on deciding whether a relation is monadic decomposable
follows from Stearns in 1967 [33] and the characterization of a binary relation R ⊆ A∗ × B ∗by LR = {rev(u)#v | (u, v) ∈ R}, where rev(u) is the mirror image of u. In [12] it wasproven that LR is a regular language if and only if R has a monadic decomposition and
if R is a deterministic rational relation, then LR is a deterministic context-free language.
Due to this characterization, Stearns’s result implies that whether a deterministic n-ary
rational relation is monadic decomposable (i.e. recognizable) is decidable in the case whenn = 2. Shortly thereafter, Fischer and Rosenberg [19] showed that the same problem isunfortunately undecidable for the full class of binary rational relations. A few years later
Valiant [37] improved the upper bound complexity for the case solved by Stearns to double
exponential-time. This is still the best known upper bound for the monadic decomposability
problem for deterministic binary rational relations to date and, furthermore, no specific lower
bounds are known. More recently Carton et al. [12] adapted the techniques from [33, 37]
to show that this decidability extends to general n-ary relations, though no complexity
analysis was provided. The problem of monadic decomposability for regular relations has
also been studied in the literature. Of course decidability with a double exponential-time
upper bound for the binary case follows from [37]. In 2000 Libkin [25] gave general conditions
for monadic decomposability for first-order theories, which easily implies decidability formonadic decomposability for general k-ary regular relations. This is because regular relations
are simply those relations that are definable in a universal automatic structures [6, 8]. The
result of Libkin was not widely known in the automata theory community and in fact the
problem was posed as an open problem in French version of [31] in 2003 and later on, Carton
et al. [12] provided a double-exponential-time algorithm for deciding whether an n-ary
regular relation is monadic decomposable. More precisely, even though it was claimed in thepaper that the algorithm runs in single-exponential time, it was noted in a recent paper by
Löding and Spinrath [27, 28] (with which the authors of [12] also agreed, as claimed in [28])that the algorithm actually runs in double-exponential time. Löding and Spinrath [27, 28]
gave a single-exponential-time algorithm (inspired by techniques from [37]) for monadic
decomposability of binary regular relations.

127

Contributions

89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125

128
129
130

131
132

133
134

98:3

In this paper we provide the precise complexity of monadic decomposability of regular
relations, closing the open questions left by Carton et al. [12] and Löding and Spinrath[27, 28]. In particular, we show the following.
I Theorem 1. Deciding whether a given regular relation R is monadic decomposable is
NLOGSPACE-complete (resp. PSPACE-complete), if R is given by a DFA (resp. an NFA).
The lower bounds hold already for binary relations (Lemma 5 and Lemma 6 in Section 3).
To prove the upper bounds, we first prove the upper bounds for binary relations (Lemma 10

ICALP 2019

98:4

Monadic Decomposability of Regular Relations

135
136
137
138
139
140
141

in Section 4) and then extend them to n-ary relations for any given n > 2 (Lemma 11 in
Section 5).
The existing proof techniques (e.g. in [12, 28, 25]) for deciding monadic decomposability
typically aim for finding proofs that the relations are monadic decomposable. In contrast,
our proof technique relies on finding a proof that a relation is not monadic decomposable. Asa brief illustration, suppose we want to show that the regular relation R = {(v, v) : v ∈ Σ∗ }is not monadic decomposable. We define an equivalence relation ∼ ⊆ Σ∗ × Σ∗ asx ∼ y := ∀z([R(x, z) ↔ R(y, z)] ∧ [R(z, x) ↔ R(z, y)]).

142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168

169

170
171
172
173
174
175
176
177
178
179
180
181

This relation is regular since regular relations are closed under first-order operations [31] (afact that was also used in [12]), but the size of the automaton for this relation is unfortunately
quite large; see [27] for detailed discussion. Therefore, we will only use the complement 6∼,
which has a substantially smaller representation: polynomial (resp. exponential) size if R isgiven as a DFA (resp. an NFA). Now, that R is not monadic decomposable amounts to theexistence of an ω-sequence σ = {vi }i∈N of words such that vi 6∼ vj for each pair i, j ∈ N. By
applying the pigeonhole principle and König’s lemma, we will first construct a nicer sequenceα (see the top half of Figure 2) and then by exploiting Ramsey Theorem over infinite graphs,
we will show that there is an even nicer sequence α0 (see the bottom half of Figure 2), where
the automaton for 6∼ synchronizes its states in particular points of the computation, no
matter which pair of words from the sequence is being read. Moreover, we prove that one of
the synchronizing states has a pumping property. This leads to our NLOGSPACE algorithm
as we can guess the synchronizing states and verify that there is an accepting run that canbe pumped. This technique was inspired by a technique for proving recurrent reachability inregular model checking [34, 35].
The exponential-time upper bound for the binary case from Löding and Spinrath [28](which is inspired by the techniques used by Stearns [33] and Valiant [37]) relied on characterization of a relation R using the language LR = {rev(u)#v | (u, v) ∈ R} and useda suitable machinery that is able to decide whether LR is regular or not. Their result is
not easily extensible to n-ary relations as the encoding of a binary rational relation as acontext-free language LR does not generalize to n-ary relations. In Section 5, we show thatproving monadic decomposability for an n-ary regular relation is LOGSPACE-reducible totesting whether linearly many induced binary relations are monadic decomposable.
We conclude in Section 6 with some perspectives from formal verification and a future
research direction. The proofs omitted due to length constraints can be found in [5].

2Preliminaries

A finite alphabet is denoted by Σ and the free monoid it generates by Σ∗ . That is, Σ∗consists of all finite words over Σ. The empty word is ε. We denote by |w| the length ofword w ∈ Σ∗ . We have that |ε| = 0. The word u ∈ Σ∗ is a prefix of w ∈ Σ∗ if w = uv forsome v ∈ Σ∗ . We denote this by u ≤ w. We also write v = u−1 w, when u is a prefix of w, tostate that v is the suffix of w that is obtained after prefix u is removed. Sometimes we wantto consider a suffix of w after a prefix of particular length is removed without specifying
the actual prefix as defined above. To this end, we define partial function σ : Σ∗ × N → Σ∗such that σ(w, i) = v, where w = uv for some u ∈ Σ∗ such that |u| = i. In particular, foru ≤ w, σ(w, |u|) = u−1 w. Similarly, we define partial function τ : Σ∗ × N → Σ∗ such that
τ (w, i) = u, where |u| = i and u ≤ w.
In this paper we study relations R ⊆ Σ∗ × · · · × Σ∗ with particular structural properties.
Namely, monadic decomposable relations that are a finite union of direct products of regular

P. Barceló et al.

182
183

184
185
186

187
188
189
190
191
192
193
194
195
196
197

198
199

200
201
202
203
204
205
206
207

98:5

languages, and regular relations defined by n-tape finite automata, where the heads move insynchronized manner. See, for example, [31] for more details on such relations.
I Definition 2. An n-ary relation R ⊆ Σ∗ × · · · × Σ∗ is a monadic decomposable relation iff
Sm
it is of the form i=1 (X1,i × · · · × Xn,i ), where m is finite and each Xj,i ⊆ Σ∗ is a regular
language.
As mentioned earlier, this can be intuitively seen as the components of R being independent
in some sense. Note that in the literature, monadic decomposable relations are sometimes
called recognizable. The monadic decomposable relations can be defined using multi-tapeautomata as is done, e.g., in [12]. The above definition is more suitable for our considerations.
Let ⊥ be a fresh symbol not found in Σ. We use it to pad words in a relation R ⊆Σ∗ × · · · × Σ∗ in order for each component to be of the same length. Formally, a tuple(w1 , . . . , wn ) is transformed into (w1 ⊥`1 , . . . , wn ⊥`n ), where `i = −|wi | + max1≤j≤n |wj |for each i = 1, . . . , n. We extend this to the relation R⊥ in the expected way. We also
denote Σ ∪ {⊥} by Σ⊥ . An n-tape automaton over alphabet Σ⊥ is a tuple (Q, →A , q0 , F ),where Q is the finite set of states, q0 is the initial state, F is the set of final states, and→A ⊆ Q × (Σ⊥ )n × P(Q).
I Definition 3. An n-ary relation R ⊆ Σ∗ × · · · × Σ∗ is regular iff R⊥ is recognized by somen-tape automaton A⊥ over alphabet Σ⊥ .
That is, in a regular relation the n heads of the automaton are moving in synchronizedmanner and the n-tuple of symbols seen determines the state transition. Naturally, the statetransition can be deterministic or non-deterministic. We say that a regular relation is definedby an NFA if the underlying n-tape automaton is non-deterministic, otherwise we say thatthe relation is defined by a DFA. Note that in the literature, regular relations are sometimes
called synchronous rational or automatic relations.
We recall a useful characterization from [12]. Consider an n-ary regular relation R ⊆Σ∗ × · · · × Σ∗ . For each j = 1, . . . , n − 1, let ∼j be the following induced equivalence relation:

208(u1 , . . . , uj ) ∼j (v1 , . . . , vj ) := ∀(wj+1 , . . . , wn ) ∈ Σ∗ × · · · × Σ∗ we have that
(u1 , . . . , uj , wj+1 , . . . , wn ) ∈ R ⇐⇒ (v1 , . . . , vj , wj+1 , . . . , wn ) ∈ R and209(wj+1 , . . . , wn , u1 , . . . , uj ) ∈ R ⇐⇒ (wj+1 , . . . , wn , v1 , . . . , vj ) ∈ R.

210
211
212
213
214

215
216

I Lemma 4 ([12]). The n-ary regular relation R is monadic decomposable iff ∼j has finite
index for each j = 1, . . . , n − 1. That is, there are finitely many equivalence classes over ∼j .
In other words, R is not monadic decomposable iff for some j = 1, . . . , n − 1, there is an
infinite sequence {ui }i≥0 , where each ui is a j-tuple of words, such that for each 0 ≤ i < ` itis the case that ui 6= u` and ui 6∼j u` .
In Section 4, we focus on binary relations for which we simplify the notation as there is
only one possible value of j. We write ∼ instead of ∼j and R6∼ for the binary regular relation

217
218
219
220

221
222
223
224
225

R6∼ (w, w0 ) := ∃u (R(w, u) ∧ ¬R(w0 , u)) ∨ (¬R(w, u) ∧ R(w0 , u)) ∨(R(u, w) ∧ ¬R(u, w0 )) ∨ (¬R(u, w) ∧ R(u, w0 )) .
That is, R6∼ consists of all words w, w0 ∈ Σ∗ for which there exists a word u ∈ Σ∗ such that
one of R(w, u) and R(w0 , u) is accepted while the other is not, or one of R(u, w) and R(u, w0 )is accepted while the other is not.
We assume that the reader is familiar with complexity classes and logarithmic space
reductions via logarithmic space transducers; see for example [32].

ICALP 2019

98:6

Monadic Decomposability of Regular Relations

226

227
228
229

230
231

232
233
234
235
236
237

3

In this section, we consider binary regular relations given by NFA and provide a PSPACE
lower bound for deciding if such a relation is monadic decomposable. Then, we prove thatthe same problem for DFA is NLOGSPACE-hard.
I Lemma 5. The problem of deciding whether a binary regular relation given by an NFA ismonadic decomposable is PSPACE-hard.
Proof. We give a logarithmic space reduction from the universality problem for NFA, which
is PSPACE-hard [29]. Recall that in this problem, we are asked to decide whether L(A) = Σ∗given an NFA A over Σ.
Let A be an NFA over alphabet Σ, and let {#} be a fresh symbol that we will use as aseparator symbol. We assume that # 6= ⊥. We construct relation R = R1 ∪ R2 using thelanguage L of A, where
R1 = {(u, u) | u ∈ (Σ ∪ {#})∗ }

238
239

240
241
242
243
244
245
246
247
248
249
250
251
252
253

254
255

256
257

258

259

260
261

262
263
264
265
266

Hardness of deciding monadic decomposability of regular relations

andR2 = (L · {#})∗ × (Σ∗ · {#})∗ .

Intuitively, R1 contains all pairs (w1 , w2 ) such that w1 = w2 = u0 #u1 # · · · #un #, whereui ∈ Σ∗ , and R2 contains all pairs (w1 , w2 ) such that w1 = v0 #v1 # · · · #vm #, where vi ∈ L,
and w2 = u00 #u01 # · · · #u0n #, where u0i ∈ Σ∗ . It is easy to construct an NFA that recognizes
R in LOGSPACE. Next we show that L = Σ∗ iff R is monadic decomposable.
Assume first that L = Σ∗ . Then R1 ⊆ R2 , and thus R = (Σ∗ · {#})∗ × (Σ∗ · {#})∗ which
has a trivial monadic decomposition.
Sn
For the other direction, assume that R is monadic decomposable, i.e., R = i=1 (Ai × Bi )for some regular languages Ai , Bi . Let w ∈ Σ∗ . We show that w ∈ L as well. Consider
a set {((w#)i , (w#)i ) | i = 1, . . . , n + 1} ⊆ R1 ⊆ R. By the pigeonhole principle, there
are two elements ((w#)j , (w#)j ) and ((w#)k , (w#)k ) that belong to the same componSn
ent of i=1 (Ai × Bi ), say to A1 × B1 . Therefore, (w#)j ∈ A1 and (w#)k ∈ B1 , andhence their direct product, ((w#)j , (w#)k ), is in A1 × B1 ⊆ R. Recall that R = R1 ∪ R2 .
Clearly, ((w#)j , (w#)k ) ∈/ R1 as the lengths of the two words are different. It follows that((w#)j , (w#)k ) ∈ R2 and hence (w#)j ∈ (L · {#})∗ . This implies that w ∈ L.
J
I Lemma 6. The problem of deciding whether a binary regular relation given by a DFA ismonadic decomposable is NLOGSPACE-hard.
The proof is straightforward by a reduction from reachability problem for directed acyclic
graphs.

4

Deciding monadic decomposability of binary regular relations

In this section we prove our main technical result.
I Lemma 7. There is an NLOGSPACE algorithm that takes as input an NFA for R6∼ , where
R is a binary regular relation, and decides whether R is monadic decomposable.
We start by defining some notation. We assume any binary regular relation R6∼ to begiven as an NFA with set of states Q. The R6∼ -type of a pair (w1 , w2 ) of words over Σ is anelement of the transition monoid. Recall that the transition monoid transforms any given
6∼
state q ∈ Q to a set Q0 ⊆ Q of states when reading (w1 , w2 ). We denote this by Rw
(q)
1 ,w2
for each q ∈ Q. We write types(R6∼ ) for the set of all R6∼ -types.

P. Barceló et al.

267
268
269
270
271
272
273
274

275
276

277
278
279
280
281
282

98:7

Consider an infinite sequence {wi }i≥0 of words over Σ as defined in Lemma 4. Additionally,
we assume that the words in the sequence are of strictly increasing length and that for eachi > 0 the words wi and wi+1 have a common prefix of length |wi−1 |. That is, wi can be
written as β0 · · · βi−1 αi , where each βj and αi is a non-empty word. To simplify notation,
we denote ρ(wi ) = β0 · · · βi . That is, ρ(wi ) is of length |wi | and is a prefix of wj , for each0 ≤ i < j. We will show how to construct such sequence in Proposition 8. The words wi , wj
and wk are illustrated in the top of Figure 1.
With each pair (i, j), where i < j, we associate the following quinary tuple over types(R6∼ ):

6∼
6∼
6∼
6∼
6∼
Ci,j = Rw, Rρ(w, Rσ(w, Rε,σ(w, Rε,σ(ρ(w.
i ,ρ(wi )i ),ρ(wi )j ,|wi |),σ(ρ(wj ),|wi |)j ,|wi |)j ),|wi |)Intuitively, the first component corresponds to the computation of (β0 · · · βi−1 αi , β0 · · · βi−1 βi ),the second to (β0 · · · βi−1 βi , β0 · · · βi−1 βi ) needed in order to compute the third component, (βi+1 · · · βj−1 αj , βi+1 · · · βj−1 βj ). The final two components are used to compute theset of states reachable after the whole word in the first component is read. That is(⊥|βi+1 ···βj−1 αj | , βi+1 · · · βj−1 αj ) and (⊥|βi+1 ···βj−1 βj | , βi+1 · · · βj−1 βj ). See Figure 1 for a
pictorial depiction.
wi
wj
wk

β0 · · · βi−1 αi
β0 · · · βi−1 βi βi+1 · · · βj−1 αj
β0 · · · βi−1 βi βi+1 · · · βj−1 βj · · ·β0 · · · βi−1 αi
β0 · · · βi−1 βi

β0 · · · βi−1 βi
β0 · · · βi−1 βi

βi+1 · · · βj−1 αjβi+1 · · · βj−1 βj⊥···⊥
βi+1 · · · βj−1 αj⊥···⊥βi+1 · · · βj−1 βj

1st component

2nd component

3rd component

4th component

5th component

Figure 1 Correspondence between components of Ci,j and parts of computation on wi , wj andwk , where i < j < k.
283
284
285
286
287

288
289
290
291
292
293
294

295
296
297
298
299
300
301
302
303

We can then establish the following important proposition. Consider an infinite sequenceof words that are pairwise from different equivalence classes as in Lemma 4. We show nextthat we can extract an infinite subsequence with additional structural properties. Perhaps
the most important property is that Ci,j is the same for all i, j. This subsequence will allow
us to prove the main lemma.
I Proposition 8. A binary regular relation R over Σ∗ × Σ∗ is not monadic decomposable
iff there are infinite sequences {ui }i≥0 , {γi }i≥0 , and {δi }i≥0 of words over Σ and a quinary
tuple C over types(R6∼ ) such that for each i ≥ 0 it is the case that
1. |γi | = |δi | > 0,
2. ui = δ0 · · · δi−1 γi ,3. (ui , uj ) ∈ R6∼ , for each j > i, and4. Ci,j = C, for each j > i.
Proof. By Lemma 4, the existence of such sequences directly implies that the relation is notmonadic decomposable. Assume then that R is not monadic decomposable. By Lemma 4,
there exists a sequence {vi }i≥0 such that R6∼ (vj , v` ) for all j 6= `. It remains to show how toconstruct the three sequences satisfying the additional properties from {vi }i≥0 . First, weconstruct an auxiliary sequence {wi }i≥0 in the following way. Let vj be the first non-empty
word of {vi }i≥0 . Denote vj = w00 = α0 . Consider prefixes of vi of length |α0 |. Since |α0 |is finite and the sequence is infinite, there exists a prefix that appears infinitely often by
the pigeonhole principle. Denote this prefix by β0 . Now we consider an infinite subsequence{wi0 }i≥0 of {vi }i≥0 where w00 = vj and wi0 , where i > 0, has β0 as the proper prefix. We can

ICALP 2019

98:8

Monadic Decomposability of Regular Relations

304
305
306
307
308
309
310
311
312
313
314
315
316
317

318
319
320
321

write w10 = β0 α1 and repeat the procedure. By König’s Lemma, we can always repeat theprocedure and obtain the desired auxiliary sequence {wi }i≥0 in the limit.
From Infinite Ramsey’s Theorem, there is an infinite sequence 0 ≤ `0 < `1 < · · · and atuple C ∈ types(R6∼ )5 such that for each 0 ≤ i < j we have C`i ,`j = C. Namely, we consider acomplete infinite graph with natural numbers as vertices. An edge between vertices i and jis coloured with Ci,j ∈ types(R6∼ )5 . Now there is an infinite clique coloured with C which
gives us our infinite sequence 0 ≤ `0 < `1 < · · · .
We then define the ui s, γi s, and δi s, for i ≥ 0, as follows.
γ0 = w`0 and γi+1 , for i > 0, is the word σ(w`i+1 , |w`i |).
δi is defined as ρ(γi ).
ui = δ0 · · · δi−1 γi , for each i ≥ 0.
It is easy to see then that ui = w`i and ρ(ui ) = δ0 · · · δi−1 δi = ρ(w`i ), for each i ≥ 0.
Therefore, {ui }i≥0 , {γi }i≥0 , {δi }i≥0 , and C satisfy the conditions in the statement of the
proposition. See Figure 2 for a pictorial depiction of the construction.
J
In other words, by Proposition 8, there is a sequence {ui }i≥0 and a C such that for eachi, j, the runs on R6∼ are synchronized after (γi , δi ), (δi , δi ), (δi−1 γj , δi−1 δj ), (ε, δi−1 γj ) and(ε, δi−1 δj ) have been read. In particular, the runs are synchronized in states of Rγ6∼i ,δi , Rδ6∼i ,δi ,6∼
6∼Rδ6∼−1 γ ,δ−1 δ , Rε,δand Rε,δ, respectively.
−1
−1
γ
δ
i

j

u0
u1
u2
u3
u4
u5
u6

..
.

i

j

i

j

j

i

α0
By thepigeonhole
principle−−−−−−→

u00
u01
u02
u03

..
.

α0
β0
β0
β0

w0
w1
w2
w3
w4
w5
w6

α1
By König’s
Lemma→ ··· →

..
.

..
.

..
.

α0
β0
β0
β0
β0
β0
β0

α1
β1 α2
β1 β2
β1 β2
β1 β2
β1 β2

α3
β3
β3
β3

..
.

α4
β4 α5
β4 β5 α6γ0By Infinite
Ramsey’s Theorem−−−−−−−−−−−−→

w`0
w`1
w`2
w`3
w`4
w`5
w`6

β0
β0
β0
β0
β0
β0
β0

..
.

γ1

β1 α2
β1 β2
β1 β2
β1 β2
β1 β2
β1 β2
β1 β2

α3
β3
β3
β3
β3
β3

β4 α5
β4 β5
β4 β5
β4 β5
β4 β5

δ0

δ1

δ2

γ2
γ2
γ3

β6 α7
β6 β7 β8
β6 β7 β8
β6 β7 β8

α9
β9
β9

δ2

γ4
γ5
β10 β11 α12β10 β11 β12 α13

δ3

..
.

δ4

Figure 2 An illustration of construction of sequence {ui }i≥0 of Proposition 8 in two steps. HereR6∼ (ui , uj ), R6∼ (u0i , u0j ) and R6∼ (wi , wj ) for every i 6= j. Moreover as C = Ci,j , the sets of states
reachable after each δi and γi are the same (indicated by thick lines).
322
323
324

325
326
327

328
329

We can then prove the following crucial result. We assume here that R is a binary regular
relation over Σ × Σ such that R6∼ is given as an NFA over Σ × Σ whose set of states is Q.
We further assume that q0 is the initial state of R6∼ and F its set of final states.
I Lemma 9. Relation R is not monadic decomposable iff there are an infinite sequence{(xi , yi )}i≥0 of pairs of words over Σ and states q, q 0 , p, r ∈ Q, such that p ∈ F , it is the casethat q ∈ Rx6∼0 ,y0 (q0 ), and the following statements hold for each i ≥ 0.
1. |xi | = |yi | and yi is a prefix of both xi+1 and yi+1 .
6∼
2. q 0 ∈ Ry6∼i ,yi (q0 ); q ∈ Ry6∼−1 x ,y−1 y (q 0 ); p ∈ Rε,y
−1
x
i

330

i+1

i

i+1

6∼
3. If i > 0, we also have that p ∈ Rε,y
−1
x
i

i

i+1

(q);
i+1

6∼
(r) and r ∈ Rε,y
−1
y
i

6∼
r ∈ Rε,y
−1
y
i

(r).
i+1

(q).
i+1

P. Barceló et al.

331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349

98:9

Proof. Assume first that R is not monadic decomposable. By Proposition 8, there areinfinite sequences {ui }i≥0 , {γi }i≥0 , and {δi }i≥0 of words over Σ and a quinary tuple C overtypes(R6∼ ) such that for each i ≥ 0 it is the case that
1. |γi | = |δi | > 0,
2. ui = δ0 · · · δi−1 γi ,3. (ui , uj ) ∈ R6∼ , for each j > i, and4. Ci,j = C, for each j > i.
We then define a sequence {(xi , yi )}i≥0 such that xi := ui , for each i ≥ 0, and yi is theprefix of xi+1 = ui+1 that has the same length as xi = ui , i.e., yi = τ (xi+1 , |xi |). Hence,yi = ρ(ui ) = δ0 · · · δi . Clearly, |xi | = |yi | ≥ 0 and yi is a prefix of both xi+1 and yi+1 , for eachi ≥ 0. We prove next that the sequence {(xi , yi )}i≥0 also satisfies the remaining conditions.
Before defining q, q 0 , p, r ∈ Q, let us highlight the intuition why such states exist forevery i. We can find such states because by our assumption Ci,j = C for each i < j. Further,whether q is reachable from q0 is stored in the first component of C. Similarly, the second
and third components of C allow us to find q 0 that is reachable from q0 and such that q isreachable from q 0 . Finally, the fourth component is for checking whether p is reachable fromq and r, while the fifth component for checking that r is reachable from both q and r.
Let us define q, q 0 , p, r ∈ Q as follows.
6∼
q and p are states such that p ∈ F and it is the case that q ∈ Rx6∼0 ,y0 (q0 ) and p ∈ Rε,y
(q).
−1
x
1

0

350
351

Notice that such q and p must exist as (x0 , x1 ) ∈ R6∼ , i.e., it holds that Rx6∼0 ,x1 (q0 ) ∩ F 6= ∅,6∼
and Rx6∼0 ,x1 (q0 ) = Rx6∼0 ,y0 (q0 ) ◦ Rε,y
.
−1
x
1

0

352

q 0 is a state such that q 0 ∈ Ry6∼0 ,y0 (q0 ) and q ∈ Ry6∼−1 x ,y−1 y (q 0 ). Notice that such a q 0 must353

exist. Indeed, since C0,1 = C1,2 = C, we have Ru6∼0 ,ρ(u0 ) = Rx6∼0 ,y0 = Ru6∼1 ,ρ(u1 ) = Rx6∼1 ,y1 .

354This implies that q ∈ Rx6∼1 ,y1 (q0 ) = Ry6∼0 ,y0 (q0 )◦Ry6∼−1 x ,y−1 y , as we know that q ∈ Rx6∼0 ,y0 (q0 )

0

0

355
356

357
358
359

360
361
362

363
364

365

1

0

1

0

1

1

and there must be an intermediate state q 0 that is reached after reading (y0 , y0 ).
We have that r is a state such that6∼(q);r ∈ Rε,y
−1
y
0

1

6∼
(r);
p ∈ Rε,y
−1
x
1

6∼
(r).
r ∈ Rε,y
−1
y

and

2

1

The existence of such state r is not obvious but straightforward; see [5].
We now prove that q, q 0 , p, r satisfy all the requirements in the statement of the Lemma.
By definition, q ∈ Rx6∼0 ,y0 (q0 ) and p ∈ F . We can then prove by induction that for each i ≥ 0
it is the case thatq 0 ∈ Ry6∼i ,yi (q0 );q ∈ Ry6∼−1 xi−1i+1 ,yi yi+1

(q 0 );

6∼p ∈ Rε,y
−1
x
i

(q);
i+1

6∼
and, in addition, that for each i > 0 it is the case that p ∈ Rε,y
−1
x
i

366
367
368
369
370
371
372
373
374
375
376

2

6∼
r ∈ Rε,y
−1
y
i

i+1

(q);
i+1

6∼
(r) and r ∈ Rε,y
−1
y
i

(r).

i+1

The base case i = 0 holds by definition. The inductive case is straightforward.
Let us assume now that there are an infinite sequence {(xi , yi )}i≥0 of pairs of words
over Σ and states q, q 0 , p, r ∈ Q that satisfy the conditions stated in the statement of thelemma. We prove next that R is not monadic decomposable by showing that there areinfinite sequences {wi }i≥0 , {αi }i≥0 and {βi }i≥0 of words over Σ such that {wi }i≥0 , {αi }i≥0 ,and {βi }i≥0 satisfy the conditions stated in Lemma 4.
We define wi := xi for each i ≥ 0. Furthermore, α0 := x0 , β0 := y0 , and for each i > 0−1−1
we set αi := yi−1
xi and βi := yi−1
yi . Clearly |αi | = |βi | > 0 and wi = xi = β0 · · · βi−1 αi ,for each i ≥ 0. We prove next that (wi , wj ) ∈ R6∼ for each 0 ≤ i < j. Actually, we prove a6∼
6∼stronger claim: p ∈ Rw
(q0 ) and r ∈ Rw
(q0 ), for each 0 ≤ i < j, where as beforei ,wji ,ρ(wj )ρ(wj ) = τ (wj+1 , |wj |) = β0 β1 · · · βj . The claim can be proved by induction.
J

ICALP 2019

Monadic Decomposability of Regular Relations

q0(yi , yi )q0

(yi−1 xi+1 , yi−1 yi+1 )(ε, yi−1 xi+1 )

q

p

1 i+
− y

(ε,
y−

yi
(ε,

i+ 1
1x
i+
2)

98:10

)

1

r

−1
(ε, yi+1
yi+2 )

Figure 3 Runs in R6∼ on states q, q 0 , p and r as defined in Lemma 9. The runs exist for everyi ≥ 0.

377
378
379
380

381
382
383
384
385
386
387
388

The runs as extracted from the sequence {(xi , yi })i≥0 satisfying the conditions of Lemma 9
are depicted in Figure 3.
Lemma 9 allows us to reduce the monadic decomposability problem to a set of reachability
checks on types. With the help of this property, we can then prove Lemma 7.
Proof of Lemma 7. For each (q, q 0 , p, r) ∈ Q × Q × Q × Q with p ∈ F do the following.
Check if there are words w0 , v0 , w1 , v1 such that |w0 | = |v0 | > 0, |w1 | = |v1 | > 0, and it
6∼
6∼
holds that (i) q ∈ Rw
(q0 ), (ii) q 0 ∈ Rv6∼0 ,v0 (q0 ), (iii) q ∈ Rw
(q 0 ), (iv) q 0 ∈ Rv6∼1 ,v1 (q 0 ),
0 ,v0
1 ,v1
6∼
6∼
(v) p ∈ Rε,w1 (q), and (vi) r ∈ Rε,v1 (q).
6∼
Check if there are words w, v such that |w| = |v| > 0, and it holds that (i) q ∈ Rw,v
(q 0 ),
6∼
6∼
6∼
6∼
6∼
(ii) q 0 ∈ Rv,v
(q 0 ), (iii) p ∈ Rε,w(q), (vi) r ∈ Rε,v(q), (v) p ∈ Rε,w(r), and (vi) r ∈ Rε,v(r).
If this holds for any such a tuple, then R is not monadic decomposable. Else, R is monadic
decomposable. It is easy to see that this algorithm can be implemented in NLOGSPACE. J
We have the necessary ingredients to prove a part of Theorem 1.

389

390
391

392
393
394
395
396
397
398
399
400

401

402
403
404

405
406

407
408

I Lemma 10. Deciding whether a given binary regular relation R is monadic decomposable
is in NLOGSPACE (resp. in PSPACE), if R is given by a DFA (resp. an NFA).
Proof. The claim follows from Lemma 7. Namely, from the definition of R6∼ , it follows that,
if R is given by a DFA, then R6∼ can be constructed in LOGSPACE. Indeed, this can be done
as disjunctions, conjunctions and projections can all be done in LOGSPACE and then via
composability of LOGSPACE transducers we can construct R6∼ of logarithmic size. (Note thatthe output of a LOGSPACE transducer is of at most polynomial size.) Then by Lemma 7, we
obtain the decidability of monadic decomposability in NLOGSPACE for R given by a DFA.
Similarly, if R is given by an NFA, we construct R6∼ of polynomial size since an NFA
can be transformed into a DFA using a PSPACE transducer. (Again, the output of a PSPACE
transducer is of at most exponential size.) Thus monadic decomposability is in PSPACE. J

5

Deciding monadic decomposability of regular relations

In this section, we finish the proof of Theorem 1. The remaining component is showing thatmonadic decomposability of n-ary regular relations is decidable in NLOGSPACE for DFA andPSPACE for NFA.
I Lemma 11. Deciding whether a given n-ary regular relation R is monadic decomposable
is in NLOGSPACE (resp. in PSPACE), if R is given by a DFA (resp. an NFA).
Proof of Theorem 1. The upper bounds follow from Lemma 11 and the lower bound follows
from Lemma 5 for NFA and from Lemma 6 for DFA.
J

P. Barceló et al.

409
410
411
412
413
414
415
416
417
418
419

420

421

98:11

In order to prove Lemma 11, we extend Lemma 10 to n-ary relations. Let us first definesome helpful notation used throughout the section.
Recall that words of regular relations are padded to be of the same length using ⊥.
We denote this function by PAD⊥ . For example, PAD⊥ ((a, ε, ab)) = (a⊥, ⊥⊥, ab). Let
us now define a padding function δn that acts slightly differently. Instead of padding thewords in a tuple to make them of the same length, the new function pads a sequence oftuples with tuples where some elements are ⊥. Let us describe δn in more details. DefineΣn = (Σ⊥ )n \ {⊥n }, i.e., an alphabet consisting of n-tuples of letters from Σ⊥ , excluding(⊥, . . . , ⊥). Now δn : (Σ∗ )n → Σ∗n is an injective mapping that uses ⊥ to extend the shorterwords to the same length as the longest word. For example, δ3 maps (a, ε, ab) ∈ (Σ∗ )3 to(a, ⊥, a)(⊥, ⊥, b) ∈ Σ∗3 as follows:   
a
a⊥
a
⊥







(a, ε, ab) →−− ⊥⊥ →− ⊥− (a, ⊥, a)(⊥, ⊥, b).
ε →
⊥ →
ab
ab
a
b

426

I Lemma 12. For n ≥ 1, {(x1 , . . . , xn , y) | δn (x1 , . . . , xn ) = y} ⊆ (Σ∗ )n × Σ∗n is regular.
Pm
Given an n-ary relation R ⊆ (Σ∗ )n and positive integers x1 , . . . , xm such that i=1 xi = n,an m-ary relation Rx1 ,...,xm ⊆ Σ∗x1 × · · · × Σ∗xm can be uniquely determined via the mappings
δx1 , . . . , δxm . More precisely, there exists a one-to-one correspondence ∆x1 ,...,xm between
relations R and Rx1 ,...,xm that maps each (w1 , . . . , wn ) ∈ R to

428
427

(δx1 (w1 , . . . , wx1 ), δx2 (wx1 +1 , . . . , wx1 +x2 ), . . . , δxm (wx1 +···+xm−1 +1 , . . . , wn )) ∈ Rx1 ,...,xm .

422

423
424
425

429
430
431
432
433
434
435

436
437

438
439
440
441
442
443
444
445
446

447
448

449
450
451
452

For example, a ternary relation R = {(a, ε, ab)} over (Σ∗ )3 uniquely determines a binary
relation R1,2 = {(a, (⊥, a)(⊥, b))} over Σ∗1 × Σ∗2 through the correspondence ∆1,2 . For thesake of readability, if the integers x1 , . . . , xm have a constant subsequence of length k, i.e.,
xi = xi+1 = · · · = xi+k−1 for some i, we write the relation as Rx1 ,...,xi−1 ,xki ,xi+k ,...,xm .
In the following, we shall use Rk to denote the binary relation Rk,n−k induced by R. It
turns out that being able to check monadic decomposability for binary relations is sufficient
to check monadic decomposability for general n-ary relations.
I Lemma 13. Let R be an n-ary regular relation and let R1 , . . . , Rn−1 be the induced binary
relations. Then R is monadic decomposable iff R1 , . . . , Rn−1 are monadic decomposable.
Proof. Define δi (S) = {δi (s1 , . . . , si ) | (s1 , . . . , si ) ∈ S}. The only-if part of the lemma isSS
immediate, since R = i Xi,1 × · · · × Xi,n implies that Rk = i δk (Xi,1 × · · · × Xi,k ) ×δn−k (Xi,k+1 × · · · × Xi,n ) for 1 ≤ k ≤ n − 1, namely, R1 , . . . , Rn−1 are monadic decomposable.
To see the other direction, we say that an n-ary relation R is k-decomposable if theinduced k-ary relation R1k−1 ,n−k+1 of R is monadic decomposable. Now it suffices toshow that R is n-decomposable since R = R1n . We shall prove this by induction onk ∈ {2, . . . , n}. Note that R is 2-decomposable by the assumption that R1 is monadic
S
decomposable. For 2 ≤ k ≤ n − 1, suppose that Rk = j Aj × Bj and R is k-decomposable,S
say R1k−1 ,n−k+1 = i Xi,1 × · · · × Xi,k−1 × Yi . Then R is (k + 1)-decomposable as we have[ [R1k ,n−k =Xi,1 × · · · × Xi,k−1 × Ai,j × Bj ,ijwhere Ai,j = {x ∈ Σ∗ | ∃x1 ∈ Xi,1 · · · ∃xk−1 ∈ Xi,k−1 . δk (x1 , . . . , xk−1 , x) ∈ Aj }, i.e., Ai,j isthe projection of δk−1 (Aj ) ∩ (Xi,1 × · · · × Xi,k−1 × Σ∗ ) on the k-th component. Note thatδk−1 (Aj ) is regular since Aj and {(x1 , . . . , xk , y) | δk (x1 , . . . , xk ) = y} are regular (cf. [8]).
Hence Ai,j is also regular. The claim that R is n-decomposable then follows by induction. J

ICALP 2019

98:12

453
454
455
456
457
458

459

460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477

478
479

480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498

Monadic Decomposability of Regular Relations

Proof (sketch) of Lemma 11. To prove the lemma, we show that if R is regular, then so
are the induced relations R1 , . . . , Rn−1 . Moreover, given the automaton of R, one canconstruct the automaton for each Ri in logarithmic space from R. We then check if each Ri
is monadic decomposable for i = 1, . . . , n − 1. From Lemma 10 the latter is in NLOGSPACE(resp. PSPACE), and thus the whole procedure is in NLOGSPACE (resp. PSPACE) if R is given
by a DFA (resp. an NFA).
J

6Concluding Remarks

Monadic decomposability for rational relations (and subclasses thereof) is a classical problem
in automata theory that dates back to the late 1960s (the work of Stearns [33] and Fischer andRosenberg [19]). While the general problem is undecidable, the subcase of regular relations(i.e. those recognized by synchronized multi-tape automata) provides a good balance between
decidability [25, 12] and expressiveness. The complexity of this subcase remained open for overa decade (exponential-time upper bound for the binary case [27, 28], double exponential-time
upper bound in the general case [12], and no specific lower bounds). This paper closes thisquestion by providing the precise complexity for the problem: NLOGSPACE (resp. PSPACE)
for DFA (resp. NFA) representations.
Some perspectives from formal verification and future work: Researchers fromthe area of formal verification have increasingly understood the importance of the monadic
decompositions techniques, e.g., see [38]. Directly pertinent to monadic decomposability of
regular relations is the line of work of constraint solving over strings, wherein increasingly
more complex string operations are needed and thus added to solvers [36, 3, 26, 1, 13, 2, 14].
As an example, let us take a look at the recent work of Chen et al. [14], which spells out
a string constraint language with semantic conditions for decidability that directly use thenotion of monadic decomposability of relations over strings. Loosely speaking, a constraint is
simply a sequence of program statements, each being either an assignment or a conditional:
S ::=y := f (x1 , . . . , xr ) | assert(g(x1 , . . . , xr )) | S; S

where f : (Σ∗ )r → Σ∗ is a partial string function and g ⊆ (Σ∗ )r is a string relation. The
meaning of a constraint is what one would expect in a program written in a standard
imperative programming language, which should support assignments and assertions. Notethat loops are not allowed in the language since their target application is symbolic executions(e.g. see [11]). They provided two semantic conditions for ensuring decidability, one of which
requires that each conditional g is effectively monadic decomposable. There is evidence(e.g. [21, 14]) that some form of length reasoning in g is indeed required for many applicationsof symbolic executions of string-manipulating programs, but much of the length constraints
could be (not yet fully automatically) translated to regular constraints. A potential applicationfor our results is therefore to provide support for complex string relations for g in the formof regular relations, which permit a rather expressive class of conditionals (e.g. some form oflength reasoning, etc.). Despite this, this application also highlights what is currently missingin the entire literature of monadic decomposability of rational relations: a study of the
problem of outputting the monadic decompositions of the relations, if monadic decomposable.
(In fact, this is also true of other logical theories before the recent work of Veanes et al. [38].)
What is the complexity of this problem with various representations of recognizable relations(e.g. finite unions of products, boolean combinations of regular constraints, etc.)? Although
our results provide a first step towards solving this function problem, we strongly believe
this to be a highly challenging open problem in its own right that deserves more attention.

P. Barceló et al.

References

499

500

1

501
502
503
504

2

505
506
507

3

508
509
510

4

511
512
513

5

514
515
516

6

517
518
519
520
521

7
8
9

522
523

10

524
525

11

526
527

12

528
529
530

13

531
532
533

14

534
535
536

15

537
538

16

539
540

17

541
542

18

543
544

19

545
546

20

547
548
549
550

98:13

21

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukás Holík,
Ahmed Rezine, and Philipp Rümmer. Flatten and conquer: a framework for efficient analysisof string constraints. In Proceedings of PLDI 2017, pages 602–617. ACM, 2017. doi:10.1145/
3062341.3062384.
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukás Holík,
Ahmed Rezine, and Philipp Rümmer. TRAU: SMT solver for string constraints. In Formal
Methods in Computer Aided Design, FMCAD 2018, 2018.
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer, and Jari Stenman. String constraints for verification. In Proceedings of CAV 2014,
volume 8559 of LNCS, pages 150–166. Springer, 2014. doi:10.1007/978-3-319-08867-9_10.
James Bailey, Guozhu Dong, and Anthony Widjaja To. Logical queries over views: Decidability
and expressiveness. ACM Trans. Comput. Log., 11(2):8:1–8:35, 2010. doi:10.1145/1656242.
1656243.
Pablo Barceló, Chih-Duo Hong, Xuan-Bach Le, Anthony W. Lin, and Reino Niskanen.
Monadic decomposability of regular relations. CoRR, abs/1903.00728, 2019. URL: https://arxiv.org/abs/1903.00728.
Michael Benedikt, Leonid Libkin, Thomas Schwentick, and Luc Segoufin. Definable relations
and first-order query languages over strings. J. ACM, 50(5):694–751, 2003. doi:10.1145/
876638.876642.
Jean Berstel. Transductions and Context-Free Languages. Teubner-Verlag, 1979.
Achim Blumensath. Automatic Structures. PhD thesis, RWTH Aachen, 1999.
George S. Boolos, John P. Burgess, and Richard C. Jeffrey. Computability and Logic. Cambridge
University Press, fifth edition, 2007.
Egon Börger, Erich Grädel, and Yuri Gurevich. The Classical Decision Problem. Springer,
1997.
Cristian Cadar and Koushik Sen. Symbolic execution for software testing: Three decades later.
Commun. ACM, 56(2):82–90, 2013. doi:10.1145/2408776.2408795.
Olivier Carton, Christian Choffrut, and Serge Grigorieff. Decision problems among themain subfamilies of rational relations. RAIRO – Theoretical Informatics and Applications,40(2):255–275, 2006. doi:10.1051/ita:2006005.
Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu. What is decidable
about string constraints with the ReplaceAll function. PACMPL, 2(POPL):3:1–3:29, 2018.
doi:10.1145/3158091.
Taolue Chen, Matthew Hague, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu. Decision
procedures for path feasibility of string-manipulating programs with complex operations.
PACMPL, 3(POPL):49:1–49:30, 2019. doi:10.1145/3290362.
Christian Choffrut. Relations over words and logic: A chronology. Bull. of the EATCS,
89:159–163, 2006.
Thomas Colcombet and Christof Löding. Transforming structures by set interpretations.
Logical Methods in Computer Science, 3(2), 2007. doi:10.2168/LMCS-3(2:4)2007.
Patrick Cousot and Radhia Cousot. Systematic design of program analysis frameworks. In
Proceedings of POPL 1979, pages 269–282, 1979. doi:10.1145/567752.567778.
Calvin C. Elgot and Jorge E. Mezei. On relations defined by generalized finite automata. IBM
J. Res. Dev., 9(1):47–68, 1965. doi:10.1147/rd.91.0047.
Patrick C. Fischer and Arnold L. Rosenberg. Multitape one-way nonwriting automata. J.
Comput. Syst. Sci., 2(1):88–101, 1968. doi:10.1016/S0022-0000(68)80006-6.
Christiane Frougny and Jacques Sakarovitch. Synchronized rational relations of finite and infinite words. Theor. Comput. Sci., 108(1):45–82, 1993. doi:10.1016/0304-3975(93)90230-Q.
Vijay Ganesh, Mia Minnes, Armando Solar-Lezama, and Martin C. Rinard. Word equations
with length constraints: What’s decidable? In Proceedings of HVC 2012, pages 209–226.
Springer, 2012. doi:10.1007/978-3-642-39611-3_21.

ICALP 2019

98:14551
552

Monadic Decomposability of Regular Relations

22
23

553
554

24

555
556

25

557
558
559

26

560
561
562

27

563
564
565

28

566
567
568

29

569
570
571
572
573

30
31
32

574
575

33

576
577

34

578
579

35

580
581

36

582
583
584

37

585
586
587

38

Bernard R. Hodgson. Decidabilite par automate fini. Ann. Sc. Math. Quebec, 7:39–57, 1983.
Jean-Louis Imbert. Redundancy, variable elimination and linear disequations. In Proceedingsof ILPS 1994, pages 139–153, 1994.
Gabriel Kuper, Leonid Libkin, and Jan Paredaens. Constraint Databases. Springer Publishing
Company, Incorporated, first edition, 2010.
Leonid Libkin. Variable independence, quantifier elimination, and constraint representations.
In Proceedings of ICALP 2000, volume 1853 of LNCS, pages 260–271. Springer, 2000. doi:
10.1007/3-540-45022-X\_23.
Anthony W. Lin and Pablo Barceló. String solving with word equations and transducers:
Towards a logic for analysing mutation XSS. In Proceedings POPL 2016, pages 123–136. ACM,
2016. doi:10.1145/2837614.2837641.
Christof Löding and Christopher Spinrath. Decision problems for subclasses of rational
relations over finite and infinite words. In Proceedings of FCT 2017, volume 10472 of LNCS,
pages 341–354. Springer, 2017. doi:10.1007/978-3-662-55751-8\_27.
Christof Löding and Christopher Spinrath. Decision problems for subclasses of rational
relations over finite and infinite words. Discrete Mathematics & Theoretical Computer Science,21(3), 2019. URL: https://dmtcs.episciences.org/5141.
Albert R. Meyer and Larry J. Stockmeyer. The equivalence problem for regular expressions
with squaring requires exponential space. In 13th Annual Symposium on Switching andAutomata Theory (SWAT 1972), pages 125–129. IEEE, 1972. doi:10.1109/swat.1972.29.
M. Nivat. Transduction des langages de Chomsky. Ann. Inst. Fourier, 18:339–455, 1968.
Jacques Sakarovitch. Elements of Automata Theory. Cambridge University Press, 2009.
Michael Sipser. Introduction to the Theory of Computation. Thomson Course Technology
Boston, second edition, 2006.
Richard Edwin Stearns. A regularity test for pushdown machines. Information and Control,
11(3):323–340, 1967. doi:10.1016/S0019-9958(67)90591-8.
A. W. To. Model Checking Infinite-State Systems: Generic and Specific Approaches. PhD
thesis, LFCS, School of Informatics, University of Edinburgh, 2010.
A. W. To and Leonid Libkin. Recurrent reachability analysis in regular model checking. In
LPAR, pages 198–213, 2008.
Minh-Thai Trinh, Duc-Hiep Chu, and Joxan Jaffar. S3: A symbolic string solver for vulnerability detection in web applications. In Proceedings of CCS 2014, pages 1232–1243. ACM, 2014.
doi:10.1145/2660267.2660372.
Leslie G. Valiant. Regularity and related problems for deterministic pushdown automata.
Journal of the ACM, 22(1):1–10, 1975. doi:10.1145/321864.321865.
Margus Veanes, Nikolaj Bjørner, Lev Nachmanson, and Sergey Bereg. Monadic decomposition.
Journal of the ACM, 64(2):1–28, 2017. doi:10.1145/3040488.