=Paper=
{{Paper
|id=Vol-3875/ARQNL2024_paper7
|storemode=property
|title=On Regular Relations in Parametric Array Theories
|pdfUrl=https://ceur-ws.org/Vol-3875/ARQNL2024_paper7.pdf
|volume=Vol-3875
|authors=Rodrigo Raya
|dblpUrl=https://dblp.org/rec/conf/arqnl/Raya24
}}
==On Regular Relations in Parametric Array Theories==
https://ceur-ws.org/Vol-3875/ARQNL2024_paper7.pdf
On Regular Relations in Parametric Array Theories
Rodrigo Raya1
1
Max-Planck Institute for Software Systems, Kaiserslautern, Germany
Abstract
Parametric array theories are extensions of the quantifier-free theory of arrays with relations that hold component-
wise. Unlike more expressive theories of arrays they allow specifying linear cardinality constraints on interpreted
sets of indices, a notion close to the Härtig quantifier from model theory. We apply the notion of generalised
power of a structure to study the satisfiability problem of parametric array theories. We show that reasoning about
component-wise relations, linear cardinality constraints and succinct regular relations can be done efficiently by
reduction to propositional satisfiability. We indicate how our techniques can be adapted to theories of trees.
Keywords
decision procedures, satisfiability modulo theories, symbolic automata
1. Introduction
Many abstractions in computer science and mathematics are naturally modelled as collections of objects
of certain type. When addressing the problem of automatically verifying properties of such abstractions
it becomes crucial to choose an adequate language in which to express the properties of interest.
Our research is influenced by work in the area of deductive software verification [5, 23]. Research in
this area led to the development of specialised algorithms that determine the validity of formulas in
restricted fragments of first-order logic. The resulting algorithms are today studied in the so-called
satisfiability modulo theories (SMT) framework.
Starting with [21], first-order theories under the name of “array theories” have been studied and,
along the years, new decidable fragments and applications have been found. Bradley [6] carried out
a systematic exploration of a very expressive and decidable fragment known as the “array property
fragment”. Most notably, this fragment allowed to express the property of an array being ordered while
having an efficiently decidable satisfiable problem under mild restrictions. Moreover, Bradley’s work
showed that minor variations to the fragment’s syntax would led to undecidability, by reduction from
Hilbert’s tenth problem.
In spite of the above, and after Bradley’s work, a family of decidable array theories has been used in the
verification of so-called array-based systems [17, 26, 13, 27, 15]. This framework has been used to model
sequential programs manipulating arrays and lists, as well as parameterised concurrent systems with
local and shared variables [3, 1, 20]. These programs are essential in specialised computing scenarios
such as data-base driven systems [4] or business processes [15].
In [30, 29, 31, 32], we have investigated the structure of these array theories. We have observed
that they extend classical array theories with point-wise relations, which are defined as in the element
theory for every component of the arrays. The conclusion of our investigation is that these point-wise
relations are the essential difficulty when designing decision procedures for these theories. In particular,
we have described how the satisfiability problem of these theories can be reduced in polynomial time to
the satisfiability problem of the theory of a power structure [28] and that the latter admits an efficient
procedure for eliminating existential quantifiers [30].
Our results are applicable to a variety of array theories from the literature [10, 16, 14, 1] to which we
refer to as “parametric” array theories since they often allow to be instantiated with different index
and element theories. An interesting feature of parametric array theories is that the componentwise
ARQNL 2024: Automated Reasoning in Quantified Non-Classical Logics, 1 July 2024, Nancy, France
Envelope-Open rraya@mpi-sws.org (R. Raya)
Orcid 0000-0002-0866-9257 (R. Raya)
© 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
ceur-ws.org
ISSN 1613-0073 ARQNL 2024 80 P ROCEEDINGS
Proceedings
of two arrays 𝑎 and 𝑏 as:
relations only require one universal quantifier to be expressed. For instance, one may define the addition
𝑎 + 𝑏 = 𝑐 if and only if for every 𝑖 ∈ 𝐼 , 𝑎(𝑖) + 𝑏(𝑖) = 𝑐(𝑖)
This is in contrast to other array theories such as the array property fragment [5], which allow properties
using several related universally quantified indices. For instance, one may define in this fragment the
property of an array being ordered:
𝑎 is ordered if and only if for every 𝑖, 𝑗 ∈ 𝐼 , 𝑖 ≤ 𝑗 implies 𝑎[𝑖] ≤ 𝑎[𝑗]
While “array properties” in [5] allow several universal quantifiers, this comes at the cost of severe
syntactic restrictions. In contrast, parametric array theories offer the possibility of using linear cardi-
nality relations on sets of indices [16, 14, 1, 30]1 as well as constraints on the sums of elements of array
variables. These properties are inexpressible in the array property fragment.
These results motivate us to push further our investigation. In this paper, rather than moving to
the design of algorithms for first-order theories (which would be justified by the incipient quantifier
elimination method of [30]), we choose to further explore the possibilities in the quantifier-free setting
which is the one relevant to the satisfiability modulo theories framework.
We take inspiration from the work of Feferman and Vaught [12], who introduced the notion of
generalised power of a structure and motivated by the question of decidability of the weak monadic
second order theory of one succesor (WS1S), raised by Tarski, discuss generalised powers with this theory
of indices in the later sections of their paper. However, deciding WS1S is computationally intractable
[34]. Thus, we present the definable relations of the theory in the form of regular expressions. It was
proved by Büchi [7] that both formalisms are expressively equivalent. We refer to the relations on sets
of indices induced by regular expressions or WS1S formulas as regular relations. 2
There are several reasons that lead us to think that an extension of array theories with cardinality
constraints and regular expressions is worthwhile investigating. First, this extends the work of Alberti,
Ghilardi and Pagani [1] since it is well-known that WS1S is more expressive than Presburger arithmetic
[35]. Second, this extension allows us to express properties of arrays such as those appearing in array
folds logic [9]. While array folds logic only allows folding expressions over one array variable, this
restriction does not appear in the fragment that we present. Third, a similar extension but without
cardinality constraints has been considered concurrently to our work in [18].
Both in [18] and in our work, it seems that a non-trivial insight for the construction of the decision
algorithm is needed. We point out to the reader that this insight is materialised in our paper in the
partition variables introduced in Section 4.1. Indeed, since our specifications contain formulas whose
interpretations, as sets of indices of the arrays, may overlap, it is essential to ensure that there exists a
model adhering to the regular specification regardless of the overlaps in the semantic domain.
Unlike [18], we focus in the case of regular languages which should be more familiar to the readers.
Nevertheless, we include a final section pointing out the main ingredients of the extension to regular
tree languages. Also, for the sake of clarity, we have focused in cardinality constraints, but it should be
clear that an extension to summation constraints is also possible.
Organisation of the paper. The rest of the paper is organised as follows. Section 2 describes
generalised powers using specific theories of sets with cardinalities, theories describing their contents,
and theories describing regular relations on the indices of these sets. Section 3 describes the satisfiability
preserving encoding of arrays in generalised powers. Section 4 gives an algorithm that in polynomial
time takes as input a generalised power structure specification and outputs an equivalent formula in
1
A similar notion appears in the model theory literature under the name of Härtig’s quantifier [2].
2
We had considered regular expressions in our PhD thesis [29]. Here we consider regular expressions over first-order formulas.
This formalism has been popularised in recent times under the name of symbolic regular expression and it can also be seen
as motivated by Feferman-Vaught’s results. This is what we mean by “succinct” regular relations. We also sometimes speak
of “ordering” instead of regular relations since regular relations are precisely those expressible in the monadic theory of
order [7].
81
the combination of the quantifier-free theory of Boolean algebra of sets with Presburger arithmetic and
the alphabet’s theory. Section 5 discusses the applicability of the technique in the setting of theories of
trees, connecting to recent work. Section 6 concludes the paper.
2. Generalised powers
Let us start with the definition of generalised power structure as it is given in [12].
Definition 2.1. The generalised power 𝒫 (ℳ, 𝐼 ) of a structure ℳ = ⟨𝑀, …⟩ is a structure whose carrier
set is the set 𝑀 𝐼 of functions from the (possibly infinite) index set 𝐼 to the carrier set 𝑀 of the structure
ℳ and whose relations are interpreted as sets of the form
{(𝑎1 , … , 𝑎𝑛 ) ∈ (𝑀 𝐼 )𝑛 ∣ Φ(𝑆1 , … , 𝑆𝑘 )}
where 𝑛 is a natural number, Φ is a Boolean algebra expression over 𝒫 (𝐼 ) using the symbols ⊆, ∪, ∩ or ⋅𝑐
and each set variable 𝑆 is interpreted as
𝑆 = {𝑖 ∈ 𝐼 ∣ 𝜃(𝑎1 (𝑖), … , 𝑎𝑛 (𝑖))}
where 𝜃 is a formula in the first-order theory of ℳ.
generalised power 𝒫 (ℳ, 𝐼 ), the term “elements” for the members of the carrier set of the structure
In the following, we will use the term “arrays” for the functional elements in the carrier from a
ℳ and the term “indices” for the members of the set 𝐼. We will use the notation 𝑎(𝑖) when we want to
emphasize the algebraic perspective and the notation 𝑎[𝑖] when we want to emphasize the connection
to array theories. In particular, we will use the latter notation when describing how to translate from
parametric array theories to generalised powers.
Nothing prevents us from considering set interpretations of the form
𝑆 = {𝑖 ∈ 𝐼 ∣ 𝜓 (𝑖)}
where 𝜓 is a formula that refers only to indices in the set 𝐼. In fact, this direction is pursued in [1] where
a fragment of the theory of arrays is investigated that corresponds to a generalised power whose set
interpretations conflate both the theory of indices and the theory of elements using the quantifier-free
fragment of Presburger arithmetic to refer to both. We will use different set interpretations for indices
and elements. We will use relations of the following form:
𝐹 (𝑆1 , … , 𝑆𝑘 ) ∧ 𝑅(𝑆1 , … , 𝑆𝑘 ) ∧ 𝐶(𝑎1 , … , 𝑎𝑘 ) (1)
Here 𝐹 specifies linear cardinality constraints on the shared set variables 𝑆1 , … , 𝑆𝑘 . 𝑅 specifies the regular
relations on the set of indices 𝑆1 , … , 𝑆𝑘 . Finally, 𝐶 specifies the componentwise relations on the arrays
𝑎1 , … , 𝑎𝑘 . The precise description of Formula (1) occupies the rest of the section.
2.1. Sets of indices
Formulas 𝐹 , 𝑅 and 𝐶 in (1) use variables 𝑆1 , … , 𝑆𝑘 representing subsets of an index set 𝐼. This is explicitly
shown in (1) for 𝐹 and 𝑅. The variables 𝑆1 , … , 𝑆𝑘 are omitted from formula 𝐶 to emphasize the role of
componentwise relations on array variables. Thus, the variables 𝑆1 , … , 𝑆𝑘 are used to combine the three
theories. This approach to theory combination was pioneered in [37]. As we focus on arrays, 𝐼 = ℕ.
Generalisations to trees are also possible and in that case 𝐼 = {0, 1}∗ .
82
2.2. Linear cardinality constraints on the sets of indices
𝐹 (𝑆1 , … , 𝑆𝑘 ) is a formula in the quantifier-free theory of Boolean algebra with Presburger arithmetic
(QFBAPA) [25]. The syntax of QFBAPA is given in Figure 1. The top-level symbol 𝐹 presents the
Boolean structure of the formula, 𝐴 stands for the atomic formulas which can be either Boolean algebra
expressions on the sets denoted by the symbol 𝐵 or Presburger arithmetic restrictions on numbers
denoted by the symbol 𝑇. The operator dvd stands for the divisibility relation, which is used to ensure
algebra with Presburger arithmetic (BAPA)[24]. 𝒰 represents the universal set 𝐼. Lowercase 𝑥 and 𝑘
that the quantifier-free fragment has the same expressive power as the full first-order theory of Boolean
represent Boolean and integer variables respectively. The remaining interpretations are standard in the
respective theories (Boolean algebra of sets or Presburger arithmetic).
𝐹 ∶∶= 𝐴 | 𝐹1 ∧ 𝐹2 | 𝐹1 ∨ 𝐹2 | ¬𝐹
𝐴 ∶∶= 𝐵1 = 𝐵2 | 𝐵1 ⊆ 𝐵2 | 𝑇1 = 𝑇2 | 𝑇1 ≤ 𝑇2 | 𝐾 dvd 𝑇
𝐵 ∶∶= 𝑥 | ∅ | 𝒰 | 𝐵1 ∪ 𝐵2 | 𝐵1 ∩ 𝐵2 | 𝐵𝑐
𝑇 ∶∶= 𝑘 | 𝐾 | 𝑇1 + 𝑇2 | 𝐾 ⋅ 𝑇 | |𝐵|
𝐾 ∶∶= … | − 2 | − 1 | 0 | 1 | 2 | …
Figure 1: QFBAPA’s syntax
Example 2.1. An example of QFBAPA formula is |𝐴| > 1 ∧ 𝐴 ⊆ 𝐵 ∧ |𝐵 ∩ 𝐶| ≤ 2.
2.3. Componentwise relations on arrays
𝐶(𝑎1 , … , 𝑎𝑘 ) is a formula specifying componentwise relations. It does so with set interpretations of the
𝑆𝑗 = {𝑖 ∈ 𝐼 ∣ 𝜙𝑗 (𝑎(𝑖), 𝑐)}
form:
where 𝑎 denotes a tuple of array variables, 𝑐 denotes a tuple of constants from the element theory and
𝜙𝑗 is a formula of the element theory. As in Definition 2.1, 𝑎(𝑖) denotes the 𝑖-th position of array 𝑎 and
𝑎(𝑖) = (𝑎1 (𝑖), … , 𝑎𝑘 (𝑖)).
Example 2.2. The equality between two arrays 𝑎1 and 𝑎2 can be written in the fragment of (1) as:
𝑆 = {𝑖 ∈ 𝐼 ∣ 𝑎1 (𝑖) = 𝑎2 (𝑖)} ∧ |𝑆| = |𝒰|
where 𝒰 as explained above, represents the universal set 𝐼.
2.4. Regular relations on the set of indices
𝑅(𝑆1 , … , 𝑆𝑘 ) is a formula specifying regular relations in the set of indices. For instance, the array could
be specified by the symbolic regular expression:3
𝜙1 (𝑒, 𝑐)(𝜙1 (𝑒, 𝑐) ∨ 𝜙2 (𝑒, 𝑐))∗ 𝜙3 (𝑒, 𝑐) (2)
This specifies that the first element 𝑒 of the array satisfies the formula 𝜙1 (𝑒, 𝑐), then there is a sequence
of zero or more elements 𝑒 satisfying either 𝜙1 (𝑒, 𝑐) or 𝜙2 (𝑒, 𝑐) and the last element 𝑒 satisfies the formula
𝜙3 (𝑒, 𝑐). Each instantiation of 𝑒 is different for each witness, while the value of the parameters in 𝑐 must
be the same for the whole array. However, this approach conflates the specifications of the indices and
the specifications of the elements of the arrays.
3
There are several possibilities to write regular relations. Here we use regular expressions for economy of notation.
83
Let us instead write a symbolic version of the regular expression above
𝑆1 (𝑆1 ∨ 𝑆2 )∗ 𝑆3 (3)
To relate this symbolic expression and the theory of the elements, we let 𝑡 be a sequence of bit-strings
𝑡 ∈ ({0, 1}3 )∗ and define
𝑆1 = {𝑖 ∈ 𝐼 ∣ 𝑡1 (𝑖) = 1} ∧ 𝑆1 = {𝑖 ∈ 𝐼 ∣ 𝜙1 (𝑎(𝑖), 𝑐)}
𝑆2 = {𝑖 ∈ 𝐼 ∣ 𝑡2 (𝑖) = 1} ∧ 𝑆2 = {𝑖 ∈ 𝐼 ∣ 𝜙2 (𝑎(𝑖), 𝑐)} (4)
𝑆3 = {𝑖 ∈ 𝐼 ∣ 𝑡3 (𝑖) = 1} ∧ 𝑆3 = {𝑖 ∈ 𝐼 ∣ 𝜙3 (𝑎(𝑖), 𝑐)}
where 𝑡1 , 𝑡2 and 𝑡3 denote, respectively, the first, second and third rows of the sequence and 𝑡𝑗 (𝑖) denotes
the 𝑖-th position in 𝑡𝑗 .
Then, satisfiability of (2) is equivalent to satisfiability of
∃𝑡 ∈ ({0, 1}3 )∗ .𝑡 ⊧ 𝑆1 (𝑆1 ∨ 𝑆2 )∗ 𝑆3 ∧ (4) (5)
where 𝑡 ⊧ 𝑅(𝑆1 , … , 𝑆𝑘 ) means that the bit-string sequence 𝑡 satisfies propositionally the regular expression
𝑅(𝑆1 , … , 𝑆𝑘 ), that is, there is a word 𝑤 of propositional formulas over the variables 𝑆1 , 𝑆2 and 𝑆3 generated
by 𝑅 such that for each 𝑖, 𝑡(𝑖) ⊧ 𝑤(𝑖) propositionally.
Example 2.3. A bit-string sequence 𝑡 belonging to the language of the symbolic regular expression
𝑆1 (𝑆1 ∨ 𝑆2 )∗ 𝑆3 is the following
1 1 0 0 0
(1) (0) (1) (1) (0)
0 0 0 1 1
The values of its rows are respectively 𝑡1 = 11000, 𝑡2 = 10110 and 𝑡3 = 00011.
It satisfies the word of propositional formulas 𝑆1 (𝑆1 ∨ 𝑆2 )(𝑆1 ∨ 𝑆2 )(𝑆1 ∨ 𝑆2 )𝑆3 which is generated by
𝑆1 (𝑆1 ∨ 𝑆2 )∗ 𝑆3 .
We call the bit-string sequences 𝑡 regular tables or simply tables and write 𝑇 (𝑅) for the set of all
tables satisfying the symbolic regular expression 𝑅.
3. Encoding of arrays
Let us briefly mention how would the terms of an array theory, most importantly, array “reads” and
“writes”, be written in the language of generalised powers, while preserving the satisfiability of formulas.
An array read is a functional term 𝑎[𝑗]. To encode this term in generalised powers, we introduce the
A componentwise specification is written as in Example 2.2.
set variable 𝐽 representing the singleton set {𝑗} and require that |𝐽 | = 1. We then introduce an element
theory variable 𝑎𝑗 and require that {𝑖 ∈ 𝐼 ∣ 𝑎(𝑖) = 𝑎𝑗 } ⊇ 𝐽.
An array write is a functional term 𝑠𝑡𝑜𝑟𝑒(𝑎, 𝑗, 𝑣). To encode this term in generalised powers, we
introduce a new variable 𝑏 to stand for the term 𝑠𝑡𝑜𝑟𝑒(𝑎, 𝑗, 𝑣) and require that {𝑖 ∈ 𝐼 ∣ 𝑏(𝑖) = 𝑣} ⊇ 𝐽 and
{𝑖 ∈ 𝐼 ∣ 𝑎(𝑖) = 𝑏(𝑖)} ⊇ 𝒰 ∖ 𝐽.
Example 3.1. Consider the array formula from [5].
𝑖1 = 𝑗 ∧ 𝑖1 ≠ 𝑖2 ∧ 𝑎[𝑗] = 𝑣1 ∧ 𝑠𝑡𝑜𝑟𝑒(𝑠𝑡𝑜𝑟𝑒(𝑎, 𝑖1 , 𝑣1 ), 𝑖2 , 𝑣2 )[𝑗] ≠ 𝑎[𝑗]
For each index variable 𝑗, 𝑖1 , 𝑖2 , we introduce set variables 𝐽 , 𝐼1 , 𝐼2 and impose that 𝐼1 = 𝐽, 𝐼1 ≠ 𝐼2 and
|𝐼1 | = |𝐼2 | = |𝐽 |.
The term 𝑎[𝑗] = 𝑣1 is translated into {𝑖 ∈ 𝐼 ∣ 𝑎(𝑖) = 𝑣1 } ⊇ 𝐽.
We introduce the array variables 𝑏 for 𝑠𝑡𝑜𝑟𝑒(𝑎, 𝑖1 , 𝑣1 ) and 𝑐 for 𝑠𝑡𝑜𝑟𝑒(𝑏, 𝑖2 , 𝑣2 ). We can then encode the
fourth conjunct as {𝑖 ∈ 𝐼 ∣ 𝑐(𝑖) ≠ 𝑎(𝑖)} ⊇ 𝐽. The store operators are encoded as indicated above.
The resulting formula is in the theory of the generalised power and is equisatisfiable to the original.
84
4. Deciding generalised powers
Let us now give a method to decide satisfiability of formulas of the form (1). These are of the following
form:
𝐹 (𝑆1 , … , 𝑆𝑘 ) ∧ ∃𝑡 ∈ 𝑇 (𝑅). ⋀ 𝑆𝑖 = { 𝑛 ∈ ℕ | 𝜙𝑖 (𝑎(𝑛), 𝑐) } = { 𝑛 ∈ ℕ | 𝑡𝑖 (𝑛) = 1 }
𝑘
(6)
𝑖=1
The satisfiability problem requires showing that the following formula is true:
∃𝑎 ∈ 𝒟 ∗ ,𝑡 ∈ 𝑇 (𝑅), 𝑐.
𝐹 (𝑆1 , … , 𝑆𝑘 ) ∧ ⋀ 𝑆𝑖 = { 𝑛 ∈ ℕ ∣ 𝜙𝑖 (𝑎(𝑛), 𝑐) } = { 𝑛 ∈ ℕ ∣ 𝑡𝑖 (𝑛) = 1 }
𝑘 (7)
where 𝒟 is the domain of the array elements.
𝑖=1
existential fragment of the first-order theory of the domain 𝒟 such that Formula (7) is equivalent to the
We show how to compute in polynomial time a formula in the combination of QFBAPA and the
computed formula.
formula (8) in the combination of QFBAPA and the existential fragment of the first-order theory of 𝒟,
Theorem 4.1. There is a polynomial time algorithm that given formula (7) computes an equivalent
𝑇 ℎ∃∗ (𝒟 ).
4.1. Construction of the equivalent formula
and 𝑇 ℎ∃∗ (𝒟 )
The equivalent formula has three parts. The first is an existential prefix shared between both QFBAPA
∃𝑁 ≤ 𝑝(|𝐹 |), ∃𝑠 ∈ [𝑚], 𝜎 ∶ [𝑠] ↪ [𝑚], ∃𝛽1 , … , 𝛽𝑁 ∈ {0, 1}𝑘 .
where 𝑁 is a natural number, 𝑝 is a polynomial, |𝐹 | is the number of symbols used to write 𝐹, [𝑛] ∶=
{ 1, … , 𝑛 } abbreviates the set of the first 𝑛 natural numbers, 𝑚 is the number of propositional formulas
used in 𝑀𝑆 , 𝜎 is an injection from [𝑠] to [𝑚] and 𝑘 is the number of set variables used in 𝐹.
The second part of the formula is an expression in the theory 𝑇 ℎ∃∗ (𝒟 )
𝐶(𝛽1 , … , 𝛽𝑁 ) ∶= ∃𝑐. ⋀ ∃𝑒 ∈ 𝐷.𝜙 𝛽𝑗 (𝑒, 𝑐)
𝑁
where we use the notation that given the list 𝜙1 , … , 𝜙𝑘 of formulas specifying the elements in Formula 6
𝑗=1
and given a bit-string 𝛽 ∈ {0, 1}𝑘 , 𝜙 𝛽 ∶= ⋀𝑖=1 𝜙𝑖 .
𝑘 𝛽(𝑖)
The third part of the formula is in QFBAPA
𝐻 (𝑐1 , … , 𝑐𝑘 , …) ∶=𝜌(𝑐1 , … , 𝑐𝑚 ) ∧ 𝐹 (𝑆1 , … , 𝑆𝑘 ) ∧ ⋀ 𝑃𝑖 ⊆ 𝑝𝐿𝜎(𝑖) ∧
𝑠
𝑖=1
⋀ |𝑃𝑖 | = 𝑐𝜎 (𝑖) ∧ ∪𝑘𝑖=1 𝑆𝑖 = ∪𝑚
𝑖=1 𝑝𝐿𝑖 = ∪𝑖=1 𝑝𝛽𝑖 = ∪̇ 𝑖=1 𝑃𝑖
𝑠
𝑁 𝑠
where 𝜌 is a formula in the existential fragment of Presburger arithmetic of size linear in the size of the
𝑖=1
regular expression 𝑅. 𝜌 describes the Parikh image of 𝑅. The description of the Parikh image in terms
of linear-size existential Presburger arithmetic formulas is based on a result from [33].
The Parikh image of a symbolic regular expression 𝑅 using propositional letters 𝐿1 , … , 𝐿𝑚 over the
Definition 4.1 (Parikh Image).
variables 𝑆1 , … , 𝑆𝑘 is the set
Parikh(𝑅) = {(|𝑠|𝐿1 , … , |𝑠|𝐿𝑚 ) ∣ 𝑠 ∈ 𝑀𝑆 (𝐿1 , … , 𝐿𝑚 )}
where 𝑠 is a word of propositional formulas and |𝑠|𝐿𝑖 is the number of occurrences of 𝐿𝑖 in the symbolic
table 𝑠.
85
Example 4.1. Continuing Example 2.3, we had a symbolic regular expression 𝑆1 (𝑆1 ∨ 𝑆2 )∗ 𝑆3 and a word
of propositional formulas 𝑆1 (𝑆1 ∨ 𝑆2 )(𝑆1 ∨ 𝑆2 )(𝑆1 ∨ 𝑆2 )𝑆3 . Thus, one vector in the Parikh image is (1, 3, 1).
In general, the Parikh image of 𝑆1 (𝑆1 ∨ 𝑆2 )∗ 𝑆3 would contain the vectors (1, 𝑘, 1) for each 𝑘 ∈ ℕ.
Continuing with the description of the third part of the formula, 𝐹 is the QFBAPA term in Formula 6,
𝑝𝛽 ∶= ∩𝑘𝑖=1 𝑆𝑖 where 𝛽 ∈ {0, 1}𝑘 , 𝑝𝐿 ∶= ∪𝛽⊧𝐿 𝑝𝛽 where ⊧ is the propositional satisfaction relation and
𝛽(𝑖)
𝛽 ∈ {0, 1}𝑘 , | ⋅ | denotes the cardinality of the argument set expression, ∪̇ 𝑖∈𝐼 𝑆𝑖 is the set ∪𝑖∈𝐼 𝑆𝑖 where we
emphasize that each pair of sets 𝑆𝑖 , 𝑆𝑗 are disjoint.
Shortening tuples of variables with an overline, we write Formula (8) as
∃𝑁 ≤ 𝑝(|𝐹 |), ∃𝑠 ∈ [𝑚], 𝜎 ∶ [𝑠] ↪ [𝑚], ∃𝛽 ∈ {0, 1}𝑘 .𝐶(𝛽) ∧ ∃𝑐, 𝑃.𝐻 (𝑐, 𝑃, 𝛽) (8)
Intuitively, the partition variables 𝑃𝑖 determine which propositional formula generated each value
This formula can be computed in polynomial time.
of the arrays accepted, so that, even if these formulas overlap, a model corresponding to a run of the
automaton can be rebuilt. The reason why we need to check the existence of only one witness per
that satisfied the corresponding formula 𝜙 𝛽 (see also [30, 31]).
elementary Venn region follows from the fact that we can “replicate” this witness in each of the indices
4.2. Proof of the theorem
We prove that Formula (6) and Formula (13) are equivalent.
⇒) If Formula (7) is true, then there are sets 𝑆1 , … , 𝑆𝑘 , a finite array 𝑎 and a table 𝑡 ∈ 𝑇 (𝑅) such that
𝐹 (𝑆1 , … , 𝑆𝑘 ) ∧ ⋀ 𝑆𝑖 = { 𝑛 ∈ ℕ | 𝜙𝑖 (𝑎(𝑛), 𝑐) } = { 𝑛 ∈ ℕ | 𝑡𝑖 (𝑛) = 1 }
𝑘
(9)
𝑖=1
Let 𝑠 be the symbolic table corresponding to 𝑡, that is, the table made of the propositional formulas
generated by 𝑅(𝑆1 , … , 𝑆𝑘 ) such that 𝑡 satisfies 𝑠.
Define 𝑐𝑖 ∶= |𝑠|𝐿𝑖 for 𝑖 ∈ {1, … , 𝑚} as the number of occurrences of 𝐿𝑖 in the symbolic table 𝑠, 𝑠 =
| { 𝑖 | 𝑐𝑖 ≠ 0 } |, 𝜎 mapping the indices in [𝑠] to the indices 𝑖 of the terms for which 𝑐𝑖 is non-zero and
𝑃𝑖 = { 𝑛 ∈ ℕ | 𝑠(𝑛) = 𝐿𝜎 (𝑖) }. From the equalities 𝑆𝑖 = { 𝑛 ∈ ℕ | 𝑡𝑖 (𝑛) = 1 } = { 𝑛 ∈ ℕ | 𝜙𝑖 (𝑎(𝑛), 𝑐) } in (9),
we can show that the following holds
𝜌(𝑐1 , … , 𝑐𝑚 ) ∧ 𝐹 (𝑆1 , … , 𝑆𝑘 ) ∧ ⋀ 𝑃𝑖 ⊆ 𝑝𝐿𝜎(𝑖) ∧
𝑠
𝑖=1
(10)
⋀ |𝑃𝑖 | = 𝑐𝜎 (𝑖) ∧ ∪𝑘𝑖=1 𝑆𝑖 = ∪𝑚
𝑖=1 𝑝𝐿𝑖 = ∪̇ 𝑖=1 𝑃𝑖
𝑠
𝑠
𝑖=1
Formula (10) is in QFBAPA. Following the procedure from [25], we eliminate Boolean algebra
expressions and the cardinality operator yielding a system of equations of the form
𝑘1
∃𝑘1 , … , 𝑘𝑝 .𝐺 ∧ ∑ ( ⋮ ) ⋅ 𝑙𝛽𝑗 = ( ⋮ )
2𝑘 −1J𝑏0 K𝛽𝑗
𝑘𝑝
(11)
𝑗=0 J𝑏𝑝 K𝛽
𝑗
where 𝐺 is the existential Presburger arithmetic formula that results from (10) after the elimination and
𝑙𝛽𝑗 = |𝑝𝛽𝑗 |.
We remove from the sum those terms corresponding to elementary Venn regions 𝛽 such that 𝑙𝛽 = 0.
This includes regions whose associated formula in the interpreted Boolean algebra 𝜙 𝛽 (𝑎, 𝑐) is unsatisfiable,
86
and regions corresponding to bit-strings not occurring in 𝑡. This transformation leaves a reduced set of
indices ℛ participating in the sum:
𝑘1
∃𝑘1 , … , 𝑘𝑝 .𝐺 ∧ ∑ ( ⋮ ) ⋅ 𝑙𝛽𝑗 = ( ⋮ )
J𝑏0 K𝛽𝑗
𝑘𝑝
(12)
𝛽∈{ 𝛽1 ,…,𝛽𝑁 }⊆ℛ J𝑏𝑝 K𝛽
𝑗
We now give the key auxiliary result from [25] proved in [11].
Definition 4.2. Given a subset 𝑆 ⊆ ℝ𝑛 , the integer conic hull of 𝑆 is the set
𝑖𝑛𝑡𝑐𝑜𝑛𝑒 (𝑆) = { ∑ 𝜆𝑖 𝑠𝑖 |𝑡 ≥ 0, 𝑠𝑖 ∈ 𝑆, 𝜆𝑖 ∈ ℕ}
𝑡
𝑖=1
Theorem 4.2. Let 𝑋 ⊆ ℤ𝑛 be a finite set of integer vectors, 𝑏 ∈ 𝑖𝑛𝑡𝑐𝑜𝑛𝑒 (𝑋 ) and 𝑀 = maxx∈𝑋 ‖x‖∞ =
maxx∈𝑋 max{|𝑥1 |, … , |𝑥𝑛 |} where |𝑥| denotes the absolute value of the number 𝑥. There exists a subset
𝑋 ′ ⊆ 𝑋 such that 𝑏 ∈ 𝑖𝑛𝑡𝑐𝑜𝑛𝑒 (𝑋 ′ ) and |𝑋 ′ | ≤ 2𝑛 log2 (4𝑛𝑀) where |𝑋 ′ | denotes the cardinality of the set
𝑋 ′.
Using Theorem 4.2, there is a polynomial family of Venn regions 𝛽1 , … , 𝛽𝑁 and corresponding
cardinalities 𝑙𝛽′1 , … , 𝑙𝛽′𝑁 such that:
𝑘1
∃𝑘1 , … , 𝑘𝑝 .𝐺 ∧ ∑ ( ⋮ ) ⋅ 𝑙𝛽𝑗 = ( ⋮ )
J𝑏0 K𝛽𝑗
′
𝑘𝑝
(13)
𝛽∈{ 𝛽1 ,…,𝛽𝑁 }⊆ℛ J𝑏𝑝 K𝛽
𝑗
We can assume that each cardinality variable 𝑙𝛽′ is non-zero, since otherwise, we can remove it from
the sum. With this assumption, 𝑙𝛽′1 , … , 𝑙𝛽′𝑁 lists the cardinalities of a model of (10) which defines the
cardinality of the elementary Venn region 𝑆1 1 ∩ … ∩ 𝑆𝑘 𝑘 to be equal to 𝑙𝛽′ if 𝛽 ∈ {𝛽1 , … , 𝛽𝑁 } and zero
′𝛽 ′𝛽
otherwise. In particular, we have that the following formula, corresponding to the subformula 𝐻 in (8),
holds
𝜌(𝑐1 , … , 𝑐𝑚 ) ∧ 𝐹 (𝑆1′ , … , 𝑆𝑘′ ) ∧ ⋀ 𝑃𝑖′ ⊆ 𝑝𝐿′ 𝜎(𝑖) ∧
𝑘
𝑖=1 (14)
⋀ |𝑃𝑖′ | = 𝑐𝜎 (𝑖) ∧ ∪𝑘𝑖=1 𝑆𝑖′ = ∪𝑚
𝑖=1 𝑝𝐿𝑖 = ∪𝑖=1 𝑝𝛽𝑖 = ∪̇ 𝑖=1 𝑃𝑖
𝑠
′ 𝑁 𝑠 ′
𝑖=1
For each 𝛽 ∈ {𝛽1 , … , 𝛽𝑁 }, the formula ∃𝑒.𝜙 𝛽 (𝑒, 𝑐) is true, since 𝑙𝛽′ > 0. Thus, the subformula 𝐶 in (8) is
also true.
⇐) If Formula (8) is true, then there is a natural number 𝑁 ≤ 𝑝(|𝐹 |) where 𝑝 is a polynomial, 𝑠 ∈ [𝑚],
𝛽1 , … , 𝛽𝑁 ∈ {0, 1}𝑘 , 𝑐1 , … , 𝑐𝑚 ∈ ℕ and sets 𝑆1 , … , 𝑆𝑘 , 𝑃1 , … , 𝑃𝑠 such that
∃𝑐. ⋀ ∃𝑒.𝜙 𝛽𝑗 (𝑒, 𝑐) ∧ 𝜌(𝑐1 , … , 𝑐𝑚 ) ∧ 𝐹 (𝑆1 , … , 𝑆𝑘 ) ∧ ⋀ 𝑃𝑖 ⊆ 𝑝𝐿𝜎(𝑖) ∧
𝑁 𝑠
𝑗=1 𝑖=1
(15)
∧ ⋀ |𝑃𝑖 | = 𝑐𝜎 (𝑖) ∧ ∪𝑘𝑖=1 𝑆𝑖 = ∪𝑚
𝑖=1 𝑝𝐿𝑖 = ∪̇ 𝑖=1 𝑃𝑖 = ∪𝑖=1 𝑝𝛽𝑖
𝑠
𝑠 𝑁
𝑖=1
From (15) and the definition of 𝜌, follows that there is a symbolic table 𝑠 generated by the symbolic
regular expression 𝑅 such that |𝑠|𝐿𝑖 = 𝑐𝑖 for each 𝐿𝑖 ∈ { 𝐿1 , … , 𝐿𝑚 } occurring in 𝑠. Moreover, from
⋀ 𝑃𝑖 ⊆ 𝑝𝐿𝜎(𝑖) ∧ ∪𝑚
𝑖=1 𝑝𝐿𝑖 = ∪̇ 𝑖=1 𝑃𝑖
𝑠
𝑠
𝑖=1
87
we have that all the sets 𝑝𝐿𝑖 are empty except 𝑝𝐿𝜎(1) , … , 𝑝𝐿𝜎(𝑠) .
From the subformula
𝑖=1 𝑝𝐿𝑖 = ∪̇ 𝑖=1 𝑃𝑖 ∧ ⋀ 𝑃𝑖 ⊆ 𝑝𝐿𝜎(𝑖) ∧ ⋀ |𝑃𝑖 | = 𝑐𝜎 (𝑖)
∪𝑚
𝑠 𝑠
𝑠
𝑖=1 𝑖=1
follows that we may define 𝑃𝑖 to consist of the indices of 𝑠 labelled with the formula 𝐿𝜎 (𝑖) for each
𝑖 ∈ {1, … , 𝑠}. This is because the values in 𝑃𝑖 are guaranteed to satisfy the formula 𝐿𝜎 (𝑖) . Note that the
values in 𝑃𝑖 could satisfy other formulas 𝐿𝜎 (𝑗) . However, the role of the variables 𝑃𝑖 is to determine
which formula of the regular expression generated the values satisfying 𝐿𝜎 (𝑖) regardless of whether the
witnesses satisfied other formulas too.
From the subformula
∃𝑐. ⋀ ∃𝑒.𝜙 𝛽𝑗 (𝑒, 𝑐) ∧ ∪̇ 𝑠𝑖=1 𝑃𝑖 = ∪𝑁
𝑖=1 𝑝𝛽𝑖
𝑁
𝑗=1
it follows that there exist values 𝑒𝛽1 , … , 𝑒𝛽𝑁 satisfying the formulas 𝜙 𝛽1 (𝑒, 𝑐), … , 𝜙 𝛽𝑁 (𝑒, 𝑐) and moreover,
all the elements in 𝑝𝛽𝑗 belong to a single set 𝑃𝑖 .
We define a table 𝑡 by substituting in 𝑠 the indices in 𝑃𝑖 by the values 𝛽𝑗 such that 𝑝𝛽𝑗 ⊆ 𝑃𝑖 . Similarly,
we build an array 𝑎 by substituting in 𝑠 the indices in 𝑃𝑖 by the values 𝑒𝛽𝑗 such that 𝑝𝛽𝑗 ⊆ 𝑃𝑖 .
Observe that 𝐹 (𝑆1 , … , 𝑆𝑘 ) holds by assumption. Moreover,
𝑆𝑗 = ∪{𝑖∣𝛽𝑖 (𝑗)=1} 𝑝𝛽𝑖 = { 𝑛 ∈ ℕ ∣ 𝑡𝑗 (𝑛) = 1 }
𝑆𝑗 = ∪{𝑖∣𝛽𝑖 (𝑗)=1} 𝑝𝛽𝑖 = { 𝑛 ∈ ℕ ∣ 𝜙𝑗 (𝑎(𝑛), 𝑐) }
Thus, Formula (7) is true.
4.3. Computational complexity of the combination
Note that Theorem 4.1 also allows to assert at once the complexity of the underlying logical theory.
Corollary 4.1. Let 𝒞 be the complexity class to which the satisfiability problem of 𝑇 ℎ∃∗ (𝒟 ) belongs.
If 𝒞 = P then the satisfiability problem of formulas of the form (6) is in NP. If 𝒞 ⊇ NP then the
satisfiability problem of formulas of the form (6) is in 𝒞.
5. The case of trees
One can adapt the techniques of Section 4 to the case when the regular specification is given by a
parametric tree automaton, thus extending the results of [18]. The main difference with the procedure
of Section 4 is that in the case of parametric tree automata one needs to compute the Parikh image
of a regular tree language. This is done in a completely analogous way as it is done in Definition 4.1
for parametric finite automata. Note that it is easy to convert from non-deterministic top-down to
non-deterministic bottom-up tree automata [8, Theorem 1.6.1]. One can then use the observation of
Klaedtke and Rueß [22, Lemma 17] which allows to reduce the problem to the computation of the Parikh
image of a context-free grammar. Finally, [36] says that the Parikh image of a context-free grammar
can be described by a linear-sized existential Presburger arithmetic formula.
6. Conclusion
We have shown how to extend decision procedures for satisfiability of parametric array fragments
with regular constraints. In terms of quantifiers, this shows how to simultaneously support Härtig’s
quantifiers and WS1S second-order quantification. Our techniques extend previous results of Alberti,
Ghilardi and Pagani [1] since the relations expressible in WS1S extend those expressible in Presburger
88
arithmetic. They also extend recent results in the literature [18], which did not handle the cardinality
operator.
Our work mixes ideas from decision algorithms for three different logical theories: quantifier-free
BAPA [25], combinations of BAPA with WS1S and WS2S [37] and existential fragment of power struc-
tures [30]. However, a crucial technical difficulty has been overcome to make the combination work.
This difficulty stems from the fact that while Büchi’s automata are over finite alphabets, the correspond-
ing automata (or equivalently, regular expressions) that appear in the Feferman-Vaught framework use
first-order formulas in their transitions, since set variables are interpreted. We demonstrated, as our
colleagues [18], that one can still use the Parikh image of this symbolic automata to combine theories.
Since one is now counting formulas rather than symbols from a finite alphabet, and formulas can
overlap in the semantic domain, it becomes necessary to indicate to the QFBAPA constraint which
transition of the automaton produced each index. We achieved this by introducing a partition of the
sets of indices of the array, where each part corresponds to the indices generated by a given transition.
The implementation of the algorithm could be achieved mixing the techniques of ARCA-SAT [1]
with software computing the Parikh image of regular expressions and context-free grammars. For the
latter, there exist several implementations, we mention for instance [19], where a fix to the construction
original of Verma et alii [36], is also described.
Possible applications of the decision procedure include automatic verification of array manipulating
programs in deductive verification systems and model checking of distributed protocols. Nevertheless,
due to the number of ideas that are combined in this work, we would not be surprised if further
applications are found in the future.
Acknowledgements
The author wishes to express his gratitude to Viktor Kunčak for suggesting us the application of the
methods of our thesis to symbolic automata. Anthony Lin and Oliver Markgraf provided useful remarks
on the final presentation of the results in this paper. Research supported by the Swiss NSF Project
P500PT_222338
References
[1] F. Alberti, S. Ghilardi, and E. Pagani. Cardinality constraints for arrays (decidability results and
applications). Formal Methods in System Design, 51(3):545–574, December 2017. doi:10.1007/
s10703-017-0279-6.
[2] J. Barwise and S. Feferman, editors. Model-Theoretic Logics. Perspectives in Logic. Cambridge
University Press, Cambridge, 2017. doi:10.1017/9781316717158.
[3] Roderick Bloem, Ayrat Khalimov, Swen Jacobs, Igor Konnov, Helmut Veith, Josef Widder, and Sasha
Rubin. Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing
Theory. Springer International Publishing, Cham, 2015. doi:10.1007/978-3-031-02011-7.
[4] Mikołaj Bojańczyk, Luc Segoufin, and Szymon Toruńczyk. Verification of database-driven systems
via amalgamation. In Proceedings of the 32nd ACM SIGMOD-SIGACT-SIGAI symposium on Principles
of database systems, PODS ’13, pages 63–74, New York, NY, USA, June 2013. Association for
Computing Machinery. doi:10.1145/2463664.2465228.
[5] Aaron Bradley and Zohar Manna. Calculus of computation: decision procedures with applications to
verification. Springer, Berlin, 2007. OCLC: ocn190764844.
[6] Aaron R Bradley. Safety analysis of systems. PhD thesis, Stanford University, May 2007.
[7] J. Richard Büchi. Weak Second-Order Arithmetic and Finite Automata. Mathematical Logic
Quarterly, 6(1-6):66–92, 1960. doi:10.1002/malq.19600060105.
[8] Hubert Comon, Max Dauchet, Remi Gilleron, Florent Jacquemard, Denis Lugiez, Christof Loding,
Sophie Tison, and Marc Tommasi. Tree Automata Techniques and Applications. INRIA, 2008.
89
[9] Przemysław Daca, Thomas A. Henzinger, and Andrey Kupriyanov. Array Folds Logic. In Computer
Aided Verification, Lecture Notes in Computer Science, pages 230–248, Cham, 2016. Springer
International Publishing. doi:10.1007/978-3-319-41540-6_13.
[10] Leonardo de Moura and Nikolaj Bjorner. Generalized, efficient array decision procedures. In
2009 Formal Methods in Computer-Aided Design, pages 45–52, Austin, TX, November 2009. IEEE.
doi:10.1109/FMCAD.2009.5351142.
[11] Friedrich Eisenbrand and Gennady Shmonin. Carathéodory bounds for integer cones. Operations
Research Letters, 34(5):564–568, September 2006. doi:10.1016/j.orl.2005.09.008.
[12] S. Feferman and R. Vaught. The first order properties of products of algebraic systems. Fundamenta
Mathematicae, 47(1):57–103, 1959.
[13] Paolo Felli, Alessandro Gianola, and Marco Montali. SMT-based Safety Checking of Parameterized
Multi-Agent Systems. Proceedings of the AAAI Conference on Artificial Intelligence, 35(7):6321–6330,
May 2021. Number: 7. URL: https://ojs.aaai.org/index.php/AAAI/article/view/16785, doi:10.
1609/aaai.v35i7.16785.
[14] Klaus Freiherr von Gleissenthall. Cardinalities in Software Verification. PhD thesis, Technische
Universität München, Fakultät für Informatik, 2016.
[15] Alessandro Gianola. Verification of Data-Aware Processes via Satisfiability Modulo Theories, volume
470 of Lecture Notes in Business Information Processing. Springer Nature Switzerland, Cham, 2023.
doi:10.1007/978-3-031-42746-6.
[16] Klaus v. Gleissenthall, Nikolaj Bjørner, and Andrey Rybalchenko. Cardinalities and universal
quantifiers for verifying parameterized systems. In Proceedings of the 37th ACM SIGPLAN Conference
on Programming Language Design and Implementation, PLDI ’16, pages 599–613, New York, NY,
USA, June 2016. Association for Computing Machinery. doi:10.1145/2908080.2908129.
[17] Arie Gurfinkel, Sharon Shoham, and Yuri Meshman. SMT-based verification of parameterized
systems. In Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of
Software Engineering, FSE 2016, pages 338–348, New York, NY, USA, November 2016. Association
for Computing Machinery. URL: https://dl.acm.org/doi/10.1145/2950290.2950330, doi:10.1145/
2950290.2950330.
[18] Matthew Hague, Artur Jeż, and Anthony W. Lin. Parikh’s Theorem Made Symbolic. Proceedings
of the ACM on Programming Languages, 8(POPL):65:1945–65:1977, January 2024. URL: https:
//dl.acm.org/doi/10.1145/3632907, doi:10.1145/3632907.
[19] Matthew Hague and Anthony Widjaja Lin. Synchronisation- and Reversal-Bounded Analysis of
Multithreaded Programs with Counters. In P. Madhusudan and Sanjit A. Seshia, editors, Computer
Aided Verification, Lecture Notes in Computer Science, pages 260–276, Berlin, Heidelberg, 2012.
Springer. doi:10.1007/978-3-642-31424-7_22.
[20] Chih-Duo Hong and Anthony W. Lin. Regular Abstractions for Array Systems. Proceedings of the
ACM on Programming Languages, 8(POPL):638–666, January 2024. URL: https://dl.acm.org/doi/10.
1145/3632864, doi:10.1145/3632864.
[21] James Cornelius King. A program verifier. PhD thesis, Carnegie-Mellon University, Pittsburgh
Pennsylvania USA, September 1969. Section: Technical Reports. URL: https://apps.dtic.mil/sti/
citations/AD0699248.
[22] Felix Klaedtke and Harald Rueß. Parikh Automata and Monadic Second-Order Logics with Linear
Cardinality Constraints. Technical Report 177, Freiburg University, Institute of Computer Science,
2002.
[23] Daniel Kroening and Ofer Strichman. Decision Procedures. Texts in Theoretical Computer Science.
An EATCS Series. Springer Berlin Heidelberg, Berlin, Heidelberg, 2 edition, 2016. doi:10.1007/
978-3-662-50497-0.
[24] Viktor Kunčak, Huu Hai Nguyen, and Martin Rinard. Deciding Boolean Algebra with Pres-
burger Arithmetic. Journal of Automated Reasoning, 36(3):213–239, April 2006. doi:10.1007/
s10817-006-9042-1.
[25] Viktor Kunčak and Martin Rinard. Towards Efficient Satisfiability Checking for Boolean Algebra
with Presburger Arithmetic. In Automated Deduction – CADE-21, Lecture Notes in Computer
90
Science, pages 215–230, Berlin, Heidelberg, 2007. Springer. doi:10.1007/978-3-540-73595-3_
15.
[26] Haojun Ma, Aman Goel, Jean-Baptiste Jeannin, Manos Kapritsos, Baris Kasikci, and Karem A.
Sakallah. I4: incremental inference of inductive invariants for verification of distributed proto-
cols. In Proceedings of the 27th ACM Symposium on Operating Systems Principles, pages 370–384,
Huntsville Ontario Canada, October 2019. ACM. doi:10.1145/3341301.3359651.
[27] Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, and Clark Barrett. Counterexample-
Guided Prophecy for Model Checking Modulo the Theory of Arrays. In Jan Friso Groote
and Kim Guldstrand Larsen, editors, Tools and Algorithms for the Construction and Analysis
of Systems, pages 113–132, Cham, 2021. Springer International Publishing. doi:10.1007/
978-3-030-72016-2_7.
[28] Andrzej Mostowski. On direct products of theories. The Journal of Symbolic Logic, 17(1):1–31,
March 1952. doi:10.2307/2267454.
[29] Rodrigo Raya. Decision Procedures for Power Structures. PhD thesis, EPFL, 2023. doi:10.5075/epfl-
thesis-10546.
[30] Rodrigo Raya and Viktor Kunčak. NP Satisfiability for Arrays as Powers. In 23rd Interna-
tional Conference on Verification, Model Checking, and Abstract Interpretation, Lecture Notes
in Computer Science, pages 301–318, Cham, 2022. Springer International Publishing. doi:
10.1007/978-3-030-94583-1_15.
[31] Rodrigo Raya and Viktor Kunčak. On algebraic array theories. Journal of Logical and Algebraic
Methods in Programming, 136:100906, January 2024. doi:10.1016/j.jlamp.2023.100906.
[32] Rodrigo Raya and Viktor Kunčak. Succinct ordering and aggregation constraints in algebraic
array theories. Journal of Logical and Algebraic Methods in Programming, 140:100978, August 2024.
doi:10.1016/j.jlamp.2024.100978.
[33] Helmut Seidl, Thomas Schwentick, Anca Muscholl, and Peter Habermehl. Counting in Trees
for Free. In Automata, Languages and Programming, Lecture Notes in Computer Science, pages
1136–1149, Berlin, Heidelberg, 2004. Springer. doi:10.1007/978-3-540-27836-8_94.
[34] Larry Stockmeyer and Albert R. Meyer. Cosmological lower bound on the circuit complexity of a
small problem in logic. Journal of the ACM, 49(6):753–784, November 2002. doi:10.1145/602220.
602223.
[35] Wolfgang Thomas. Languages, Automata, and Logic. In Handbook of Formal Languages, pages
389–455. Springer Berlin Heidelberg, Berlin, Heidelberg, 1997. URL: http://link.springer.com/10.
1007/978-3-642-59126-6_7, doi:10.1007/978-3-642-59126-6_7.
[36] Kumar Neeraj Verma, Helmut Seidl, and Thomas Schwentick. On the Complexity of Equational
Horn Clauses. In Automated Deduction – CADE-20, volume 3632, pages 337–352, Berlin, Heidelberg,
2005. Springer Berlin Heidelberg. doi:10.1007/11532231_25.
[37] Thomas Wies, Ruzica Piskac, and Viktor Kunčak. Combining Theories with Shared Set Operations.
In Frontiers of Combining Systems, Lecture Notes in Computer Science, pages 366–382, Berlin,
Heidelberg, 2009. Springer. doi:10.1007/978-3-642-04222-5_23.
91