Reasoning on Data Words over Numeric Domains
Diego Figueira

Anthony W. Lin

diego.figueira@cnrs.fr
Univ. Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800
Talence, France

awlin@mpi-sws.org
TU Kaiserslautern
Max Planck Institute for Software Systems
Kaiserslautern, Germany

ABSTRACT
We introduce parametric semilinear data logic (pSDL) for reasoning about data words with numeric data. The logic allows parameters, and Presburger guards on the data and on the Parikh imageof equivalence classes (i.e. data counting), allowing us to capture
data languages like: (1) each data value occurs at most once in theword and is an even number, (2) the subset of the positions containing data values divisible by 4 has the same number of a’s andb’s, (3) the data value with the highest frequency in the word isdivisible by 3, and (4) each data value occurs at most once, andthe set of data values forms an interval. We provide decidability
and complexity results for the problem of membership and satisfiability checking over these models. In contrast to two-variable
logic of data words and data automata (which also permit a form ofdata counting but no arithmetics over numeric domains and haveincomparable inexpressivity), pSDL has elementary complexity ofsatisfiability checking. We show interesting potential applicationsof our models in databases and verification.

CCS CONCEPTS• Theory of computation → Transducers; Automata over infinite objects; Logic and verification; Modal and temporal logics; Regular languages; Complexity theory and logic.

KEYWORDS
Data words, logic and automata, Presburger arithmetic, counting,complexity
ACM Reference Format:
Diego Figueira and Anthony W. Lin. 2022. Reasoning on Data Words overNumeric Domains. In 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (LICS ’22), August 2–5, 2022, Haifa, Israel. ACM, New
York, NY, USA, 13 pages. https://doi.org/10.1145/3531130.3533354

1

INTRODUCTION

A data word is a word, each of whose positions contains a labeldrawn from a finite alphabet (just like a normal word in formal
language theory), and a data value from some infinite domain. An
example of data word over the alphabet A = {a,b} and data domain D = Z is (a, 7)(b, 10)(a, 3)(a, 100). The study of automata andlogics over data words has spanned across nearly three decades,
Permission to make digital or hard copies of part or all of this work for personal orclassroom use is granted without fee provided that copies are not made or distributedfor profit or commercial advantage and that copies bear this notice and the full citationon the first page. Copyrights for third-party components of this work must be honored.
For all other uses, contact the owner/author(s).
LICS ’22, August 2–5, 2022, Haifa, Israel© 2022 Copyright held by the owner/author(s).
ACM ISBN 978-1-4503-9351-5/22/08.
https://doi.org/10.1145/3531130.3533354

starting from the study of register automata [22] with a decidable emptiness problem. In addition to this basic register automata
model, there is nowadays a plethora of variants of register automata and other different (and mostly incomparable) models of automata and logics over data words with a decidable emptiness problem including automata with pebbles [31], deterministic memory
automata over ordered data [4], data automata and two-variable
first-order logic [6, 39], alternating 1-register automata and LTL
with freeze quantifiers [15], single-use register automata [8], nominal automata [7], streaming data-string acceptors [2] and its variant over rationals [10], and symbolic finite automata [14] and theirextension with registers [13].
Most of the automata models and logics over data words witha decidable emptiness problem impose a severe restriction on theoperations that can be performed on the data values, i.e., mostly
only comparing data equalities is permitted. In practice, however,
we are interested in a specific domain theory like the set of integers
and permit operations like those that are allowed in the theory of
integer linear arithmetic. For example, consider the (SMT) theories
of arrays (e.g. see [9, 26]). Structurally, arrays can be construed asdata words without a finite alphabet (or equivalently with a unaryfinite alphabet) and integers as the data domain. However, theories of arrays permit the full integer linear arithmetic to express
relationship among the data stored in the arrays, for which there
is only a very limited support by any automata model and logic
over data words. As we shall soon see, certain types of arithmetic
reasoning are also not supported by array theories.
The main goal of this paper is to initiate an investigation of how
integer arithmetic reasoning can be incorporated into automata
models and logics over data words. In doing so, our hope is tobring automata/logic over data words closer to applications, e.g.,in databases and verification.
What type of arithmetic reasoning? In the literature of logic andautomata, many types of integer arithmetic reasoning have been
considered, which include the following:(i) Integer arithmetic constraints on the data values in the
input word, e.g., two positions i < j in the word w =w 1 · · · wn satisfy data(wi ) > data(w j ), data(wi ) ≥ 100 anddata(w j ) = 0 mod 2.
(ii) Letter counting and length, e.g., accept only words whose
numbers of as and bs coincide.
(iii) Data counting, e.g., every data value occurs at most oncein the input word.
(iv) Aggregation, e.g., the k-th largest (or most frequent) data
value is even.
Existing models supporting arithmetic reasoning usually permit
one but not other types of arithmetic reasoning. In practice, weLICS ’22, August 2–5, 2022, Haifa, Israel

are often interested in combining two such types of reasoning, as
explicated in Example 1.1 and Example 1.2.
Example 1.1. We have a daily log file containing a sequence of
events of the form (a, i), where i is the user ID and a ∈ {−1, +1}
denoting that a dollar has been either spent (−1) or earned (+1).
Suppose that we want to ensure that each person earns at least as
much as he spends. Such a property combines (ii) and (iii), and isto the best of our knowledge not expressible in any existing modelwith decidable satisfiability/emptiness on data words.
Example 1.2. We have a log file contining a sequence of pairs of
the form (id, heiдht ) ∈ N2 , where id is an id of a person in a groupand height the integer round-off of the height of the person. For
example, we want to check that each id appears exactly once andthat the median of the heights in the sequence is between 170-180.
This property makes use of (i), (ii), and (iv) and, to the best of ourknowledge, is not expressible in existing decidable models.
State-of-the-art. As we mentioned, most existing models for reasoning over data words do not support arithmetic reasoning overnumeric data domains. For example, guards over linear arithmetic(i.e. (i) above) are not allowed in models like two-variable logics
FO2 (<, +1, ∼) and data automata [5, 6]; this is FO2 over data words
with the order (<), successor (+1) and equal data-value (∼) binary
relations. Here, one can talk about two positions i < j in the input word having the same data value data(i) = data(j), but for
example not data(i) < data(j). This limitation is partially lifted by
Schwentick and Zeume [39], in that two data values can now be
checked for inequality in their logic (e.g. data(i) < data(j)), at theexpense of disallowing the successor relation +1 over positions in
the input word (e.g. one cannot say now that j = i + 1, which canbe done in [6]). The strengths of these formalisms lie in data counting, e.g., every datum occurs at most once in the word, or an evennumber of times; the latter can be done in data automata, but not
in FO2 .
Relaxing the ability (iii) to perform data counting, more models can come into consideration. Array Property Fragment (APF)[9, 26] supports a full integer linear arithmetic reasoning on thearray indices as well as the elements (i.e. (i)). In an APF formula,
universal quantifiers are restricted, so as to allow decidability ofsatisfiability. APF can express, for instance, that an array is ordered.
Array Folds Logic (AFL) [12] addresses the limitations of APF in
performing length reasoning and aggregation (i.e. (iv)) at the expense of disallowing universal quantification. Unlike APF, however, AFL cannot express properties like an array is ordered. We
also mention the model of nondeterministic looping word automata
with arithmetic [18], which input ω-words and consider the theoryof rational linear arithmetic. If one considers instead finite words
and the theory of integer linear arithmetic, this model is strictly
subsumed by AFL. Another noteworthy model is that of Symbolic
Register Automata (SRA), which are an extension of symbolic automata [14] by registers that can be checked for equality. Such amodel is a one-way automata model allowing Presburger guards
on the currently seen data value, and can for example express thatall seen data are even, and that two data in every two consecutive positions are different (which is not expressible in AFL). We finally mention the register automata model of [10] over rational linear arithmetic (inspired by the streaming transducer model in [3]),Figueira and Lin

extending the original model [22] of Kaminski and Francez. Here,the registers are separated into control registers (on which guards
comprising order comparisons can be applied) and data registers(allowing general arithmetic operations). The model supports rational arithmetic operations (i) and aggregation (iv), but not data
counting (iii).
In summary, existing logic and automata models on data words
still have limited support of arithmetic reasoning. In particular,models that support data counting (e.g. two-variable data logic
and data automata [5, 6, 39]) typically do not permit arithmetics
on numeric data domain, letter counting and length reasoning,
and aggregation. Our goal is to identify a model that supports
these four features, while admitting decidable emptiness with elementary complexity (unlike the case of FO2 (<, +1, ∼) and data
automata) and interesting potential applications in databases andverification.
Contributions. We propose in this paper Parametric Semilinear
Data Logic (pSDL), which is an extension of Linear Temporal
Logic (LTL) for reasoning about data words with numeric data
(i.e. the data domain is the set of integers). Aiming to address
the four types of arithmetic reasoning (i)–(iv), we extend the standard LTL with four features: (a) Presburger formulas, which serve
two purposes, namely to check the data value located at a certain position, as well as to perform letter/data counting and length
reasoning, (b) parameters (a form of read-only variables), which
can be used in the Presburger formulas, (c) additional modalities of the form h=iβ (resp. h,iβ ) with h=iβ (y1, ...,yn ) (φ 1 , . . . , φn )(resp. h,iβ (y1, ...,yn ) (φ 1 , . . . , φn )) carrying the meaning that one
can jump to precisely yi different positions (other than the current position) of the same data value satisfying φi (resp. different
data value to the current position), where the integer linear arithmetic constraint β (y1, . . . , yn ) holds. The resulting logic strictly
extends LTL and the modal logic fragment of FO2 (<, +1, ∼) (essentially, an extension of unary temporal logic [17] with the h=i andh,i modalities). More concretely, pSDL can express the property in
Example 1.1. Moreover, in the process of proving decidability for
pSDL satisfiability, we introduce the automata counterpart called
Parametric Semilinear Data Automata (pSDA), whose expressivity
strictly subsumes pSDL, as well as Parikh automata [23], symbolic
automata [14], and nondeterministic looping word automata withinteger linear arithmetic [18].
The following is the main result of the paper:
Theorem 1.3. Satisfiability for pSDL is in 2-NEXP and is NEXPhard. Satisfiability for the fragment SDLMNF of pSDL without parameters and linear arithmetic constraints on data values in minterm
normal form is NEXP-complete.
Note that k-NEXP means “k-fold nondeterministic exponential
time”. The decidability and the complexity results go through atranslation to pSDA, whose decidability and complexity of emptiness we also determine in this paper. Here, SDL denotes the fragment of pSDL without parameters. The restriction to minterm normal form (MNF) is one that is often applied in the literature of symbolic automata [14] — which enforces constraints on data values
to be the same if they intersect — and does not decrease the expressivity of the model. For example, the constraints p(x ) := x > 7 andReasoning on Data Words over Numeric Domains

