We develop quantifier elimination procedures for a fragment of higher order logic arising from the formalization of distributed systems (especially of fault-tolerant ones). Such procedures can be used in symbolic manipulations like the computation of Pre/Post images and of projections. We show in particular that our procedures are quite effective in producing counter abstractions that can be model-checked using standard SMT technology.
Building accurate declarative models of distributed systems requires some
complex logic, because integer and boolean variables are not sufficient: since
such systems are parameterized (i.e. they are composed by a finite but unspecified
number of processes), one needs to use arrays [
Quantifier elimination is a rare phenomenon in second order logic, but not
completely unexpected, witness the large literature on correspondence theory in
modal logic. For our intended applications, some quantifier elimination results
were already mentioned in [
Copyright c 2017 by the paper's authors
The paper is organized as follows: in Section 2 we introduce preliminary
notation for higher order logic, in Section 3 we describe our quantifier
elimination results and in Section 4 we show how to apply the results to verification
problems. This paper is focused on algorithmic procedures; the reader can find
the detailed analysis of a benchmark in an Appendix of the extended (online
available) version [
In order to have enough expressive power, we use higher order logic, more
specifically Church’s type theory (see e.g. [
A constrained signature Σ consists of a set of (primitive) sorts and of a set of
(primitive) sorted function symbols,3 together with a class CΣ of Σ-structures,
called the models of Σ.4 Using primitive sorts, types can be built up using
ex1Quantifier elimination required in the benchmarls analyzed in [
2 Some notation we use might look slightly non-standard; it is similar to the notation
of [
3These include 0-ary function symbols, called constants; constants of sort Z will be called (arithmetic) parameters.
4 In the standard model-checking literature, CΣ is a singleton; here we must allow many structures in CΣ, because our model-checking problems are parametric: the sort modeling the set of processes of our system specifications must be interpreted onto ponentiation (= functions type); terms can be built up using variables, function symbols, as well as λ-abstraction and functional application.
Our constrained signatures always include the sort Ω of truth-values; terms
of type Ω are called formulae (we use greek letters α, β, . . . , φ, ψ, . . . for them).
For a type S, the type S → Ω is indicated as ℘(S) and called the power set of S;
if S is constrained to be interpreted as a finite set, Σ might contain a cardinality
operator ] : ℘(S) −→ Z, whose interpretation is assumed to be the intended
one (]s is the number of the elements of s - as such it is always a nonnegative
number). If φ is a formula and S a type, we use {xS | φ} or just {x | φ} for
λxS φ. We assume to have binary equality predicates for each type; universal
and existential quantifiers for formulae can be introduced by standard
abbreviations (see e.g. [
Given a tuple of variables v, a Σ-interpretation of v in a model M ∈ CΣ is a function I mapping each variable onto an element of the correponding type (as interpreted in M). The evaluation of a term t(v) according to I is recursively defined in the standard way and is written as tM,I . A Σ-formula φ(v) is true under M, I iff it evaluates to tt (in this case, we may also say that vM,I satisfies φ); φ is valid iff it is true for all models M ∈ CΣ and all interpretations I of v over M. We write |=Σ φ (or just |= φ) to mean that φ is valid and φ |=Σ ψ (or just φ |= ψ) to mean that φ → ψ is valid; we say that φ and ψ are Σ-equivalent (or just equivalent) iff φ ↔ ψ is valid. 2.1
Flat Cardinality Constraints
Let us fix a constrained signature Σ for the remaining part of the paper. Such Σ
should be adequate for modeling parameterized systems, hence we assume that
Σ consists of:
(i) the integer sort Z, together with some parameters (i.e. free individual
constants) as well as all operations and predicates of linear arithmetic (namely,
0, 1, +, −, =, <, ≡n);
(ii) the enumerated truth value sort Ω, with the constants tt, ff and the Boolean
operations on them;
a finite set whose cardinality is not a priori fixed. Our definition of a ‘constrained
signature’ is analogous to the definition of a ‘theory’ in SMT literature; in fact, in
SMT literature, a ‘theory’ is just a pair given by a signature and a class of structures.
When transferred to a higher order context, such definition coincides with that of a
‘constrained signature’ above (thus our formal preliminary definitions are very similar
to e.g. that of [
In principle, we could consider having finitely many signatures for data instead of just one, but this generalization is only apparent because one can use product sorts and recover component sorts via suitable pairing and projection operations.
If Data is an enumerated sort, we call Σ finitary ; the subsignature Σ0 of Σ obtained by restricting to sorts and operations in (i)-(ii) is called the arithmetic subsignature of Σ.
In the syntactic definitions below, we freely take inspiration from [
Below, besides integer variables (namely variables of sort Z), data variables (namely variables of sort Data) and index variables (namely variables of sort Proc), we use two other kinds of variables, that we call array-ids and matrix-ids. An array-id is a variable of type Proc → Data or of type Proc → Z and a matrixid is a variable of type Proc → (Proc → Data) or of type Proc → (Proc → Z). Array-ids and matrix-ids of codomain sort Z are called arithmetical array-ids or matrix-ids; if Data is enumerated, array-ids and matrix-ids of codomain sort Data are called finitary. If M is a matrix-id and i, y are index variables, we may write Mi(y) or M (i, y) instead of M (i)(y).
Let us now introduce some useful classes of formulae. - Open formulae: these are built up from atomic formulae containing arithmetic parameters and the above mentioned variables, using Boolean connectives only (no binders, i.e. no λ-abstractors and no quantifiers). - 1-Flat formulae: these are formulae of the kind φ(] {x | ψ1} / z1, . . . , ] {x | ψn} / zn), where φ(z1, . . . , zn), ψ1, . . . , ψn are open and x is a variable of type Proc. - Given an index variable i, a formula φ is said to be i-uniform with respect to a matrix-id M (resp. an array-id a) iff i is not used as a bounded variable in φ and the only terms occurring in φ containing an occurrence of M (resp. of a) are of the kind Mi(y) (resp. a(i)) for a variable y.
Notice that, some quantified formulae can be rewritten as 1-flat formulae: for
instance ∀i (a(i) = c → b(i) = d) is the same as ]{i | a(i) = c → b(i) = d} = N,5
and similarly ∃i (a(i) = c) can be re-written as ]{i | a(i) = c} > 0.
Remark 1. 1-Flat formulae of this paper are slightly different from the flat
formulae of [
In this technical section we state and prove the quantifier elimination results we need. Let us fix a constrained signature Σ like in Subsection 2.1. We first investigate in a closer way our open formulae. Notice first that if an open formula is pure (i.e. it does not contain array-ids or matrix-ids), then it is a Boolean combination of arithmetic, index or data atoms, where: - arithmetic atoms are built up from variables of sort Z, parameters (i.e free constants of sort Z), by using =, <, ≡n as predicates and +, −, 0, 1 as function symbols; - index atoms are of the kind i = j, where i, j are variables of sort Proc (we do not consider further operations and predicates for this sort - apart from equality - in this paper); - data atoms are built up from variables of sort Data by applying some specific set of predicates and operations (predicates include equality, all arguments of such predicates and operations are of type Data).
By assumption (see Subsection 2.1), quantifier elimination holds for first-order Data-formulae, but this result extends very easily to all pure first-order formulae. We state this formally as a Lemma: Lemma 1. Any pure first-order formula is equivalent to an open pure first-order formula.
Proof. Using prenex formula transformations, it is sufficient to show how to
eliminate a quantifier ∃x α, where α is open and pure. Actually, using disjunctive
normal forms, we can assume that α is a conjunction of literals. Pushing the
existential quantifier inside, we can assume that such literals are all arithmetic,
all index or all data literals, depending on the sort of x. The case of arithmetic
literals is covered by Presburger quantifier elimination [
In case array-ids and matrix-ids do not occur, 1-flat formulae can also be trivialized:6 Lemma 2. A 1-flat formula without array-ids and matrix-ids is equivalent to a pure formula.
Proof. Let us eliminate subterms t of the kind ]{x | α} (with pure α) inside a pure formula φ. We can first remove from α arithmetic and data atoms, as well as index atoms not containing x, by the following equivalence (let A be the atom to be removed):
φ ↔ ([A ∧ φ(>/A)] ∨ [¬A ∧ φ(⊥/A)]) .
By Venn regions decomposition, we can assume that α is a conjunction of literals. In addition, if t is of the kind ]{x | x = i ∧ α}, we can remove it using the equivalence:
φ ↔ ([α(i/x) ∧ φ(1/t)] ∨ [¬α(i/x) ∧ φ(0/t)]) .
Thus we are left only with the case in which t is ]{x | Vsn=1 x 6= is}; we can also assume that φ entails Vs6=s0 is 6= is0 (otherwise we can force this by making φ a disjunction of case distinctions). Then we can remove t using φ ↔ (N ≥ n¯ ∧ φ(N − n¯/t)) ∨ (N < n¯ ∧ φ(0/t)) . a (1) yn. By introducing a disjunction of cases (and by distributing the existential quantifier over such disjunction and removing redundant variables), we reduce to a disjunction of formulae of the kind Once all t are removed (one by one), the statement is proved.
It is now convenient to introduce a notation for open (not necessarily pure) formulae (from now on we shall reserve the letters α, β, . . . to first-order pure formulae, to evidentiate them). Considering that there are no operation symbols of sort Proc, the only new terms that might arise in open non pure formulae (wrt pure formulae) are of the kind a(i) or Mi(j), where a is an array-id, M is a matrix-id and i, j are variables of sort Proc. Thus we may write an open formula φ as the formula obtained by replacing in a pure formula some arithmetic variables with terms of the kind a(i) or Mi(j). If our open φ does not contain matrix-ids, we can write it as
α(z, k, a(k)/e, d) or simply as α(z, k, a(k), d)
6 If the sort Proc is identified with a definable finite subset of Z, the result still holds
but is much less trivial: to get it, one must apply results from Presburger arithmetic
with counting quantifiers [
a1(k1), . . . , a1(km), . . . , an(k1), . . . , an(km) so that the matching tuple of data variables e must be indexed as e11, . . . , enm.
A 1-flat formula without matrix-ids is then written as α(z, k, a(k), d, ]{x | β1(z, x, k, a(x), a(k), d)}, . . . , ]{x | βs(z, x, k, a(x), a(k), d)}) or (with some abuse of notation) shortly as α(z, k, a(k), d, ]{x | β(z, x, k, a(x), a(k), d)}) (2) where β is a tuple of formulae (we use the convention that ]{x | β} stands for the tuple of terms ]{x | β1}, . . . , ]{x | βs}). Displaying 1-flat formulae with matrix-ids requires an even more complex notation, that we won’t use though. These notations are apparently cumbersome but have the merit of displaying the essential information on how our formulae are built up from pure formulae.
We now state a first quantifier elimination result (this is Theorem 4 from [
The following Corollary follows from Theorem 1 and Lemmas 2,1: Corollary 1. Suppose that φ is a 1-flat formula containing the array ids a (and not containing matrix-ids); then the formula ∃a φ is equivalent to an open pure formula.
Notice that the above result (as it happens with all our quantifier elimination
results) immediately implies that 1-flat formulae not containing matrix-ids are
decidable for satisfiability. If the sort Data is enumerated and all array-ids are
finitary, we can improve Corollary 1 above by including an extra quantified
variable (this is useful for benchmarks, see the Appendix of [
Proof. Let Data be enumerated as {a0, . . . , ak}; let z be the arithmetic variables occurring freely in (3) and let k = k1, . . . , kn be the index variables occurring freely in (3) (thus i is not among the k and the y are not among the z). We can assume that the y are arithmetic variables because, since Data is enumerated, existential data variables can be elimitated via disjunctions. For simplicity, we assume that (3) contains only one array-id, let it be a.7
Before working on the formula (3), it is better to make some preprocessing steps. Our final outcome will be that of producing a disjunction of existentially quantified pure formulae logically equivalent to (3): in fact, we introduce extra existentially quantified variables to be eliminated in the very end using Lemma 1. We need also to introduce extra information to complete (3): this extra information is achieved by rewriting (3) as a disjunction (each disjunct formalizes a suitable guess) and by operating on each disjunct separately.
Concretely, we shall freely assume that ∀i ∃y φ in (3) is of the kind Diff(k) ∧ ^(a(ki) = ali ) ∧ ^(uj = ]{x | a(x) = aj }) ∧ i j ∧ ∀i ∃y φ0(z, y, i, k, a(i), ]{x | β(z, y, x, i, k, a(x), a(i))}) (4) where • the formula Diff(k) says that the k are pairwise distinct (i.e. it is Vi6=j ki 6= kj ): this can be assumed without loss of generality, because one can guess a partition (introducing a disjunction over all partitions) and make the appropriate replacements so as to keep only one representative for each equivalence class of variables; • since Data is enumerated we can guess (via a disjunction) for each ki the ali which is the value of a(ki) (then, all occurrences of the term in the remaining part of the formula can be replaced by this ali ); • the uj are fresh arithmetic variables indicating the cardinality of the set of indices whose a-value is aj (these uj are the extra existentially quantified variables to be eliminated in the very end by Lemma 1); • β are open formulae as displayed and φ0 is a 1-flat formula as displayed (notice that the terms a(ki) do not occur anymore here, because we can assume that they have been replaced by the corresponding ali ).
We now operate further transformations on the subformula ∀i ∃y φ0: we want to show that this formula is equivalent to a 1-flat formula (hence without the quantifier ∀i), so that the claim of the Theorem follows from an application of Corollary 1 and Lemma 1 - by these results in fact all quantified variables in (3) can be eliminated in favor of a pure open formula in which only the k, z occur. When manipulating ∀i ∃y φ0 below, we assume all the information we have from (4), namely that the k are all distinct and that the values of the a(ki) are known.
7This is without loss of generality: since Data is enumerated and the a are finitary, one may take a product of Data and replace the tuple a with a single array with values in such a product.
As a first step, we can distinguish the case in which i is equal to some of the k from the case in which it is different from all of them; in the latter case, we can also guess the value of a(i). This observation shows that ∀i φ0 is equal to the conjunction of an open formula (expressing what happens if i is equal to any of the k) with the conjunctions (varying aj in our enumerated data) ∀i. Diff(i, k) ∧ a(i) = aj → ∃y φ00(z, y, i, k, ]{x | β0(z, y, x, i, k, a(x))}) (5) where the φ00, β0 are obtained from the φ0, β by replacing a(i) with aj. Again, it will be sufficient to show that (5) is equivalent to an open formula.
First observe that φ00 is obtained from a pure formula by replacing arithmetic variables with the terms ]{x | β0(z, y, x, i, k, a(x))}; since equality is the only predicate of sort Proc (and there are no function symbols of sort Proc), the only atoms of sort Proc that might occur in a pure formula are of the kind i = ks, ks = ks0 for some s 6= s0, but these can all be replaced by ⊥ because we have Diff(i, k) in the antecedent of the implication of (5). As a consequence φ00 can be displayed as φ00(z, y, ]{x | β0(z, x, i, k, a(x))}).
A similar observation applies also to the β0, however here we must take into consideration also atoms of the kind x = i, x = ks. Thus, the β0 are built up using Boolean conectives from atoms of the kind x = i, x = ks, from arithmetic atoms A(z, y) and from Data-atoms that might contain the term a(x). We can disregard arithmetic atoms, because for each such atom A(z, y) we may rewrite φ00 as [A(z, y)∧φ00(z, y, ]{x | β0(>/A)})] ∨ [¬A(z, y)∧φ00(z, y, ]{x | β0(⊥/A)})] . (6) Thus the β0 can be displayed as β0(x, i, k, a(x)).
When x = i or x = ks (for some s) the β0 can be simplified to > or ⊥ because we know the values of a(i), a(ks) (and as a consequence the numbers ]{x | x = i ∧ β0}, ]{x | x = ks ∧ β0} are 0/1-tuples). In conclusion we have that, for some tuple of numbers m8 that can be computed, we have that (5) is equivalent to ∀i. Diff(i, k) ∧ a(i) = aj → ∃y φ00(z, y, m¯ + ]{x | Diff(x, i, k) ∧ β00(a(x))}) (7) where β00 is obtained from β0 by replacing the atoms x = i, x = ks with ⊥. Fix now some βs00 from the tuple β00; for every enumerated data ak, each of the formulae βs00(ak) simplify to either > or ⊥ and, since we know that uk = ]{x | a(x) = ak} from (4), we can deduce that ]{x | Diff(x, i, k) ∧ a(x) = ak ∧ βs00(ak)} is equal to either 0 (in case βs00(ak) simplifies to ⊥) or to uk − nk, where nk is the number of the k, i for which we know that a(k), a(i) is equal to ak. As a consequence ]{x | Diff(x, i, k) ∧ β00(a(x))} is equal to Pk(uk − nk) (where the sum extends to all k such that βs00(ak) simplifies to >).
8This tuple depends on j, i.e. on the aj used in the antecedent of (5) (we do not indicate this dependency for simplicity).
All this can be summarized by saying that we can rewrite (7) as ∀i. Diff(i, k) ∧ a(i) = aj → ∃y θj (y, z, u) where the formulae θj are pure (the tuple u is the tuple of the uj from (4)). By Presburger quantifier elimination, we can drop the ∃y, thus getting ∀i. Diff(i, k) ∧ a(i) = aj → θj0 (z, u) Since now θj0 does not contain occurrences of i, we can rewrite this as (8) (9) (10) (11) (12) (13) and finally as
∃i (Diff(i, k) ∧ a(i) = aj) → θj0 (z, u) ]{x | Diff(x, k) ∧ a(x) = aj} > 0 → θj0 (z, u) This is a 1-flat formula. To sum up, our original formula (3) is equivalent to a formula of the kind ∃a ∃u ϑ, where ϑ is 1-flat. Then (after swapping the quantifiers ∃a ∃u) we can first use Theorem 1 to remove ∃a and then Lemma 1 to produce an equivalent pure open formula (involving just the arithmetic variables z and the index variables k). a
In case we have uniformity, we can further extend the above result to cover
formulae in which arithmetic array-ids and matrix-ids occur (see again the
Appendix of [
∃a ∃M ∀i ∃y φ (where the y are arithmetic and data variables) is equivalent to an open pure formula.
Proof. The first step is to remove ∃M for each M ∈ M, using uniformity. In fact, by uniformity, M occurs in φ only inside terms of the kind Mi(y) (for some index variable y); thus, using choice axiom (in the form of an anti-skolemization), we can rewrite (12) as
∃a ∀i ∃b ∃y φ(· · · b/Mi · · · ) and then we can swap the existential quantifiers ∃b∃y and apply Theorem 1, thus obtaining a formula of the kind ∃a ∀i ∃y ∃e ψ where the e are further arithmetic or data variables, ψ is 1-flat and contains only the array-id a. Let us now split the a as a0, a00, where the a00 are i-uniform and the a0 are finitary. We can apply the same anti-skolemization argument to the a00 and rewrite ∃a0 a00 ∀i ∃y ∃e ψ as ∃a0 ∀i ∃z ∃y ∃e ψ(z/a00(i)), where the z are fresh arithmetic variables replacing the terms a00(i) in ψ. Now Theorem 2 can be used to eliminate the a0.
We now go to verification applications. We summarize the essential machinery
for making quantifier elimination to apply (for more information, see [
S = (Σ, v, Φ, ι, τ ) where (i) Σ is a constrained signature, (ii) v is a tuple of variables, (iii) Φ, ι are v-formulae, (iv) τ is a (v, v0)-formula (here the v0 are renamed copies of the v) such that ι(v) |=Σ Φ(v),
Φ(v) ∧ τ (v, v0) |=Σ Φ(v0) .
In the above definition, the v are meant to be the variables specifying the system status, ι is meant to describe initial states and τ is meant to describe the transition relation. The v-formula Φ, as it is evident from (15), describes an invariant of the system (known to the user). Invariants are quite useful - and often essential - in concrete verification tasks, that’s why we included them in Definition 1.
A safety problem for a system specification S like above is a v-formula υ(v); the system is safe with respect to υ iff there is no n ≥ 0 such that the formula ι(v0) ∧ τ (v0, v1) ∧ · · · ∧ τ (vn−1, vn) ∧ υ(vn) is satisfiable.
Directly attacking safety problems for a system like (14) might be a too difficult task, that’s why it is useful to replace it with a simpler system: in our applications, we shall try to replace S by some S0 whose variables are all integer variables. To this aim, we ‘project’ S onto a subsystem S0, i.e. onto a system comprising only some of the variables of S. In order to give a precise definition of what we have in mind, we must first consider subsignatures: here a subsignature Σ0 of Σ is a signature obtained from Σ by dropping some symbols of Σ and taking as Σ0-models the class CΣ0 of the restrictions M|Σ0 to the Σ0-symbols of the structures M ∈ CΣ . The following proposition is immediate: Proposition 1. Let S0 = (Σ0, v0, Φ0, ι0, τ0) and S = (Σ, v, Φ, ι, τ ) be system specifications, with respective safety problems υ(v0) and υ(v). Suppose that Σ0 is a subsignature of Σ and let v = v0, v1; suppose also that the following hold: (i) |=Σ Φ0(v0) ↔ ∃v1Φ(v0, v1); (ii) |=Σ ι0(v0) ↔ ∃v1ι(v0, v1); (iii) |=Σ τ0(v0, v00) ↔ ∃v1 ∃v10(Φ(v0, v1) ∧ τ (v0, v1, v00, v10)); (iv) |=Σ υ0(v0) ↔ ∃v1υ(v0, v1).
Then if S0 is safe with respect to υ0, so it is S with respect to υ.9
9Notice that only the right-to-left implications of (i)-(iv) are needed for the
proposition to hold; however, if we have also the left-to-right implications, the system
specification S0 is better, in a sense that can be specified formally [
The system specification S0 satisfying the above condition (i)-(iii) with respect to S is called the (Σ0, v0)-projection of S; if Σ0 is the arithmetical subsignature of Σ and v0 are all the arithmetic variables of S, S0 is called the arithmetic projection of S.
Theorem 4. If Φ, ι, τ do not contain matrix-ids and are of the kind ∃k1 · · · ∃knφ for a 1-flat formula φ and for index variables k1, . . . , kn, then S = (Σ, v, Φ, ι, τ ) has an (effectively computable) arithmetic projection.
Proof. Let v be z, a, where the z are arithmetic variables and the a are array variables; we also abbreviate k1, . . . , kn as k. We need to show that a formula of the kind ∃a ∃k α(z, k, a(k), ]{x | β(z, x, k, a(x), a(k))}) (16) is equivalent to a pure arithmetic formula.10 But this is indeed the case: just swap the existential quantifiers and apply Corollary 1 and Lemma 1. The result follows because there are no ground index atoms and all ground data atoms are equivalent to > or to ⊥, according to our assumptions from Subsection 2.1.
Next result concerns specifications using matrix-ids in a finitary signature. Theorem 5. Let the sort Data be enumerated and let Φ, ι, τ be disjunctions of formulae of the kind ∃k ∀i ∃y φ (17) where φ is 1-flat, k are index variables, y are arithmetic and data variables and i is an index variable such that all matrix variables and all non-finitary array variables from v are i-uniform in φ; then S = (Σ, v, Φ, ι, τ ) has an (effectively computable) arithmetic projection.
Proof. Similar to the proof of Theorem 4, using Theorem 3 instead of Corollary 1.
To sum up, given a system specification S = (Σ, v, Φ, ι, τ ) and a safety
problem υ(v), if the formulae Φ, ι, τ, υ satisfy suitable syntactic restrictions so
that our quantifier elimination results apply, we can compute the arithmetic
projection S0 of S and try to show that S0 is safe with respect to υ0(v0) (the
latter is the formula obtained in its turn by eliminating the higher order variables
from υ(v)).11 Thus a model ckecking problem formulated in higher order logic
can be solved via a model checking problem for counter systems (i.e. for system
specifications in a purely arithmetic signature). The literature on distributed
systems confirms that this is a viable approach: since long time it has been
observed that counter systems [
11A more sophisticated strategy would preprocess the system specification S by
artificially adding to it some extra integer variables counting certain definable sets (see
the Appendix of [
It should be noticed that safety problems for counter systems are themselves
undecidable, however the sophisticated machinery (predicate abstraction [
Arithmetic projections obtained by our methods are far from trivial: the
reader may realize this by looking at the detailed analysis of a classical
benchmark in the Appendix of [
We have investigated quantifier elimination results for fragments of higher
order logic suggested by verification applications in the distributed algorithms
area. We have shown how to apply such results in order to automatically produce
arithmetic projections that can be effectively handled by state-of-the-art
SMTbased model checkers. Similar applications can be devised for forward/backward
model checking, along the lines sketched in [
A potentially weak point to be taken care is the complexity of the algorithms we employ: in fact, the procedure for quantifier elimination used in the proof of Theorems 1, 2, 3 produces super-exponential blow-ups of the size of the formulae it is applied to. Notice however that, when building a counters simulation of a concrete algorithm, such a heavy procedure is applied to each instruction (or to each block of instructions) separately, i.e. not to the whole code. Moreover, it is not difficult to realize (going through the details for our benchmarks) that it is hardly the case that the quantifier elimination procedure is applied in its full generality: in fact, it is always applied to easier fragments, where complexity reduces (recall for instance the content of footnote 1). The same observation applies also to the instances of the Presburger quantifier elimination procedure that are invoked in our manipulations: usually, they are confined to difference logic formulae or to formulae where quantifiers can be eliminated by simple instantiations. The identification of such shortcuts and the study of the related complexities is important for future work and preliminary to any substantial implementation effort.
Another delicate point is related to the syntactic limitations we require on
the formulae describing system specifications (see the statements of Theorems 4
and 5): such syntactic limitations are needed to ensure higher order quantifier
elimination. Although it seems that a significant amount of benchmarks are
captured despite such limitations, it is essential to develop techniques
applicable in more general cases. To this aim, we observe that just overapproximations
are needed to build simulations and that, even if the best simulation may not
exist, still practically useful simulations might be produced. In fact, quantifier
elimination is just an extreme solution to symbol elimination problems. Symbol
elimination and interpolation are a well-known technique to build invariants,
abstractions and overapproximations, and for this reason their investigation has
deserved considerable attention in the automated reasoning literature [