q(x ) := x ≡ 3 (mod 4) have common solutions, but they can beturned into four constraints in MNF of the form (¬)p(x ) ∧ (¬)q(x ).
Our theorem also implies that the aforementioned modal logic fragment of FO2 (<, +1, ∼) is decidable in elementary time (more precisely, in NEXP), unlike the case of FO2 (<, +1, ∼). This is the modal
logic on data words having the successor, predecessor, future, andpast binary relations as modalities, as well as the “equal data value”
and the “distinct data value” relations. As an aside, our proofs establish interesting connections to Presburger Arithmetic with star
operations [21, 34] and unary counting quantifiers [38].
Our logic pSDL has NP-complete membership (since satisfiability of quantifier-free Presburger formulas can be reduced to it),though it becomes solvable in polynomial-time when we restrict
to SDL. We believe that these complexity classes could still allow
efficient query evaluation (e.g. on our log file examples) with thehelp of SMT-solvers.
Last but not least, our results can be lifted to the data
domain Zk and Nk using a standard “flattening trick”, e.g.,(a, 7, 8)(b, 7, 9)(a, 3, 100) over the alphabet A = {a,b} can bemapped to (a 1 , 7)(a 2 , 8), (b 1 , 7)(b 2 , 9)(a 1 , 3)(a 2 , 100) over the alphabet A′ = {a 1, a 2 , b 1 , b 2 }. This allows us to encode the property in Example 1.2. More generally, this allows us to reason about
a sequence of events with applications (e.g. querying/static analysis over a time series data), and verifying invariants of arraymanipulating programs.
Organization. We provide a more detailed exposition of SDL
through examples and potential applications in Section 2. We fix
notation and basic terminologies in Section 3. For readability, we
start with the simpler fragment, i.e., SDL with 1-ary modalities, i.e.,h=iβ (ȳ ) and h,iβ (ȳ) with |ȳ| = 1. We define this logic in Section
4, provide the automata counterpart (called SDA), for which decidability and complexity of nonemptiness are proven in Section
5. Translation from SDL to SDA is in Section 6. We then provide
the extensions to the general case — with parameters, and k-ary
modalities — in Section 7. We conclude in Section 8.

2

PSDL: EXAMPLES AND APPLICATIONS

We provide here an overview of our logic pSDL by means of examples, and discuss potential applications thereof. In the sequel, we
work with the data domain N of natural numbers, but our results
easily extend to the data domain Z of all integers.
Querying log files. We now discuss Example 1.1 and Example 1.2.
We first show how to express the property in Example 1.1. This
example can already be done in SDL with 2-ary modalities. In particular, the formula expressing it isG(−1 → h=iy2 >y1 (−1, +1)).
Intuitively, the formula says that it is globally the case that if auser (say with a user ID id) spends $1 (i.e. -1) at a particular time
point on the day, then the user earns $ y2 on that day, which is atleast the total spending (i.e. $ y1 + 1). In particular, y2 here counts
the number of occurrences of positions labeled by (+1, id ), while
y1 counts the number of positions (other than the current position,
which is labeled by (−1, id )) labeled by (−1, id ). The above formula
is in fact in SDLMNF because no parameters are used and that noarithmetic constraints on the current data values are applied.

LICS ’22, August 2–5, 2022, Haifa, Israel

We now proceed to the property in Example 1.2, which is a
simple reasoning over a relational table. For simplicity, we willassume that only one person has the median height; this is easily extendable to the case when there are more persons with themedian height, but will make the formula messier. Using the flattening trick, we consider the finite alphabet A = {1, 2} indicating the first/second arguments in the tuple (id, heiдht ). Thus, weensure that the input word is of the form ((1, ?), (2, ?)) ∗ , where ?
can indicate any number. This can be enforced easily in LTL, e.g.,G((1 → X2)∧(2∧X⊤ → X1)). Next, we enforce that each ID occurs
uniquely in the sequence. This can be enforced by the formula
G(1 → ¬ h=iy ≥1 1)
which says that globally one cannot jump to another tuple whose
first argument has the same ID as the current one. Indeed, whenparameterized with y ≥ 1, the construct h=iy ≥1 ψ can be regarded
as the modality “jump to a position with the same data value satisfying ψ ”. Finally, we use the parameter pmed to determine themedianF(2 ∧ 170 ≤ x = pmed ≤ 180 ∧ h,iy1 =y2 (x < pmed , x > pmed )).
The formula first finds the second argument of a tuple in the table.
Here, x denotes the current data value that is “saved” into pmed .
[In the sequel, x is mostly used to denote the current data value.]
This is required since our modality “forgets” the current data value,
which has to then be alleviated by the use of parameters. The final
conjunct simply says that there are the same number y1 = y2 ofpeople who are shorter than the person with the median height
and those who are taller than the person with the median height.
Observe that linear arithmetic constraints are used for two purposes in the above formula: as counting constraints (e.g. y1 = y2 ),as well as for limiting the values that certain locations in the input
word can take (e.g. x < pmed ).
We show that the first query above can be checked inpolynomial-time. The second query, on the other hand, can be written in pSDL, whose membership problem is NP-complete (cf. Theorem 7.3). We leave it for future work to determine whether SMTsolvers could be used to effectively perform such a query evaluation for pSDL. On the side of static analysis, Theorem 1.3 implies
that vacuity of our queries can be automatically checked.
Array-manipulating programs. We now show a simple application of pSDL for verifying that the bubble sort preserves the invariant Inv that “every value occurs precisely once”. We will model the
bubble sort algorithm as a repeated nondeterministic applicationof swapping the element xi at position i and the element x j at position j such that i < j and xi > x j . To treat this more formally, weneed to model a transduction T for this swap relation.
We model T as the data language over the boosted alphabet
A = {a,b, c} containing all words w obtained by replacing theith position (a, d i ) (resp. jth position (a, d j )) in the data word(a, d 1 ) · · · (a, d n ) by (b, d i )(c, d j ) (resp. (b, d j )(c, d i )), for some i < jand d i > d j . Observe that the subsequence w 1 of w whose first components are a or b represents the initial array content, while thesubsequence w 2 of w whose first components are a or c represents
the result of applying T .

LICS ’22, August 2–5, 2022, Haifa, Israel

Figueira and Lin

Example 2.1. Suppose T is to swap the 2nd and 4th elementsin the array [4, 7, 1, 2, 0]. We represent this array the word w =(a, 4)(b, 7)(c, 2)(a, 1)(b, 2)(c, 7)(a, 0).
Thus, w 1 = (a, 4)(b, 7)(a, 1)(b, 2)(a, 0) gives the original array,
while w 2 = (a, 4)(c, 2)(a, 1)(c, 7)(a, 0) represents the array obtained after applying the swap.


the input word, we are guaranteed to have every data value between [pmin , pmax ] in the input word. Note, however, that thistrick does not apply when we allow each data value to occur morethan once.

Note that we can express T quite easily in pSDL. First we express
that the projection to the first components is in a ∗bca ∗bca ∗ , whichis easily expressible in LTL (and so in pSDL). The following formula
φ expresses that the swap takes place:

Basic notation. Let N = {0, 1, 2, . . . }. We write k to denote theset {1, . . . , k }. The set of finite words over a domain A is denotedby A∗ . We will often work with finite words over the cartesian
product of pairwise disjoint alphabets, e.g., w ∈ (A × B × C ) ∗ . We
use letters A, B to denote finite alphabets. For w ∈ (A × N) ∗ , wewrite data(w ) and lab(w ) to denote the projection of w onto N and
A respectively. Given a word w ∈ A∗ and a set I ⊆ {1, . . . , |w |},we write w[I ] to denote the subword of w given by the indices in
I (e.g., w[{1, . . . , |w |}] = w, w[∅] = ε). We write w[i] as short forw[{i}]. We write |w | to denote the length of w.

F(b ∧ p = x ∧ X((p ′ = x ∧ p > p ′ ) ∧ F(b ∧ p ′ = x ∧ X(p = x )))).
Note that x is used to record the current data value, while the parameter p (resp. p ′) is used to save d i (resp. d j ).
To disprove that Inv is an invariant, we need to show that, there
exists an input data word w such that w 1 satisfies Inv but w 2 satisfies ¬Inv. The following SDL formula ψ expresses this:G((a ∨ b) ∧ ¬ h=iy ≥1 (a ∨ b)) ∧ ¬G((a ∨ c) ∧ ¬ h=iy ≥1 (a ∨ c)).
The final formula is φ ∧ ψ , which is unsatisfiable since Inv is aninvariant under T . The decidability of pSDL implies that this satisfiability can be algorithmically checked.
Other properties. We conclude this section by collecting a few
examples that can be expressed in pSDL. As far as we are aware,these cannot be expressed in other formalisms with decidable satisfiability/emptiness problem.
(P1) Each data value occurs at most once in the word and isan even number.
(P2) Property (P1) and the subset of the positions containing
data values divisible by 4 has the same number of a’s andb’s.
(P3) Each data value occurs an even number of times, and amost frequent data is even.
(P4) Each data value occurs at most once, and the set of data
values forms an interval.
(P5) Each data occurs at most once, and the k-th biggest value
is the length of the word.
(P6) Each data value occurs the same number of times.
For example, (P3) can be expressed in pSDL as the conjunction of
G(h=i1≤y <p∧y≡1 (mod 2) ⊤).
andF(x ≡ 0(mod 2) ∧ h=ip−1=y ≥0 ⊤)(Recall that h=i is ‘strict’, in the sense that it only counts occurrences different from the current position’s.) Note that the parameter p is used as a placeholder for the most frequent data value
in the input word. As another example, assuming that each data
value occurs in the input at most once (which we saw is expressible in pSDL), (P4) can be expressed as a conjunction of F(x =pmax ) ∧ F(x = pmin ) andG(pmin ≤ x ≤ pmax ) ∧ h,iy=pmax −pmi n ⊤.
Here, we save the maximum and minimum data values into parameters, and say that there are precisely pmax − pmin + 1 data
values in the input word. Because of uniqueness of data values in

3 PRELIMINARIES

Parikh images, semilinear sets, Presburger arithmetic. The
Parikh image of a word w ∈ A∗ over a finite alphabet A, is afunction Π(w ) : A → N assigning to each a ∈ A the number of
appearances of a in w. The Parikh image of a language L ⊆ A∗ isΠ(L) = {Π(w ) : w ∈ L} ⊆ NA .
A linear set is a subset of Nk that can be described as an arithmetic progression {v̄ 0 +α 1v̄ 1 +· · ·+αn v̄n | α 1 , . . . , αn ∈ N} for somen ∈ N and v̄ 0 , . . . , v̄n ∈ Nk . A semilinear set is a finite union of
linear sets. Linear sets are represented by the offset v̄ 0 and thegenerators v̄ 1 , . . . , v̄n , where numbers are represented in binary.
Presburger arithmetic refers to first-order logic in the languageof addition (+), inequality (≤), and modulo k (mod k) operatorsfor every k > 1, evaluated over the natural numbers (this is sometimes called extended Presburger arithmetic). For example, ∃x (x ≥y +y) ∧ ((y +x ) mod 19 = y) is a Presburger formula with one freevariable. Each Presburger formula φ(x 1 , . . . , xk ) with k free varidef

ables denotes a set [[φ]] = {(n 1 , . . . , n k ) ∈ Nk : (n 1 , . . . , n k ) |= φ}.
It is well-known that semilinear sets correspond precisely to Presburger arithmetic [19] and to Parikh images of context free (orregular) languages by Parikh’s Theorem [32]. A quantifier-free
Presburger formula is any Presburger formula with no quantifiers. Presburger formulas admit quantifier elimination [20, 35]: forevery Presburger formula there exists an equivalent quantifier-freeformula. An existential formula is a Presburger formula of the form
∃x 1 , . . . , xn φ, where φ is quantifier-free.
We extend now Presburger Arithmetic with the star operator ∗ .
For any formula φ(x 1 , . . . , xn ) and m ≥ 0, we permit formulas φ ≤mand φ ∗ with semantics [[φ ≤m ]] := {t¯1 + · · · + t¯m′ : m ′ ≤ m and t¯i |=S
φ for every i} ⊆ Nn (or ∅ if m = 0), and [[φ ∗ ]] := m ≥0 [[φ ≤m ]]. We∗≤mdefine, in an analogous way, sets S and S
for any set S ⊆ Nn .
It is known that, for every existential Presburger formula φ, φ ∗ isalso expressible by an existential Presburger arithmetic formulaof at most exponential size [34], and hence that S ∗ is semilinear
assuming S is too. Observe that φ ≤m can be expressed as follows:φ ≤m(x̄ ) = ∃y ψ ∗ (x̄y) ∧y ≤ m, where ψ (x̄y) = φ(x̄ ) ∧ y = 1. (⋆)
Note that variable y is used to ‘count’ the number of applicationsof ψ ∗ . Observe that in the translation above, the resulting formula
is of size logarithmic in m. Piskac and Kuncak [34] have shownthat existential Presburger formulas with star is NP-complete, soReasoning on Data Words over Numeric Domains

long as they are of star-height 1 (i.e. no nesting of the star operator
is allowed). As recently shown in [21], this NP upper bound can begeneralized to any fixed star-height.
Complexity classes We use standard notations for complexity
classes [25], including NP, PSPACE, k-NEXP, #P, PP, P#P , and NPNP .
For example, 2-NEXP is the class of problems solvable by a nondeterministic Turing machine in double exponential time. The class#P is the class of counting problems, whose solutions correspond to
the number of accepting paths of a nondeterministic polynomialtime Turing machine. Some of these classes have also oracle access. For example, P#P = PPP (e.g. see [41]) corresponds to theclass of problems solvable in polynomial time with access to a #P
oracle. By Toda’s theorem ([40], see also [25]), P#P contains theentire polynomial hierarchy (PH). The class NPNP corresponds tothe second-level of PH. Finally, we use the class PNP[log] [44] of
problems solvable in polynomial-time with logarithmically manycalls to an NP oracle. It is known that PNP[log] contains the entireboolean hierarchy, which in turn contains NP, co-NP, DP, etc.

4

SEMILINEAR DATA LOGIC

We now formally define Semilinear Data Logic (SDL). For readability, we disallow parameters and restrict to 1-ary modalities.
This will be generalized in Section 7. SDL has an LTL-navigationalflavor, featuring common modalities such as Next, Future, Until,
Since, etc. On top of that, it has two kinds of extra modalities. One
modality h=iβ ψ which allows to state that β satisfies n, for n thenumber of positions j different from the current one with the samedata value and a certain property ψ . And another modality h,iβ ψwhich works similarly but for positions with different data values.
We use quantifier-free Presburger formulas for testing for suchproperties β. Further, we allow Presburger guards on data values.
The logic can express the following properties:• “for every a-position there is a b-position with the samevalue”,• “there are no two a-positions with the same value”, or• “there are no two consecutive positions with the samevalue”.
The first two properties above can be expressed with previously
studied logics such as FO2 (<, ∼), and the last one with FO2 (+1, <, ∼) logics of [6], using register automata [22] or freeze-LTL [16].
Further, using the linear arithmetic power, we can ‘count’ the number of positions with the same data value as the current one. One
can then express properties like “for every a-position with an evendata value there is an odd number of b-positions with the samevalue”.
Definition. The syntax of Semilinear Data Logic (SDL) overwords w ∈ (A × N) ∗ is given by the following grammar:
φ F a | α | φ ∧ φ | ¬φ | φ U φ | φ S φ | h=iβ φ | h,iβ φ,where a ∈ A, and α, β are quantifier-free Presburger formulas with
one free variable x. We call a and α base formulas of the logic
since they correspond to leaves in the grammar derivations. As
usual, we write ⊥ as short for a ∧ ¬a for some a ∈ A; ⊤ for ¬⊥;and φ ∨ ψ for ¬(¬φ ∧ ¬ψ ).

LICS ’22, August 2–5, 2022, Haifa, Israel

For base formulas, we define the satisfaction relation on a wordw ∈ (A × N) ∗ as w, i |= α if z |= α, where z = data(w[i]); andw, i |= a if a = lab(w[i]). The U, S modalities have the expected
LTL semantics, where we define them as ‘strict’ modalities: w, i |=φ Uψ (resp. w, j |= φ Sψ ) if there is j > i such that w, j |= ψ and forevery i < ℓ < j we have w, ℓ |= φ. As it is customary, we use the
def

def

standard LTL modalities as shorthands: Fφ = ⊤ Uφ, Xφ = ⊥ Uφ,
def

def

def

def

Gφ = ¬F¬φ, F−1φ = ⊤ S φ, X−1φ = ⊥ S φ, G−1φ = ¬F−1 ¬φ.
The remaining modalities are the key constructs for testing for data
values. Given a word w ∈ (A × N) ∗ , for any position 1 ≤ i ≤ |w |,we have w, i |= h=iβ φ (resp. w, i |= h,iβ φ) if the number n ∈ Nof positions j ∈ {1, . . . , |w |} distinct from i such that (i) w, j |= φ,(ii) data(w )[j] = data(w )[i] (resp. (i) w, j |= φ and (ii) data(w )[j] ,data(w )[i]) is such that n |= β. Analogously, w, i |= h,iβ φ if thenumber n ∈ N of positions j ∈ {1, . . . , |w |} distinct from i such that(i) w, j |= φ and (ii) data(w )[j] , data(w )[i] is such that n |= β.
Observe that we have opted for a ‘strict’ version of the h=imodality, in which we count positions different from the current
one, to be in line with the semantics of U and S. However, a nondef
strict version hh=ii of the modality is definable by hh=iiβ (y ) (ψ ) =(¬ψ ∧ h=iβ (y ) (ψ )) ∨ (ψ ∧ h=iβ (y+1) (ψ )).
Remark. Notice that data modalities are closed under taking dual,
in the sense: ¬ h=iβ ψ ≡ h=i¬β ψ . Observe also that, for β (x ) := x ≥1, the formula h=iβ ψ evaluated at position i of w tests whether there
exists some other position j with the same data value satisfyingψ . In asimilar way, we can test that there are at least ℓ (using β (x ) := x ≥ ℓ)or that there are an even number of such positions j (with β (x ) := (xmod 2 = 0)). Indeed, SDL allows for counting properties for eachdata equivalence class. This particular restriction in fact subsumes
the modal logic fragment of FO2 (<, +1, ∼). As we shall see later, ourlogic has the advantage of admitting elementary complexity, in contrast to that FO2 (<, +1, ∼) being not primitive-recursive. This is because FO2 (<, +1, ∼) satisfiability can capture reachability of Petrinets, which is decidable [24, 27, 29, 30] but not primitive-recursive[11, 28].
Model checking. The model checking problem for this logic, thatis, the problem of given a formula φ and a word w ∈ (A × N) ∗whether w, 1 |= φ is in polynomial time.
Proposition 4.1. The model checking problem for SDL is in polynomial time.
Proof. Given w ∈ (A × N) ∗ and φ ∈ SDL, we use the following
standard algorithm to mark each position 1 ≤ i ≤ |w | with the setof subformulas ψ of φ such that w, i |= ψ . We proceed by induction:
we first treat base formulas, and then formulas containing alreadytreated subformulas.
For each base subformula ψ of φ, we can mark each positioni such that w, i |= ψ in linear time (remember that formulas arequantifier-free). For each subformula ψ U ψ ′ or ψ S ψ ′ we can also
mark which positions satisfy the formula in linear time, assuming
ψ ,ψ ′ have been already treated. Similarly for ¬ψ and ψ ∧ ψ ′. For
a subformula of the form h=iβ ψ we proceed as follows: For eachdata value d of w, we first count the number n of positions of w
having data d and satisfying ψ , and we then mark each position iwith data d as satisfying h=iβ ψ iff

LICS ’22, August 2–5, 2022, Haifa, Israel

Figueira and Lin• the position is marked as satisfying ψ and n − 1 |= β, or• the position is marked as not satisfying ψ and n |= β.
Observe that this takes quadratic time. Finally, for a subformulaof the form h,iβ ψ we proceed similarly: For each data value d ofw, we count the number n of positions having data different fromd and satisfying ψ , and we mark each position i with data d as
satisfying h,iβ ψ iff n |= β.
Once all the markings are done, we answer ‘yes’ if the first position is marked with the input formula φ, and ‘no’ otherwise. 
Satisfiability. Here we focus on the satisfiability problem, thatis, the problem of, given a formula φ whether there is some w ∈(A × N) ∗ such that w, 1 |= φ.
We say that the formula ψ of SDL is in minterm normal form
(MNF) if for every pair of distinct Presburger base subformulasα, α ′ thereof, we have that α (x ) ∧ α ′ (x ) is unsatisfiable.1 In particular, (x ≥ 2) ∧ F(x ≤ 5) is not in MNF, but h=ix ≥2 ⊤ ∧ F h=ix ≤5 ⊤is. Let SDLMNF be the set of formulas in MNF. We will show thefollowing in the next couple of sections.
Theorem 4.2.
(1) The satisfiability problem for SDL is in 2NEXP.
(2) The satisfiability problem for SDLMNF is NEXP-complete.
The gap between 2NEXP and NEXP is due to the cost of bringing the logic to minterm normal form. Closing the gap seems to
be a difficult problem, which underlies also the difficulties that aredealt with in practice by symbolic automata algorithms [14]. We
leave this as an open problem. The NEXP-hardness proof can befound in the full version of this paper, it follows by a reduction
from the exponential tiling problem [42]. We will show the upperbound of items 1 and 2 by reduction to an automata model ‘SDA’,or Semilinear Data Automata, that we introduce in the next section. In fact, SDA is considerably more expressive than SDL. The
remaining sections will be dedicated first to defining and showing
decidability for SDA, and then to prove the upper bound for the satisfiability of SDL, via an effective language-preserving translation
to SDA.

5

SEMILINEAR DATA AUTOMATA

We present an automata model which we call Semilinear Data Automata (SDA) and prove some basic properties (e.g. closures, decidability) about them. We will show in Section 6 that it captures
SDL.

5.1

Definition

For a finite alphabet A, we define a language acceptor of words
over A × N. A Semilinear Data Automaton (SDA) over A is apair (T , S ) where, for a finite alphabet B, we have:(1) S is a semilinear set over NB × NB ;(2) T ⊆ (A × N) ∗ × B∗ is a length-preserving transducer, defined
via a regular language LT ⊆ (A × Ψ × B) ∗ for a finite set Ψof quantifier-free Presburger formulas φ(x ) with one free variable x, and some finite alphabet B. T denotes the set of allpairs (w, w ′ ) ∈ (A × N) ∗ × B∗ such that there exist a sequenceψ 1, . . . ,ψ ℓ of Ψ-formulas where:
1 Note that we do not include formulas β of the h=i

β and h,i β modalities.

(i) |w | = |w ′ | = ℓ,(ii) data(w )[i] |= ψ i for all i ∈ ℓ, and(iii) (lab(w )[1],ψ 1 , w ′ [1]) · · · (lab(w )[ℓ],ψ ℓ , w ′ [ℓ]) is in LT .
We call B the output alphabet of T and Ψ its Presburger
alphabet.
A word w ∈ (A × N) ∗ is accepted by such an SDA if there exists
some w ′ ∈ B∗ such that(i) (w, w ′ ) ∈ T , and(ii) for every n ∈ N, (Π(w ′ [In ]), Π(w ′ [I¯n ])) ∈ S,
where In = {1 ≤ j ≤ |w | : data(w )[j] = n} and I¯n = {1, . . . , |w |} \In .
Henceforth, we assume that semilinear sets S ⊆ NB × NB as
above are represented as quantifier-free Presburger formulas, using variables xb= for each b ∈ B for the first B-components, andvariables xb, for each b ∈ B for the last B-components. Similarly, regular languages are represented as non-deterministic finite automata (NFA). We say that an SDA is in minterm normal form (MNF) if, for every pair of transitions (p, (a, φ, b), q),(p ′, (a ′, φ ′, b ′ ), q ′ ) of the NFA representing its transducer T , eitherφ ∧ φ ′ is unsatisfiable or φ = φ ′ .
The definition of SDA is inspired by the Data Automata (DA)model introduced in [6]. However, it is incomparable in expressive
power. On the one hand DA work with an abstract infinite domain
equipped with an equivalence relation, and the transducer part of
DA is just a letter-to-letter transducer T ⊆ A∗ × B∗ . It cannot express, e.g., the SDA property “each datum associated with the lettera is even”. On the other hand, DA can test for regular properties
of equivalence classes (e.g., “every class is a word in (ab) ∗ ”) whichcannot be expressed by SDA, whereas SDA can test for semilinear
constraints on the Parikh-image of equivalence classes (e.g., “for every class there are as many a’s as b’s”) which cannot be expressedby DA. Unfortunately, a generalization of both DA and SDA is infeasible: in the full version of this paper, we show that generalizing
both mechanisms (i.e., DA extended with semilinear constraints)
would result in a model with undecidable emptiness problem.
Proposition 5.1.
(1) SDA are effectively closed under union and intersection.
(2) SDA are not closed under complement.
(3) The universality, equivalence and containment problems for SDA
are undecidable.
Proof of item (1). Assume (T1 , S 1 ) and (T2 , S 2 ) are SDA. We
assume without any loss of generality that the output alphabet
B1 of T1 and B2 of T2 are disjoint. Let B1 = {a 1, . . . , a ℓ1 } andB2 = {b 1, . . . , b ℓ2 }.
(∪) Assuming S 1 and S 2 are given by Presburger formulas
φ S 1 (x a1 , . . . , x a ℓ1 , ya1 , . . . , ya ℓ1 ) andφ S 2 (xb 1 , . . . , xb ℓ , yb 1 , . . . , yb ℓ ),22

we simply define S = [[φ S ]], where φ S = φ S 1 ∨ φ S 2 . Finally, let
T = T1 ∪ T2 —whence having an output alphabet B1 ∪˙ B2 . It thenfollows that the language of (T , S ) is the union of the languages of
the two input SDA.
(∩) For intersection, we essentially build the product of both automata, which here implies considering the cartesian product ofReasoning on Data Words over Numeric Domains

LICS ’22, August 2–5, 2022, Haifa, Israel

the alphabets (in the same way as intersection of DFA implies considering the cartesian product of the states).
This time we define S as a set over NB1 ×B2 × NB1 ×B2 . Assuming S 1 , S 2 are given by formulas φ S 1 , φ S 2 as before, we define S as
φ S ({x ai ,b j , yai ,b j }i ∈ℓ1, j ∈ℓ2 ) = φ 1 ∧ φ 2 , whereyyφ α = φ S α (t ax1 , . . . , t axℓα , t a1 , . . . , t a ℓα ),PPyfor α ∈ {1, 2}, t axi = j ∈ℓ3−α x ai ,b j , t ai = j ∈ℓ3−α yai ,b j for everyi ∈ ℓα . We finally define T = T1 × T2 , that is, given w it outputsu ∈ (B1 × B2 ) ∗ iff (w, u B1 ) ∈ T1 and (w, u B2 ) ∈ T2 . We then havethat (T , S ) denotes the intersection of the languages of the two
SDA.

Proof of items (2) and (3). It is easy to see that SDA is effectively equivalent in expressive power to Parikh automata [23]when disregarding the numeric domain N. Since the latter has anundecidable universality problem, it follows that the universality
problem for SDA is also undecidable. The undecidability for theequivalence and containment problems follow thus as corollaries.
Analogously, the fact that SDA are not closed under complement
can be seen also as a consequence of Parikh automata not being
closed under complement.


5.2

The Emptiness Problem for SDA

Theorem 5.2. The emptiness problem for(1) . . . SDA is decidable in NEXP.
(2) . . . SDA in minterm normal form is in P#P and PNP[log] -hard.
(3) . . . SDA in minterm normal form whose transducers use no modular predicates is NP-complete.
We will first show decidability, and then explain how the bounds
follow from the proof.
Lemma 5.3. The emptiness problem for SDA is decidable.
Proof. Let A = (T , S ) be a SDA. Let Φ be the Presburger alphabet of T . For P ⊆ Φ, we say that x ∈ N has profile P if it satisfiesV
def V
the formula π P (x ) = ψ ∈P ψ (x ) ∧ ψ ∈Φ\P ¬ψ (x ). Let P∞ be theset of profiles P such that |[[π P ]]| = ∞ and let P<∞ be the remaining ones. For P ∈ P<∞ , let n P be the number of x ∈ N with profile
P. Observe thatn P = |[[π P ]]|.

(†)

Consider T seen as a regular language over A × Φ × B. By Parikh’s
Theorem [33], its Parikh image is semilinear, and an existential
Presburger formula φT (x̄ ) representing it can be produced, even in
linear time [43]. Assume that x̄ (i.e., the free variables of φT (x̄ )) has
a variable x a,φ,b for every a ∈ A, b ∈ B and φ ∈ Φ, representing
the number of appearances of (a, φ, b) ∈ A × Φ × B in the word;and let us assume B = {b 1 , . . . , bm }.
We now need to verify whether a given satisfying valuation forx̄ in φT is such that one can produce a word in the language ofA. For this, we will need to first guess how each number denotedby the x a,φ,b variables is distributed across profiles. Then we haveto check, separately for each profile P, that the guessed number of
elements with profile P is in agreement with the bound n P as defined above. Concretely, for a valuation of x̄, consider the propertyµ ∼ stating thatP
(1) there exists a number x a,φ,b∈ N for every possible a ∈ A, b ∈PPB, profile P, and φ ∈ P, such that x a,φ,b = P ∋φ x a,φ,b
, and
P
ˆ
(2) letting ti =
x
(i
∈
m)
and
S
⊆
NB be
φ ∈Φ, a ∈A a,φ,b i{(x 1 , . . . , xm ) : (x 1 , . . . , xm , (t 1 − x 1 ), . . . , (tm − xm )) ∈ S },(i) for every P ∈ P∞ , we have

X
X
*.
+/ ˆ∗
P
P
x a,φ,b,...,∈ S ; andx a,φ,b1
m
a ∈A,φ ∈P,a ∈A,φ ∈P(ii) for every P ∈ P<∞ , we have
X
X*.
+/ ˆ ≤n PPP
x a,φ,b
,
.
.
.
,
∈S
.
x a,φ,b1
m
a ∈A,φ ∈P,a ∈A,φ ∈P
The idea is that (1) checks that the partitioning of each x a,φ,b intoP
profiles x a,φ,b
is consistent, and (2) guarantees that the numbers
are such that: for those profiles for which we can generate as many
data tuples as we want, the sum of vectors belongs to Sˆ∗ , and forprofiles containing only n P -many data tuples, the sum of vectors
belongs to Sˆ ≤n P . Formally, we obtain the following.
Claim 1. There exists x̄ ∈ NA×Φ×B such that x̄ |= φT and x̄ |= µ ∼if, and only if, A has a non-empty language.
(⇐) We first show the right-to-left direction of Claim 1. Assumew ∈ (A × N) ∗ is in the language of A, let w ′ ∈ (A × Φ × B) ∗ be
the witnessing word of the transducer. We show that x̄ = Π(w ′ )satisfies both properties. The fact that x̄ |= φT goes by definition.
P
For the satisfaction of µ ∼ , assume x a,φ,bis the number of positions′′
i of w such that w [i] = (a, φ, b) and data(w )[i] has profile P (i.e.
data(w )[i] |= π P ). It follows that it is a partition of x̄ satisfying
item (1) of µ ∼ . We now proceed to show item (2). Let w B′ be theprojection of w ′ onto its B component. For d ∈ N, let Id = {1 ≤ i ≤|w | : data(w )[i] = d } and I¯d = {1, . . . , |w |} \Id . For every j ∈ m andd ∈ N, let x dj be the number of indices i such that data(w )[i] = dd ) = Π(w ′ [I ]) for
and w B′ [i] = b j ; in other words (x 1d , . . . , xm
B devery d. Observe that for every j,
XXP
x a,φ,b=x dj .
(†)
ja ∈A,φ ∈P

d ∈N s.t. d |=π P

Now, let us fix some d ∈ N appearing in w, and suppose it hasd ) ∈ S.
ˆ By definition of S,ˆ thisprofile P. We show that (x 1d , . . . , xmddddhappens if, and only if, (x 1 , . . . , xm , (t 1 − x 1 ), . . . , (tm − xm )) ∈ S,
where (t 1 , . . . , tm ) = Π(w B′ ). Hence, (t j − x dj ) is the number of
positions 1 ≤ i ≤ |w | such that w B′ [i] = b j and data(w )[i] , d (i.e.,
the number of b j ’s in w B′ [I¯d ]). In other words, ((t 1 − x 1d ), . . . , (tm −d )) = Π(w ′ [I¯ ]). Since w ′ is a witness for non-emptiness of A,xm
B d
it follows that (Π(w B′ [Id ]), Π(w B′ [I¯d ])) ∈ S, and by the remarksd ) ∈ S.
ˆ In view of (†), we must then have thatabove (x 1d , . . . , xm
XX*.
+/ ∈ Sˆ ≤α ,PPx a,φ,b,...,x a,φ,b1
m
a ∈A,φ ∈P,a ∈A,φ ∈P
for some α ∈ N which cannot be greater than the number of elements from N with profile P. This shows that both conditions (2i)and (2ii) must hold true.

LICS ’22, August 2–5, 2022, Haifa, Israel

Figueira and Lin(⇒) For the left-to-right direction of Claim 1, suppose φT ∧ µ ∼has a satisfying assignment x̄ ∈ NA×Φ×B . We show how to build aword w ∈ (A × N) ∗ in the language of A. Since x̄ |= φT there must
be some w ′ = (c 1 ,ψ 1, c 1′ ) · · · (c ℓ ,ψ ℓ , c ℓ′ ) ∈ LT such that Π(w ′ ) = x̄.
Since x̄ |= µ ∼ each index 1 ≤ j ≤ |w ′ | can be assigned a profile Pr j so that the word restricted to any fixed profile P satisfies
PPPˆ ≤α for some α ∈ N such thata ∈A,φ ∈P (x a,φ,b 1 , . . . , x a,φ,bm ) ∈ S
α ≤ n P if |[[π P ]]| < ∞. For any such profile P, we can then takeany α-many pairwise distinct elements d 1P , . . . , d αP ∈ N with profile P, and assign to each index j ∈ {1 ≤ j ≤ ℓ : Pr j = P }some value d iPj so that the Parikh image restricted to each d iP is
ˆ The final word w in the language of A is then any word
in S.
Pr

w = (c 1 , d 1 ) · · · (c ℓ , d ℓ ) ∈ (A × N) ∗ such that d j = d i j j for every 1 ≤ j ≤ ℓ. This concludes the proof of Claim 1.
We finally show that these properties can be expressed in Presburger arithmetic. Since as already discussed φT (x̄ ) is an existential Presburger formula, it only remains to show:
Claim 2. µ ∼ (x̄ ) is expressible by a Presburger formula.
Let χS be a formula having, besides x̄, some extra free variables
x 1 , . . . , xm , defined asdefχS (x 1 , . . . , xm , x̄ ) = (x 1 , . . . , xm , (t 1 − x 1 ), . . . , (tm − xm )) ∈ S,
P
where ti = φ ∈Φ, a ∈A x a,φ,b i for every i ∈ m. For α ∈ {∗} ∪ N,

let φ Shα i be the formula expressing that there exist variables ȳ(one for each x a,φ,b i ) such that χS≤α (x 1 , . . . , xm , ȳ) holds.2 For
the sake of brevity we will henceforth abuse notation writingP∃cond(P, a,φ,b )x a,φ,b
ψ to denote ∃x aP 1,φ ,b · · · ∃x aP z,φ ,b ψ for all
1 1 1
z z z
the triples Pi , ai , φi , bi satisfying the condition cond. Now we dedefPfine µ ∼ (x̄ ) = ∃a ∈A,b ∈B, P ⊆Φ,φ ∈P x a,φ,bA ∧ B ∧ C, where

A=

X
+/ ,
*.x
P
x a,φ,ba,φ,b =P ∋φa ∈A, ,
^

φ ∈Φ,
b ∈B

B=

X
X
*
+
P
P
φ Sh∗i .
x a,φ,b,...,x a,φ,b, x̄ / ,1m
P ∈P∞a ∈A,φ ∈P,a ∈A,φ ∈P
^

X
X
P
P
φ Shn P i*.
x a,φ,b,...,x a,φ,b, x̄ +/ .
1mP ∈P<∞
a
∈A,φ
∈P
a
∈A,φ
∈P
,
It is straightforward to see that µ ∼ is an existential Presburger
formula expressing properties (1) and (2). Hence, decidability follows from decidability of the satisfiability problem for Presburger
formulas.

C=^

Corollary 5.4. For every SDA recognizable language L ⊆ (A ×N) ∗ , we have Π({lab(w ) : w ∈ L}) ⊆ NA is semilinear.
As a corollary of the previous proof we obtain the bounds ofTheorem 5.2.
2 Recall the definition of ·∗ and · ≤m of (⋆).

Proof of Theorem 5.2. First observe that, in the proof of
Lemma 5.3, µ ∼ uses Sˆ∗ in its definition. As already mentioned thisstar operator preserves semilinearity [34], but the equivalent existential Presburger formulas without star may be of exponential
size. However, in [21] it is shown that the satisfiability problem forexistential Presburger formulas with star operators which happen
to be of star-height 1 (as is our case) is decidable in NP. Observe
that, in light of the translation (⋆), Sˆ ≤n P can be written as an existential formula of star-height 1 of size logarithmic in n P and polyˆ On the other hand, counting
nomial in the formula expressing S.
the number of satisfying assignments of an existential Presburger
formula φ is in the counting hierarchy [1], in particular in #PNP .
This is because if [[φ]] is finite, then any satisfying assignment for
φ use numbers which are at most exponential [36]; hence an NP
Turing machine can guess an assignment x̄ ∈ Nk and accept iffx̄ |= φ, which necessitates a call to an NP procedure for existential
Presburger satisfiability. The number of accepting runs will thencorrespond to the number of satisfying assignments.
Proposition 5.5 ([36, 45]). For any quantifier-free formula φ wehave the following bounds. |[[φ]]| and k[[φ]]k∞ are bounded by some
singly exponential function [36].3 Further, if φ does not use modular
predicates, |[[φ]]| can be computed in polynomial time [45].4
In view of Proposition 5.5, observe that we can compute, in #P,|[[π P ]]| for every profile P. Further, if no formula of the transducer
uses modular predicates, |[[π P ]]| can be computed in polynomial
time.
Bearing all this in mind, we now proceed to extract the statedupper bounds.
(1) Let (T , S ) be a SDA. We compute, in exponential time, all then P ’s and we produce a singly exponential sized existential formula
φT ∧ µ ∼ of star-height 1, whose satisfiability can be checked in
NEXP (in the size of the automaton).
(2) Let (T , S ) be a SDA in MNF. Observe that in this case thenonempty profiles are just singleton sets, and hence that π P canbe equivalently expressed as π {φ } (x ) = φ(x ). In this case, we cancompute in P#P the n P ’s according to (†). Thus, the produced formula φT ∧ µ ∼ can be written as a polynomial sized existential formula of star-height 1, which can be tested in NP. This gives an P#P
upper bound. The lower bound can be found in the full version of
the paper.
(3) As already observed, in this case n {φ } can be computed inpolynomial time, which was the bottleneck of the previous case.
Thus, we end up with an NP procedure.
NP-hardness follows by an easy reduction form SAT. Given a
Boolean formula φ in n variables x 1 , . . . , xn we produce the semilinear set S ⊆ NB × NB for B = {b 1, . . . , bn }, as a quantifier-freeformula with free variables {yi= }i ∈n , {yi, }i ∈n as the result of replacing each xi with yi= +yi, > 0 in φ. We finally let the transducer T be
the set of all words (w, w ′ ) ⊆ (A × N) ∗ × B∗ such that w ′ ∈ B |w | . It
is easy to check that the resulting SDA (T , S ) is non-empty if, and3 kS k is the maximum value contained in any of the components of an element of∞
S.
4 In fact, [45] shows that the number of solutions of an existential Presburger formulawith a fixed number of variables is polynomial-time computable.

Reasoning on Data Words over Numeric Domains

only if, φ is satisfiable. Observe that NP-hardness is independentof using or not modular predicates in S, and of data classes.
6

SATISFIABILITY OF SDLIn order to prove decidability for SDL, we show an effective translation from the logic to SDA. We focus here on the upper boundsof items (1) and (2) from Theorem 4.2. The lower bound of item (2)follows by a reduction from the exponential tiling problem [42] andcan be found in the full version of this paper.
For a formulaψ , we write ψ ¬ to denote ψ ′ if ψ is of the form ¬ψ ′,or ¬ψ otherwise. Given a formula φ ∈ SDL, let sub(φ) = {ψ ,ψ ¬ :ψ a subformula of φ}. A set S ⊆ sub(φ) is a maximally consistent
set of φ on the alphabet A if it is ⊆-maximal with respect to thefollowing properties(1) for every ψ ∈ sub(φ), ψ ∈ S iff ψ ¬ < S,(2) for every ψ ,ψ ′ ∈ sub(φ), ψ ∧ ψ ′ ∈ S iff ψ ∈ S and ψ ′ ∈ S,(3) there is a ∈ A s.t. a ∈ S and for every b ∈ A \ {a}, ¬b ∈ S.
Let us write MCS(φ) to denote the set of all maximally consistentsets of φ (the alphabet being implicit). Two sets S, S ′ ∈ MCS(φ) are
one-step consistent if they satisfy(a) ψ 1 U ψ 2 ∈ S iff {ψ 1 U ψ 2,ψ 1 } ⊆ S ′ or ψ 2 ∈ S ′ ;(b) ψ 1 S ψ 2 ∈ S ′ iff {ψ 1 S ψ 2,ψ 1 } ⊆ S or ψ 2 ∈ S.
We define an exponential-sized SDA Aφ = (T , S), whose language consists of all data words that satisfy φ. We define T ⊆(A×N) ∗ ×B∗ as a transducer over the output alphabet B = MCS(φ).
T is defined as the set of all pairs ((a 1 , d 1 ) · · · (an , d n ), S 1 · · · Sn )such that(i) φ ∈ S 1 ;(ii) for every 1 ≤ i < n we have that Si , Si +1 are one-step consistent;(iii) for every 1 ≤ i ≤ n we have that ai ∈ Si ;(iv) for every 1 ≤ i ≤ n and Presburger formula α ∈ Si , we haved i |= α.
We define S ⊆ NB × NB as the set denoted by the quantifier-freeformula with variables {x =, S }S ∈B ∪ {x ,, S }S ∈B consisting on the
conjunction of:P(I) x =, S > 0 → α (( S ′ ∈B,ψ ∈S ′ x =, S ′ ) − r ) for every α,ψ , S suchthat h=iα ψ ∈ S, where r = 1 if ψ ∈ S or r = 0 otherwise;P(II) x =, S > 0 → ¬α (( S ′ ∈B,ψ ∈S ′ x =, S ′ )−r ) for every α,ψ , S suchthat ¬ h=iα ψ ∈ S, where r = 1 if ψ ∈ S or r = 0 otherwise;P(III) x =, S > 0 → α (( S ′ ∈B,ψ ∈S ′ x ,, S ′ )) for every α,ψ , S withh,iα ψ ∈ S; andP(IV) x =, S > 0 → ¬α (( S ′ ∈B,ψ ∈S ′ x ,, S ′ )) for every α,ψ , S with
¬ h,iα ψ ∈ S.
Observe that S is a single exponential quantifier-free formula.
Therefore Aφ is computable in exponential time. Hence, in thelight of Theorem 5.2–(1) we obtain a 2NEXP upper bound as statedin item (1) of Theorem 4.2. Further, if φ is in MNF, then Aφ is too.
Observe that the size of base formulas in φ is logarithmic in termsof the size of Aφ . This means that the cardinalities |[[π P ]]| thatneed to be computed for every profile P (which are singleton since
we are in MNF) are at most polynomial in Aφ , and can then becomputed in space logarithmic in Aφ . With this in mind, following the upper bound proof of Theorem 5.2–(2), we obtain a nondeterministic polynomial time algorithm in the size of Aφ for its

LICS ’22, August 2–5, 2022, Haifa, Israel

non-emptiness. This then yields the NEXP upper bound of Theorem 4.2–(2).
Lemma 6.1. A word is accepted by Aφ if, and only if, it satisfies
φ.
Proof. (⇐) Suppose first w, 1 |= φ and let us show that w
is accepted by Aφ . Let w ′ be a word of length |w | whose i-th
position is labelled with {ψ ∈ sub(φ) : w, i |= ψ }, for every i.
It is easy to verify that (i) w ′ ∈ B∗ , (ii) (w, w ′ ) ∈ T , and (iii)(Π(w ′ [Id ]), Π(w ′ [I¯d ])) ∈ S for every d ∈ N, Id = {1 ≤ i ≤ |w | :data(w )[i] = d }, and I¯d = {1, . . . , |w |} \ Id .
(⇒) Suppose now that w ∈ (A × N) ∗ is accepted by Aφ , andlet us show that w, 1 |= φ. Let w ′ ∈ B∗ be the witnessing word
used for the acceptance of w. We will show that for every position
i and subformula ψ : ψ ∈ w ′ [i] iff w, i |= ψ . We show this by induction on the size of ψ . The base case is when ψ is either (a) a lettera ∈ A which follows by condition (iii) in the definition of T , or (b)a Presburger formula α which follows by condition (iv). Boolean
combinations follow by induction as a direct consequence of thedefinition of MCS(φ).
The Until modality follows by applying the the one-stepconsistency: ψ U ψ ′ ∈ w ′ [i] iff there is some i ′ > i such thatψ ′ ∈ w ′ [i ′] and for every i < j < i ′ we have ψ ∈ w ′ [j]. The Since
modality follows analogously.
Consider finally a subformula of the form h=iα ψ ∈ sub(φ), andlet d = w N [i]. By the semilinear constraint S, we have h=iα ψ ∈w ′ [i] if, and only if, the number n of distinct positions of w ′ [Id ]containing ψ is such that n |= α. By induction, this happens iff
there are n positions 1 ≤ i 1 < · · · < i n ≤ |w ′ | such that w, i j |= ψfor all j ∈ {1, . . . , n}. Hence, h=iα ψ ∈ w ′ [i] iff w, i |= h=iα ψ . The
case of h,iα ψ is analogous.
Corollary 6.2 (of Lemma 6.1 and Corollary 5.4). The spectrum (i.e. the set of sizes of models) of any SDL formula is semilinear.

7 EXTENSIONSWe show in in this section how to extend our results with parameters and k-ary modalities.

7.1 Adding parameters
Adding parameters to SDL. We use pSDL to denote the extension of SDL with parameters. The definition is the same as before but now all Presburger formulas (base formulas and formulas
used in modalities) may use some extra free variables p 1 , . . . , pt
which correspond to the parameters. Now the satisfaction relation w, i |=σ φ is defined relative to some parameter valuation
σ : {p 1, . . . , pt } → N. For any Presburger base formula α, we define w, i |=σ α iff x, σ |= α, where x = data(w[i]). Given a wordw ∈ (A×N) ∗ , for any position 1 ≤ i ≤ |w |, we have w, i |=σ h=iβ φ(resp. w, i |= h,iβ φ) iff the number n ∈ N of positions 1 ≤ j ≤ |w |such that (i) w, j |=σ φ, (ii) data(w[j]) = data(w[i]) and (iii) j , i(resp. (i) w, j |= φ and (ii) data(w[j]) , data(w[i])) is such thatn, σ |= β. Finally, w, i |= φ holds if there exists some σ such thatw, i |=σ φ.

LICS ’22, August 2–5, 2022, Haifa, Israel

Adding parameters to SDA. To derive decidability and complexity of pSDL, we extend SDA with parameters, which we call parametric SDA (pSDA). A parametric SDA (pSDA) with t parameters, is a tuple (T , S ) as before, but the formulas in the transitionsof T may also use some parameters p 1 , . . . , pt . Now T is a regular language over A × Ψ × B, where Ψ a finite set of quantifierfree Presburger formulas with free variables x, p 1 , . . . , pt , and S isa semilinear set over NB × NB × N {p1, ...,pt } . Acceptance is defined
analogously: A word w ∈ (A × N) ∗ is accepted by (T , S ) if for somew ′ ∈ B∗ and valuation σ ∈ N {p1, ...,pt } , we have(i) (w, w ′ ) ∈ Tσ , where Tσ is the transducer without parameters
obtained by replacing each pi with σ (pi ),(ii) for every x ∈ N, (Π(w ′ [I x ]), Π(w ′ [I¯x ]), σ ) ∈ S.
where I x = {1 ≤ j ≤ |w | : data(w[j]) = x } and I¯x = {1, . . . , |w |} \Ix .
This model is still closed under union and intersection. The construction is exactly as in Proposition 5.1 (item (1)) assuming, without any loss of generality, that the parameter names used by bothautomata are disjoint.
We show that the decidability proof of Lemma 5.3 can beadapted to having parameters.
Theorem 7.1. The emptiness problem for pSDA is in NEXP and
NPNP -hard.
Proof. For the upper bound, suppose the pSDA automaton
A = (T , S ) has t parameters p 1 , . . . , pt and T is in minterm normal
form (that is, in minterm normal form for every possible instantiation of the parameters). We follow closely the proof of Lemma 5.3.
The first difference being that now φT has some t extra free variables p 1 , . . . , pt . We will need to adjust µ ∼ to take into account theparameter valuations. Observe that each n P may depend on the assignment of parameters p 1 , . . . , pt . The crux of the proof will still
be to produce a Presburger formula φ such that φ is satisfiable if
and only if A has a non-empty language. But in order to do this,we need to use two constructs in the logic, which preserve semilinearity, and which we describe next.
Given a Presburger formula φ(x̄ ) and a fresh variable y let
φ ≤y (x̄ ) be a formula with free variables x̄y. Its semantics is suchthat φ ≤y (x̄ ) is satisfied by a valuation ỹ of y and n̄ of x̄ if n̄ |=[[φ]] ≤ỹ where, recall,C ≤ỹ = {x̄ 1 + · · · + x̄ỹ ′ : ỹ ′ ≤ ỹ and x̄i ∈ C for every i}.
Observe that [[φ ≤y ]] is effectively semilinear, definable by the samestar-height 1 formula of (⋆): φ ≤y (x̄ ) = ∃y ′ψ ∗ (x̄y ′ ) ∧y ′ ≤ y, wherehyiψ (x̄y ′ ) = φ(x̄ ) ∧ y ′ = 1. It then follows that φ S (x̄ ) is definable asa star-height 1 existential formula.
Consider the following unary counting quantifier∃=x y ψ (y, p 1 , . . . , pt ) having x, p 1 , . . . , pt as free variables,
which expresses that, for a given assignment p̃ 1 , . . . , p̃t ∈ N of
p 1 , . . . , pt and x̃ ∈ N of x, there are exactly x̃ many different
valuations ỹ ∈ N of variable y such that (ỹ, p̃ 1 , . . . , p̃t ) |= ψ . It
was shown in [38] that such a quantifier preserves semilinearity.
Although the complexity was not explicitly mentioned in thepaper, the algorithm of [38] could be easily adapted to produce
an equivalent existential Presburger formula (without counting
quantifiers) in single exponential time. See the full version of

Figueira and Lin

the paper for more details. Observe that given an assignment of
p 1 , . . . , pt , the number of equivalence classes with profile P ⊆ Φis given by the satisfying valuation of y in the formula^def
φ(x, p 1 , . . . , pt ) ∧ρ P (y, p 1 , . . . , pt ) = ∃=y xφ ∈P^¬φ(x, p 1 , . . . , pt ).

φ ∈Φ\P

Hence, for a given assignment σ ∈ N {p1, ...,pt } we have that there
are finitely many distinct equivalence classes with profile P ⊆ Φ if,
and only if, σ |= ∃y ρ P .
We also define the infinite version ρ ∞P of ρ P :^def ∞φ(x, p 1 , . . . , pt ) ∧ρ∞P (p 1 , . . . , pt ) = ∃ x
φ ∈P^¬φ(x, p 1 , . . . , pt ).

φ ∈Φ\P

The quantifier ∃∞ x ψ (x, z̄) simply says there are infinitely manyx’s such that φ(x, z̄) is true. By standard results for quantifierfree and Presburger arithmetic [36], we could replace ∃∞ x ψ with∃x (x > C ∧ ψ ) for some constant C that is exponential in thesize of ψ (which can therefore be represented in polynomial size inbinary).
Then, the final formula is^defP
B P , whereµ ∼ (x̄, p̄) = ∃a ∈A,b ∈B, P ⊆Φ,φ ∈P x a,φ,b
A∧
P ⊆Φ

+/ ,
*.x
P
x a,φ,ba,φ,b =P∋φa ∈A,φ ∈Φ,b ∈B ,h∗i
BP = ρ∞
∧
φ
(τ
,
.
.
.
,
τ
,
x̄
)
∨
1
m
P
S


hyi
∃y ρ P ∧ φ S (τ1 , . . . , τm , x̄ ) , andXP
τi =x a,φ,bfor every i ∈ m.
A=

^

X

i

a ∈A,φ ∈P

As before, the language is non-empty if, and only if, φT (x̄, p̄) ∧µ ∼ (x̄, p̄) is satisfiable. Note that now any satisfying assignment
does not only yield the Parikh image under T of the witnessing
word but also the valuation for all parameters. Since the ∃=y quantifier can be eliminated in exponential time, ρ P can be translated
into an equivalent, single-exponential size existential Presburger
formula . Thus, φT (x̄, p̄) ∧ µ ∼ (x̄, p̄) is an exponential sized existential formula of star-height 1, whose satisfiability can be checked in
NP. Thus, the upper bound follows.
We now prove that pSDA emptiness is NPNP -hard. The reduction is from the standard NPNP -complete problem [25, 37] of satisfiability for quantified Boolean formulas of the form
F := ∃y1, . . . , yn ∀z 1, . . . , z n G(ȳ, z̄)
where G is a quantifier-free Boolean formula. The corresponding
pSDA (T , S ) will use the parameter p for encoding assignments toȳ, and will only have one state q, which is both initial and final. The
assignments to ȳ will be stored as the data values of the pSDA. Let
1 < r 1 < · · · < r n be the first n primes. We use the Gödel encodingReasoning on Data Words over Numeric Domains

techniques for encoding G as a Presburger formula φG . Namely byrecursive definition:(1) φG := 0 = p mod r i if G = yi ,(2) φG := 0 = x mod r i if G = z i ,(3) φG := φG 1 ∧ φG 2 if G = G 1 ∧ G 2 , and(4) φG := ¬φG 1 if G = ¬G 1 .
Q
To finish the reduction, let A = B = {a}, and R := ni=1 r i . The
only transition of T is(q, (a, φG ∧ 0 < x ≤ R, a), q)
Finally, the semilinear set S is given by the quantifier-free formulax a= = 1 ∧ x a, = R − 1. These enforce that only permutations of theword (a, 1) · · · (a, R) could be accepted by (T , S ), i.e., must containeach of the Gödel encoding of assignments for z̄ restricted to theinterval {1, . . . , R} exactly once as data values. Therefore, F is true
iff (T , S ) is nonempty.
Satisfiability of SDL. It is easy to see that the reduction of SDL to
SDA can be adapted to work also in the case of parameters, whichyields decidabilty for the satisfiability problem. We comment moreon this adaptation below when discussing extensions with k-ary
modalities.
Theorem 7.2. The satisfiability problem for pSDL is in 2NEXP.

7.2

SDL with k-ary modalities

The logic SDL (with or without parameters) can be also extended with k-ary versions of the (unary) data modalities
h=iβ (y, p̄ ) (φ) and h,iβ (y, p̄) (φ). We consider now formulas withk-ary modalities of the form h=iβ (y1, ...,yk , p̄ ) (φ 1 , . . . , φk ) andh,iβ (y1, ...,yk , p̄ ) (φ 1 , . . . , φk ).
Given a parameter valuation σ : p̄ → N, a word w ∈(A × N) ∗ , and a position 1 ≤ i ≤ |w |, we define the satisfaction relation w, i |=σ h=iβ (y1, ...,yk , p̄ ) (φ 1 , . . . , φk ) (resp. w, i |=h,iβ (y1, ...,yk , p̄ ) (φ 1 , . . . , φk )) iff n 1 , . . . , n k , σ |= β, where each n ℓ(for ℓ ∈ k) is the number of positions 1 ≤ j ≤ |w | such that (i)w, j |=σ φ ℓ , (ii) data(w[j]) = data(w[i]) and (iii) j , i (resp. (i)w, j |=σ φ ℓ and (ii) data(w[j]) , data(w[i])). As before, w, i |= φholds if w, i |=σ φ for some σ . Let us call SDL+ and pSDL+ theextensions of SDL and pSDL with k-ary modalities (for every k),
respectively.
The exponential-time translation from this further extension to
SDA can be adapted, and we obtain the following.
Theorem 7.3.
• Satisfiability for pSDL+ is in 2NEXP.
• Model-checking for SDL+ is in PTIME.
• Model-checking for pSDL+ and pSDL is NP-complete.
Proof. For satisfiability, we can translate in exponential timefrom the logic to pSDA. The translation is exactly as defined in
Section 6 but now the semilinear set S needs to be updated to take
into account the k-ary modalities semantics. That is, we define S ⊆NB ×NB ×Np̄ as the set denoted by the quantifier-free formula withvariables {x =, S }S ∈B ∪ {x ,, S }S ∈B ∪ p̄ consisting on the conjunctionof:(I) x =, S > 0 → α (t 1 , . . . , tk , p̄) for every α,ψ 1, . . . ,ψ k , S suchthat h=iα (y1, ...,yk , p̄ ) (ψ 1 , . . . ,ψ k ) ∈ S, where for each i ∈ k,

LICS ’22, August 2–5, 2022, Haifa, IsraelPti = ( S ′ ∈B,ψi ∈S ′ x =, S ′ ) − r i and r i = 1 if ψ i ∈ S or r i = 0
otherwise;(II) x =, S > 0 → ¬α (t 1 , . . . , tk , p̄) for every α,ψ 1, . . . ,ψ k , S suchthat ¬ h=iα (y1, ...,yk , p̄ ) (ψ 1 , . . . ,ψ k ) ∈ S, where for each i ∈ k,P
ti = ( S ′ ∈B,ψi ∈S ′ x =, S ′ ) − r i and r i = 1 if ψ i ∈ S or r i = 0
otherwise;(III) x =, S > 0 → α (t 1 , . . . , tk , p̄) for every α,ψ 1, . . . ,ψ k , S suchthat h,iα (y1, ...,yk , p̄ ) (ψ 1 , . . . ,ψ k ) ∈ S, where for each i ∈ k,P
ti = S ′ ∈B,ψi ∈S ′ x ,, S ′ ;(IV) x =, S > 0 → ¬α (t 1 , . . . , tk , p̄) for every α,ψ 1, . . . ,ψ k , S suchthat ¬ h,iα (y1, ...,yk , p̄ ) (ψ 1 , . . . ,ψ k ) ∈ S, where for each i ∈ k,P
ti = S ′ ∈B,ψi ∈S ′ x ,, S ′ ;Observe that S is still a singly-exponential-sized quantifier-freeformula. A similar argument as shown in Lemma 6.1 still applies
to show that the reduction preserves the language.

Regarding model-checking, the same model-checking algorithm
as shown in Proposition 4.1 works for SDL+ . To treat a subformulaof the form h=iβ (y1, ...,yk ) (ψ 1 , . . . ,ψ k ), we first count, for each data
value d of w and j ∈ k, the number n j of positions of w having
data d and satisfying ψ j , and we then mark each position i withdata d as satisfying h=iβ (y1, ...,yk ) (ψ 1 , . . . ,ψ k ) iff (n 1′ , . . . , n k′ ) |=β, where n ′j = n j − 1 if position i is marked as satisfying ψ , orn ′j = n j otherwise. Observe that this still takes polynomial time.
The treatment of h,i is similar.
On the other hand, it is easy to see that model-checking of pSDL
is NP-hard, by reduction from the satisfiability problem for existential Presburger formulas. Indeed, an existential Presburger formula ∃p 1, . . . , pt φ(p 1 , . . . , pt ) (where φ is a quantifier-free formula) is satisfiable iff the pSDL formula α (x, p 1 , . . . , pt ) with tparameters p 1 , . . . , pt is satisfiable, where α is defined as (x =x ) ∧ φ(p 1 , . . . , pt ).
For the NP upper bound, suppose we are given a word w anda pSDL+ formula φ. We first guess a function f : {1, . . . , |w |} →MCS(φ), where MCS(φ) is the set of maximally consistent sets of
subformulas of φ, as defined in Section 6. We verify that the guessing is consistent with the semantics of the logic:(1) φ ∈ f (1);(2) for every 1 ≤ i < |w | we have that f (i), f (i +1) are one-step
consistent (cf. §6);(3) for every 1 ≤ i ≤ |w | we have that ¬lab(w )[i] < f (i).
Now we can instantiate non-parametric free variables of Presburger formulas with their corresponding value:• For every base subformula α (y, p̄) and position i, let γ αi (p̄)
be the result of replacing y with data(w )[i] in α.
• For every subformula ψ := h=iβ (y1, ...,yk , p̄ ) (ψ 1 , . . . ,ψ k )and position i, let γψi (p̄) be the result of replacing in
β (y1 , . . . , yk , p̄) each y ℓ with the number of positions j , iof w such that data(w )[j] = data(w )[i] and ψ ℓ ∈ f (i).
• For every subformula ψ := h,iβ (y1, ...,yk , p̄ ) (ψ 1 , . . . ,ψ k )and position i, let γψi (p̄) be the result of replacing in
β (y1 , . . . , yk , p̄) each y ℓ with the number of positions j , iof w such that data(w )[j] , data(w )[i] and ψ ℓ ∈ f (i).
Let Ψ be the set of all γψi (p̄) formulas (for every 1 ≤ i ≤ |w | andψ ∈ f (i) of the form above) and all the formulas ¬γψi (p̄) (for every

LICS ’22, August 2–5, 2022, Haifa, Israel

1 ≤ i ≤ |w | and ¬ψ ∈ f (i)). Observe that Ψ is of polynomial
size. Finally, we check that the quantifier-free Presburger formulaVΨ(p̄) is satisfiable, which is in NP.
8

CONCLUSIONSIn this paper, we have introduced parametric semilinear data logic(pSDL), which allows different types of arithmetic reasoning (constraints on data values, letter/length counting, data counting, andaggregation) on data words. We have provided decidability anda thorough complexity analysis of the satisfiability problem forthe logic, and shown that it can express many interesting properties that cannot be expressed in existing decidable formalisms
on data words, potentially leading to interesting applications (e.g.,on querying log files and verification of array-manipulating programs). Our proof introduces also the automata counterpart ofpSDL called parameteric semilinear data automata (pSDA), which
subsume known models like Parikh automata [23], symbolic automata [14], and nondeterministic looping word automata with integer linear arithmetic [18]. We have derived decidability and complexity of emptiness for pSDA, which are of independent interests.
We would like to conclude with several open problems. Firstly,
the complexity gap between 2-NEXP and NEXP of pSDL should be
filled. At the moment, we can only bridge this gap when pSDL isrestricted to SDLMNF , which subsumes the modal logic fragmentof FO2 (<, +1, ∼). Similarly, the complexity gap for SDA and pSDA
should be filled (e.g. between NPNP and NEXP). This, in turn, raises
interesting open questions on the complexity of existential Presburger Arithmetic with unary counting quantifiers and star, which(to the best of our knowledge) is not yet studied in the literature.
Secondly, can we adapt pSDL to other infinite domains and otherdecidable theories, e.g., real linear arithmetic? The answer is far
from obvious: our proof exploits heavy machinery on Presburger
Arithmetic and semilinear sets, which include closure under star
[21, 34] and closure under unary counting quantifiers [38], which
does not hold in every decidable quantifier-free theories. Thirdly,
we believe that it is highly crucial to understand further the relationships among existing models over data words, as well as arraytheories, with respect to their expressive power. We conjecture,among others, that our logic (or maybe a slight variant thereof)
subsumes Array Folds Logic [12]. Finally, it would be interesting
to investigate if the idea of using parameters could further be exploited in other logic/automata models over data words. For example, can one still extend two-variable logics [6, 39] with parameters
while preserving decidability of satisfiability?

ACKNOWLEDGMENTS
We are extremely grateful to the anonymous reviewers for theirvaluable comments. We would also like to thank Christoph Haase,
Rupak Majumdar, Alessio Mansutti, and Philipp Rümmer for productive discussions. Diego Figueira is partially supported by ANR
QUID, grant ANR-18-CE40-0031. Anthony Lin was supported by
the ERC Starting Grant 759969 (AV-SMP) and a Max-Planck Society Fellowship.

REFERENCES[1] Eric Allender and Klaus W. Wagner. 1993. Counting Hierarchies: Polynomial
Time and Constant Depth Circuits. In Current Trends in Theoretical Computer

Figueira and Lin

Science - Essays and Tutorials, Grzegorz Rozenberg and Arto Salomaa (Eds.).
World Scientific Series in Computer Science, Vol. 40. World Scientific, 469–483.
https://doi.org/10.1142/9789812794499_0035[2] Rajeev Alur and Pavol Cerný. 2011. Streaming transducers for algorithmic verification of single-pass list-processing programs. In Annual Symposium on Principles of Programming Languages (POPL), Thomas Ball and Mooly Sagiv (Eds.).
ACM Press, 599–610. https://doi.org/10.1145/1926385.1926454[3] Rajeev Alur and Pavol Cerný. 2011. Streaming transducers for algorithmic verification of single-pass list-processing programs. In Annual Symposium on Principles of Programming Languages (POPL), Thomas Ball and Mooly Sagiv (Eds.).
ACM, 599–610. https://doi.org/10.1145/1926385.1926454[4] Michael Benedikt, Clemens Ley, and Gabriele Puppis. 2010. What You Must
Remember When Processing Data Words. In Proceedings of the Alberto Mendelzon International Workshop on Foundations of Data Management (AMW) (CEUR
Workshop Proceedings, Vol. 619), Alberto H. F. Laender and Laks V. S. Lakshmanan(Eds.). CEUR-WS.org. http://ceur-ws.org/Vol-619/paper11.pdf[5] Henrik Björklund and Thomas Schwentick. 2010. On notions of regularity
for data languages. Theoretical Computer Science 411, 4-5 (2010), 702–715.
https://doi.org/10.1016/j.tcs.2009.10.009[6] Mikołaj Bojańczyk, Claire David, Anca Muscholl, Thomas Schwentick, and Luc
Segoufin. 2011. Two-variable logic on data words. ACM Transactions on Computational Logic 12, 4 (2011), 27:1–27:26. https://doi.org/10.1145/1970398.1970403[7] Mikołaj Bojańczyk, Bartek Klin, and Sławomir Lasota. 2014. Automata theory in nominal sets. Logical Methods in Computer Science (LMCS) 10, 3 (2014).
https://doi.org/10.2168/LMCS-10(3:4)2014[8] Mikolaj Bojańczyk and Rafal Stefanski. 2020. Single-Use Automata andTransducers for Infinite Alphabets. In International Colloquium on Automata, Languages and Programming (ICALP) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 168), Artur Czumaj, Anuj Dawar,
and Emanuela Merelli (Eds.). Leibniz-Zentrum für Informatik, 113:1–113:14.
https://doi.org/10.4230/LIPIcs.ICALP.2020.113[9] Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2006. What’s Decidable
About Arrays?. In International Conference on Verification, Model Checking, andAbstract Interpretation (VMCAI) (LNCS, Vol. 3855), E. Allen Emerson and Kedar S.
Namjoshi (Eds.). Springer, 427–442. https://doi.org/10.1007/11609773_28[10] Yu-Fang Chen, Ondrej Lengál, Tony Tan, and Zhilin Wu. 2017. Register automata
with linear arithmetic. In Annual Symposium on Logic in Computer Science (LICS).
IEEE Computer Society Press, 1–12. https://doi.org/10.1109/LICS.2017.8005111[11] Wojciech Czerwinski and Lukasz Orlikowski. 2021. Reachability in Vector Addition Systems is Ackermann-complete. CoRR abs/2104.13866 (2021).
arXiv:2104.13866 https://arxiv.org/abs/2104.13866[12] Przemyslaw Daca, Thomas A. Henzinger, and Andrey Kupriyanov. 2016. Array
Folds Logic. In International Conference on Computer Aided Verification (CAV).
230–248.
[13] Loris D’Antoni, Tiago Ferreira, Matteo Sammartino, and Alexandra Silva. 2019.
Symbolic Register Automata. In International Conference on Computer Aided Verification (CAV) (LNCS, Vol. 11561), Isil Dillig and Serdar Tasiran (Eds.). Springer,
3–21. https://doi.org/10.1007/978-3-030-25540-4_1[14] Loris D’Antoni and Margus Veanes. 2017. The Power of Symbolic Automata andTransducers. In International Conference on Computer Aided Verification (CAV).
47–67. https://doi.org/10.1007/978-3-319-63387-9_3[15] Stéphane Demri and Ranko Lazić. 2009. LTL with the freeze quantifier and register automata. ACM Transactions on Computational Logic 10, 3 (2009), 16:1–16:30.
https://doi.org/10.1145/1507244.1507246[16] Stéphane Demri and Ranko Lazic. 2009. LTL with the freeze quantifier and register automata. ACM Transactions on Computational Logic 10, 3 (2009), 16:1–16:30.
https://doi.org/10.1145/1507244.1507246[17] Kousha Etessami, Moshe Y. Vardi, and Thomas Wilke. 2002. First-Order Logic
with Two Variables and Unary Temporal Logic. Inf. Comput. 179, 2 (2002), 279–
295. https://doi.org/10.1006/inco.2001.2953[18] Rachel Faran and Orna Kupferman. 2020. On Synthesis of Specifications with
Arithmetic. In International Conference on Current Trends in Theory and Practice of Informatics (SOFSEM) (LNCS, Vol. 12011), Alexander Chatzigeorgiou, Riccardo Dondi, Herodotos Herodotou, Christos A. Kapoutsis, Yannis Manolopoulos, George A. Papadopoulos, and Florian Sikora (Eds.). Springer, 161–173.
https://doi.org/10.1007/978-3-030-38919-2_14[19] Seymour Ginsburg and Edwin H. Spanier. 1966. Semigroups, Presburger formulas, and languages. Pacific J. Math. 16, 2 (1966), 285–296.
[20] Christoph Haase. 2018. A survival guide to presburger arithmetic. ACM SIGLOG
News 5, 3 (2018), 67–82. https://dl.acm.org/citation.cfm?id=3242964[21] Christoph Haase and Georg Zetzsche. 2019. Presburger arithmetic with stars,
rational subsets of graph groups, and nested zero tests. In Annual Symposium on Logic in Computer Science (LICS). IEEE Computer Society Press, 1–14.
https://doi.org/10.1109/LICS.2019.8785850[22] Michael Kaminski and Nissim Francez. 1994.
Finite-Memory Automata.
Theoretical Computer Science 134, 2 (1994), 329–363.
https://doi.org/10.1016/0304-3975(94)90242-9

Reasoning on Data Words over Numeric Domains[23] Felix Klaedtke and Harald Rueß. 2003. Monadic Second-Order Logics with Cardinalities. In International Colloquium on Automata, Languages and Programming (ICALP) (Lecture Notes in Computer Science, Vol. 2719). Springer, 681–696.
https://doi.org/10.1007/3-540-45061-0_54[24] S. Rao Kosaraju. 1982. Decidability of Reachability in Vector Addition Systems(Preliminary Version). In Symposium on Theory of Computing (STOC), Harry R.
Lewis, Barbara B. Simons, Walter A. Burkhard, and Lawrence H. Landweber(Eds.). ACM, 267–281. https://doi.org/10.1145/800070.802201[25] Dexter C. Kozen. 2006. Theory of Computation. Springer.
[26] Daniel Kroening and Ofer Strichman. 2008. Decision Procedures. Springer.
[27] Jean-Luc Lambert. 1992. A Structure to Decide Reachability in Petri Nets. Theor.
Comput. Sci. 99, 1 (1992), 79–104. https://doi.org/10.1016/0304-3975(92)90173-D[28] Jérôme Leroux. 2021.
The Reachability Problem for Petri Nets is Not
Primitive Recursive.
CoRR abs/2104.12695 (2021).
arXiv:2104.12695
https://arxiv.org/abs/2104.12695[29] Ernst W. Mayr. 1981. An Algorithm for the General Petri Net Reachability Problem. In Symposium on Theory of Computing (STOC). ACM, 238–246.
https://doi.org/10.1145/800076.802477[30] Ernst W. Mayr. 1984. An Algorithm for the General Petri Net Reachability Problem. SIAM J. Comput. 13, 3 (1984), 441–460. https://doi.org/10.1137/0213029[31] Frank Neven, Thomas Schwentick, and Victor Vianu. 2004. Finite state machines
for strings over infinite alphabets. ACM Transactions on Computational Logic 5,
3 (2004), 403–435. https://doi.org/10.1145/1013560.1013562[32] Rohit Parikh. 1966. On Context-Free Languages. J. ACM 13, 4 (1966), 570–581.
https://doi.org/10.1145/321356.321364[33] Rohit Parikh. 1966. On Context-Free Languages. J. ACM 13, 4 (1966), 570–581.
https://doi.org/10.1145/321356.321364[34] Ruzica Piskac and Viktor Kunčak. 2008.
Linear Arithmetic with
Stars. In International Conference on Computer Aided Verification(CAV) (Lecture Notes in Computer Science, Vol. 5123). Springer, 268–280.

LICS ’22, August 2–5, 2022, Haifa, Israel

https://doi.org/10.1007/978-3-540-70545-1_25[35] Mojżesz Presburger and Dale Jabcquette. 1991. On the completeness of a certain
system of arithmetic of whole numbers in which addition occurs as the only
operation. History and Philosophy of Logic 12, 2 (1991), 225–233.
[36] Bruno Scarpellini. 1984. Complexity of subcases of Presburger arithmetic. Trans.
Amer. Math. Soc. 284, 1 (1984), 203–218.
[37] Marcus Schaefer and Christopher Umans. 2002. Completeness in the polynomialtime hierarchy: A compendium. SIGACT News (2002).
[38] Nicole Schweikardt. 2005. Arithmetic, first-order logic, and counting quantifiers.
ACM Transactions on Computational Logic 6, 3 (2005), 634–671.
https://doi.org/10.1145/1071596.1071602[39] Thomas Schwentick and Thomas Zeume. 2012. Two-Variable Logic with Two
Order Relations. Logical Methods in Computer Science (LMCS) 8, 1 (2012).
https://doi.org/10.2168/LMCS-8(1:15)2012[40] Seinosuke Toda. 1991. PP is as Hard as the Polynomial-Time Hierarchy. SIAM
Journal on computing 20, 5 (1991), 865–877. https://doi.org/10.1137/0220053[41] Jacobo Torán. 1991. Complexity Classes Defined by Counting Quantifiers. J.
ACM 38, 3 (1991), 753–774. https://doi.org/10.1145/116825.116858[42] Peter van Emde Boas. 1997. The convenience of tilings. Complexity, Logic, andRecursion Theory (1997), 331–363.
[43] Kumar Neeraj Verma, Helmut Seidl, and Thomas Schwentick. 2005. On the Complexity of Equational Horn Clauses. In International Conference on AutomatedDeduction (CADE) (Lecture Notes in Computer Science, Vol. 3632). Springer, 337–
352. https://doi.org/10.1007/11532231_25[44] Klaus W. Wagner. 1987. More Complicated Questions About Maxima and Minima, and Some Closures of NP. Theoretical Computer Science 51 (1987), 53–80.
https://doi.org/10.1016/0304-3975(87)90049-1[45] Kevin Woods. 2015. Presburger Arithmetic, Rational Generating Functions,and quasi-polynomials. Journal of Symbolic Logic 80, 2 (2015), 433–449.
https://doi.org/10.1017/jsl.2015.4