# Computing Difference Abstractions of Linear Equation Systems

Emilie Allart, Joachim Niehren, Cristian Versari

<figure><img src="image_1.png" /></figure>

## To cite this version:

Emilie Allart, Joachim Niehren, Cristian Versari. Computing Difference Abstractions of Linear Equation Systems. Theoretical Computer Science, 2021, 10.1016/j.tcs.2021.06.030. hal-03156136v3

HAL Id: hal-03156136

https://hal.science/hal-03156136v3

Submitted on 17 Jun 2021

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.
# Computing Difference Abstractions of Linear Equation Systems

Emilie Allart<sup>a,c</sup>, Joachim Niehren<sup>a,b</sup>, Cristian Versari<sup>a,c</sup>

<sup>a</sup>BioComputing CRISTAL - Centre de Recherche en Informatique, Signal et Automatique de Lille (CRISTAL) - UMR 9189

<sup>b</sup>Linking Dynamic Data CRISTAL - UMR 9189, Inria Lille - Nord Europe

<sup>c</sup>Université de Lille

## Abstract

Abstract interpretation was proposed for predicting changes of reaction networks with partial kinetic information in systems biology. This requires to compute the set of difference abstractions of a system of linear equations under nonlinear constraints. We present the first practical algorithm that can compute the difference abstractions of linear equation systems exactly. We also present a new heuristics based on minimal support consequences for overapproximating the set of difference abstractions. Our algorithms rely on elementary modes, first-order definitions, and finite domain constraint programming. We implemented our algorithms and applied them to change prediction in systems biology. It turns out experimentally that the new heuristics is often exact in practice, while outperforming the exact algorithm.

This journal article extends on a paper published at the 17th International Conference on Computational Methods in Systems Biology (CMSB'2019) [1].

**Keywords:** abstract interpretation, constraint programming, linear programming, elementary modes, first-order definitions, gene knockout prediction, reaction networks, systems biology, synthetic biology, metabolic networks, boolean abstraction.

## 1. Introduction

Motivated by analysis questions for steady states [2, 3] of chemical reaction networks [4, 5, 6, 7] we study the problem how to compute the set of difference abstractions of the solutions of a given linear equations system. The difference abstractions may be subject to constraints, which in the motivating application serve for expressing partial kinetic information on inhibitors and accelerators of the reactions of the network [8].

**Problem.** We consider systems of homogeneous linear equations with variables for positive real numbers in $\mathbb{R}_+$ including 0, possibly existentially quantified, such as for instance $E(X, Y)$ in (1):

$$ \exists U. \exists V. \left( \begin{array}{cccc} -1 & 0 & 1 & -1 \\ 0 & -1 & 1 & -1 \end{array} \right) \left( \begin{array}{c} X \\ Y \\ U \\ V \end{array} \right) \doteq 0 \qquad (1) $$

Given that the matrix is triangular and the variables $U, V$ are existentially quantified, we can read off the set of solutions of $E(X, Y)$ easily. A variable assignment is a solution over $\mathbb{R}_+$ if and

<footnote>Email address: emilie.allart@univ-lille.fr (Emilie Allart)</footnote>
<figure><img src="image_2.png" /><figcaption>Figure 1: The difference abstraction to $\Delta_3$.</figcaption></figure>

<figure><img src="image_3.png" /><figcaption>Figure 2: The difference abstraction to $\Delta_6$.</figcaption></figure>

only if it maps $X$ and $Y$ to the same number:

$$sol_{\mathbb{R}_+}(E(X, Y)) = \{\alpha : \{X, Y\} \to \mathbb{R}_+ | \alpha(X) = \alpha(Y)\}$$

An instance of the question studied in this article is, what happens to the value of $Y$ if we increase the value of $X$, while jumping from one solution of $E(X, Y)$ to another? Clearly, the value of $Y$ must be increased as well, since $X$ and $Y$ must have the same value in all solutions. More generally, we want to compute all possible relationships of any two solutions of $E(X, Y)$ over the positive reals.

For making this problem more precise, we consider a partition of the space $\mathbb{R}_+^2$ of concrete differences into the set of abstract differences $\Delta_3 = \{\Delta, \nabla; \approx\}$, which is illustrated in Figure 1. The abstract difference $\Delta$ stands for an increase, $\approx$ for a no-change, and $\nabla$ for a decrease. Given a finite set of variables $V$, we define the difference abstraction of two variable assignments to the positive reals $\alpha, \alpha' : V \to \mathbb{R}_+$ as the assignment $\beta : V \to \Delta_3$ such that for all $x \in V$:

$$\beta(x) = \begin{cases} \Delta & \text{if } \alpha(x) < \alpha'(x) \\ \approx & \text{if } \alpha(x) = \alpha'(x) \\ \nabla & \text{if } \alpha(x) > \alpha'(x) \end{cases}$$

Our objective then is to compute for any given linear equation system the set of difference abstractions of any two positive real solutions. In our example system $E(X, Y)$, the expected answer is $\{\beta : \{X, Y\} \to \Delta_3 | \beta(X) = \beta(Y)\}$. In general, the computation can be done by a generate and test algorithm based on Lemma 1 below, which reduces the test to a linear program. This algorithm, however, is too slow in practice, to be applicable to change prediction tasks in systems biology. This is why the previous approach by John et al. [8, 9, 10] computed an overapproximation only, by interpreting the equation system abstractly over the canonical relational structure with finite domain $\Delta_3$ and signature $\{+, -, 0, 1\}$, and solving it by finite domain constraint programming [11, 12]. The question we study in the present article is whether there exists a better algorithm useful for change prediction in systems biology, that can compute the difference abstraction exactly while avoiding any overapproximation.

Furthermore, two variants of the above problem must be supported for practical application to systems biology. First, we need to be able to treat a refined difference abstraction with 6 values $\Delta_6 = \{\uparrow, \downarrow, \sim, \uparrow, \downarrow, \approx\}$ illustrated in Figure 2. Note that $\Delta = \uparrow \lor \uparrow, \nabla = \downarrow \lor \downarrow$ and $\approx = \sim \lor \approx$, depending on whether the change started or ended with 0 or not. Second, for capturing partial kinetic information up to similarity, we must be able to impose additional constraints on the
abstract solutions we are interested in. These will be given by some first-order formulas that are to be interpreted over the abstract domain.

*Contributions.* First, we generalize the difference abstractions $h_{\Delta_3} : \mathbb{R}_+^2 \to \Delta_3$ and $h_{\Delta_6} : \mathbb{R}_+^2 \to \Delta_6$ algebraically to $\Sigma$-abstractions, which are homomorphisms between the $\Sigma$-structures. The set of concrete differences $\mathbb{R}_+^2$ becomes a $\Sigma$-algebra with signature $\Sigma = \{+, -, 0; 1\}$ equipped with pointwise addition and multiplication. The sets of abstract differences $\Delta_3$ and $\Delta_6$ become $\Sigma$-structures that are naturally induced by the finite partitioning of $\mathbb{R}_+^2$ in Figures 1 and 2. Second, we can show for any two $\Sigma$-structure $S$ and $\Delta$ (such as $\mathbb{R}_+^2$ and $\Delta_3$ above) that John's overapproximation theorem [8, 10] can be lifted to general $\Sigma$-abstractions $h : S \to \Delta$. It states that for any positive first-order $\Sigma$-formula $\phi$, its $h$-abstraction can be computed by abstract interpretation of $\Delta$:

$$h \circ sol^S(\phi) \subseteq sol^\Delta(\phi)$$

This is since any $h$-abstraction of an $S$-solution of $\phi$ is also a $\Delta$-solution of $\phi$. If furthermore $\Delta$ is finite, then we can compute $sol^\Delta(\phi)$ by finite domain constraint programming. This approach was shown to be applicable in the motivating application from systems biology [9].

The objective of this article, however, is to compute exactly the set of difference abstractions for both cases $h_{\Delta_3} \circ sol_{\mathbb{R}_+^2}(\phi)$ and respectively $h_{\Delta_6} \circ sol_{\mathbb{R}_+^2}(\phi)$, where $\phi$ is a system of linear equations possibly with existential quantifiers (which clearly can be seen as $\Sigma$-formulas). The motivation is to overcome the main problematics of John's overapproximation, which can already be illustrated at the example of $E(X, Y)$. When interpreted over the $\Sigma$-structure $\Delta_3$, the system $E(X, Y)$ admits the abstract solution $\beta = [X/\Delta, Y/\nabla]$, since $\Delta + \Delta_3 \nabla$ may be related to any value in $\Delta_3$ nondeterministically. However, $\beta$ is not the difference abstraction of any concrete solution, given that $E(X, Y)$ implies $X = Y$. In other words, $X = Y$ is a logical consequence of $E(X, Y)$ over $\mathbb{R}_+$, but not over $\Delta_3$, so precisely the information that we seek in our example is lost by abstract interpretation relying on John's overapproximation.

In order to avoid any overapproximation, one may want to enrich the linear equation system before solving it over the finite abstract structure, by adding all its logical consequences over $\mathbb{R}_+$, which correspond to all the linear combinations of the rows of the matrix (its row space). However this leads to an infinite number of consequences, so one would be forced to consider them modulo equivalence up to abstract interpretation. Since the abstract domains considered are finite, the number of equivalence classes would be finite too. However, finding a representative for each equivalence class corresponds to solving a linear programming problem, and the number of consequences to be added is exponential in the dimension of the matrix. Therefore, even if this approach leads to a finite representation of the set of logical consequences of the linear equation system, it is still unfeasible in practice for complexity reasons. A less inefficient approach but still infeasible in practice can be obtained by the *generate and test* algorithm mentioned earlier. The idea is to test the satisfiability of each abstract solution candidate individually by linear programming based on Lemma 1 below.

As a third contribution we propose a new heuristics based on minimal support consequences to improve John's overapproximation algorithm. Given a system of linear equations, the idea is to add all linear consequences that have a minimal number of variables and normalized coefficients, before computing the abstract solutions. We show how to compute this finite set of linear consequences based on elementary modes [13, 14] and orthogonal complements.

As a fourth and most important contribution, we present algorithms for computing the difference abstractions for linear equation system exactly. They can deal with $\Delta_3$ and $\Delta_6$ and with the addition of constraints on the abstract differences. The exact abstraction problems are reduced to finite domain constraint problems, that can be solved in practice with existing finite domain constraint solvers. The reductions are based on properties of first-order definitions that permit to reason with concrete differences in a first-order logic with pairs. Furthermore, we rely
on a recent algorithm [15] for the exact rewriting of linear equation systems with respect to the boolean abstraction $h_B : \mathbb{R}_+ \to \mathbb{B}$, which maps 0 to 0 and all other positive real numbers to 1. The linear equation system $\phi$ obtained by exact rewriting for the boolean abstraction satisfies $h_B \circ \mathrm{sol}^{\mathbb{R}_+}(\phi) = \mathrm{sol}^{\mathbb{B}}(\phi)$ and is again based on the computation of elementary modes.

Fifth, we implemented the minimal support heuristics and our exact abstraction algorithm for $\Delta_6$, and applied them to the prediction of leucine overproduction, a benchmark task for change prediction in systems biology [8, 9]. It turns out that the minimal support heuristics indeed computes the difference abstraction to $\Delta_6$ exactly for this benchmark, while it does not do so in general. The main advantage of this heuristic is that it outperforms the exact algorithm dramatically in computation time: only 5 minutes are needed for the knockout prediction rather than 5 hours with the always exact algorithm.

This article extends on a conference paper at CMSB'2019 [1]. This was an extended abstract without any proofs, where most of the technical difficulties could not be exposed. In particular, we could not explain how to decompose the difference abstractions for $\Delta_3$ and $\Delta_6$ into the boolean abstraction based on functions defined in first-order logic. Also we could not describe in any sufficient detail how the addition of kinetic constraint can be dealt with. So the additional material mainly consists in detailed sections on how to compute difference abstractions to $\Delta_3$ and $\Delta_6$ exactly, also in the presence of kinetic constraints. The case of $\Delta_6$ is considerably more difficult to be treated, since it requires more advanced kinds of first-order definitions. Furthermore, the presentation of the minimal support heuristics has been extended and equipped with a correctness argument.

The present article contains full proofs, of which some simpler inductions are delegated to the appendix.

*Outline.* In Sections 2 and 3 we discuss further related work and illustrate the application to change prediction in systems biology. After some preliminaries (Section 4), we recall in Section 5 the notion of $\Sigma$-abstractions and in Section 6 the $\Sigma$-structures of abstract differences $\Delta_3$ and $\Delta_6$. The standard first-order logic is recalled in Section 7 jointly with a less standard variant that we call the tuple logic. Difference abstractions and John's overapproximation theorem are recalled in Section 8. Section 9 recalls a previous result on exact boolean abstraction.

In Section 10 we use the existing result on exact boolean abstraction to provide a new characterization of difference abstraction to $\Delta_3$ and $\Delta_6$ for linear equation systems. This characterization yields an algorithm for computing difference abstractions of linear equation systems, that we extended in Section 11 so that it can take additional difference constraints into account. An overapproximation heuristics with minimal support is then presented in Section 12. And finally in Section 13, an implementation and experimentation section compares these two approaches.

## 2. Related Work

We first discuss the generate and test algorithm for solving our problem based on existing results for linear equations systems and linear programming.

Given an abstract difference $d \in \Delta_3$ and two variables $y, z$ we define a formula saying that the abstraction of the concrete difference denoted by $(y, z)$ is equal to $d$:

$$ abs_d(y, z) = \begin{cases} y < z & \text{if } d = \Delta \\ x \doteq y & \text{if } d = \approx \\ z < y & \text{if } d = \nabla \end{cases} $$

Let $\mathbf{x} = x_1...x_m$, $\mathbf{y} = y_1...y_m$ and $\mathbf{z} = z_1...z_m$ be sequences of distinct variables. Given an assignment of the variable in $\mathbf{x}$ to abstract differences $\beta : \{\mathbf{x}\} \to \Delta_3$ we define a formula
$abs_β(y, z)$ as follows:

$$abs_β(y, z) = \bigwedge_{i=1}^{m} abs_{β(x_i)}(y_i, z_i)$$

The assignment $β$ then is the difference abstraction of some pair of solutions in $sol_+^R(E(\mathbf{x}))$ if and only if the following formula is satisfiable over $R_+$.

$$E(y) \wedge E(z) \wedge abs_β(y, z)$$

**Lemma 1.** The satisfiability over $R_+$ of systems of homogeneous linear equation and strict linear inequations without constants can be decided in polynomial time.

**Proof** A strict linear inequation without constants $x < y$ is equivalent over $R_+$ to $\exists z. x + z = y \wedge z \neq 0$. Therefore, it is sufficient to consider the satisfiability over $R_+$ of systems of homogeneous linear equations $E(\mathbf{x})$ and nonzero equation $\mathbf{x}' \neq 0$. The solution set $sol_+^R(E(\mathbf{x}))$ is a cone (while for more general linear programs it could be more general polytopes). The elements of a cone can be multiplied by positive reals without leaving the cone. Therefore, the nonzero equation $\mathbf{x}' \neq 0$ can be rewritten to $\mathbf{x}' \geq 1$ without affecting the satisfiability of the formula. This rewriting eliminates the strict inequations without constants at the cost of introducing nonstrict inequations with constants. The result is a linear program. Instead of interpretation over $R_+$ we can add inequations $\mathbf{x} \geq 0 \wedge \mathbf{x}' \geq 0$ and change to an interpretation over $\mathbb{R}$. It well known that the satisfiability of linear programs over $\mathbb{R}$ can be tested in polynomial time [16]. □

So by a naive enumerate and test algorithm, we can compute in the case of $\Delta_3$ the set of all difference abstractions for $sol_+^\Delta(E(\mathbf{x}))$ in time $O(3^m poly(|E(\mathbf{x})|))$. For $\Delta_6$, the analogous argument yields $O(6^m poly(|E(\mathbf{x})|))$.

Flux balance analysis [2, 3] can be used to predict the effect of influx changes of metabolic networks at steady state. Such predictions can be based on reasoning with linear equation systems that describe the rates of the reactions in a steady state of the metabolic network, by using Gaussian elimination, elementary flux modes (EFMs) [17], or optimisation methods [18, 19]. Most importantly, precise quantitative kinetic information is not required in contrast to classical mathematical analysis methods for reaction networks. In fact, even when the kinetic functions associated to chemical reactions are known, the values of the rate constants are most often missing, since it is difficult to measure them experimentally in the precise state of the regulation of the metabolic network at the time point of interest.

Recently, abstract interpretation [20, 21, 22] has been exploited to design novel algorithms [8, 10] that can use partial kinetic information beneficially for predicting changes of metabolic networks. They can in particular exploit the knowledge about the enzymes and inhibitors. Similarly to flux balance analysis, the linear equations describing steady states are used, but in addition to them, kinetic constraints are inferred from the partial kinetic information of inhibitors and enzymes.

### 3. Application to Change Prediction in Systems Biology

Reaction networks [4, 5, 6, 7] are widely used in systems biology to model the dynamics of biological systems, so that their behaviour can be simulated or analysed. We are interested in change predictions for reaction networks with partial kinetic information [8, 9, 10]. The steady state semantics of such networks yields a system of linear equations, and a set of nonlinear constraints about the differences abstraction in $\Delta_6$ of solutions of the linear system.
<figure><img src="image_4.png" /><figcaption>Figure 3: An example of reaction network with partial kinetic information.</figcaption></figure>

<table><caption>Figure 4: Steady state semantics.</caption><thead><tr><th>Linear equation system over R<sub>+</sub>:</th><th>Nonlinear constraints over Δ<sub>6</sub>:</th></tr></thead><tbody><tr><td>v<sub>in-A</sub> = v<sub>1</sub> + v<sub>2</sub></td><td>v<sub>1</sub> = A * D</td></tr><tr><td>v<sub>1</sub> = v<sub>out-B</sub></td><td>v<sub>2</sub> = A * E</td></tr><tr><td>v<sub>2</sub> = v<sub>out-C</sub></td><td>v<sub>3</sub> ∈ {↓, ~}</td></tr><tr><td>v<sub>4</sub> = v<sub>6</sub></td><td>v<sub>4</sub> ∈ {↓, ~}</td></tr><tr><td>v<sub>3</sub> = v<sub>5</sub></td><td>v<sub>5</sub> = D</td></tr><tr><td></td><td>v<sub>6</sub> = E</td></tr><tr><td></td><td>v<sub>out-B</sub> = B</td></tr><tr><td></td><td>v<sub>out-C</sub> = C</td></tr></tbody></table>

A simple example of reaction network with partial formal kinetic information is given in Figure 3; the linear equation system and the nonlinear constraints on its difference abstraction are given in Figure 4. The networks has five species A, B, C, D, E and nine reactions 1, ..., 6, *in-A*, *out-B*, *out-C*. As with the graphical notation for Petri nets, the species are nodes drawn as circles and the reactions nodes drawn as boxes. The colors of the species indicate their biological role, but do not contribute to the semantics. Metabolites are drawn in yellow and enzymes in brown circles. Reaction *in-A* is an inflow of the metabolite A, while reactions *out-B* and *out-C* are outflows of the metabolites B and C respectively. The inflows are controlled externally, while the outflows are controlled internally in the system. Reactions 3 and 4 correspond respectively to the gene expression of the enzymes D and E. These reactions may be knocked out, modeling a gene knockout. The knockouts are changes that are controlled externally similarly to the change of inflow *in-A*. None of the other reactions can be changed externally. Reaction 6 degrades the enzyme E and reaction 5 degrades the enzyme D. Reaction 1 transforms its metabolic substrate A, into its metabolic product B, while being activated and accelerated by the enzyme D. Symmetrically, the reaction 2 transforms its metabolic substrate A, into its metabolic product C, while being activated and accelerated by the enzyme E.

In a steady state of the reaction network, the concentrations of all its species become stable. For each species we have a linear equation, that states that the rate of its production is equal to the rate of its consumption. For species A, for instance, this is the following equation over $R_+$, since species A is produced by inflow *in-A* at rate $v_{in-A}$, while it is consumed by reaction 1 at rate $v_1$ and reaction 2 at rate $v_2$:

$$v_{in-A} = v_1 + v_2$$

The network has partial kinetic information: we know the enzymes (and inhibitors) of the reactions, but not necessarily their precise kinetics. For instance, the precise kinetics of reaction 1 is unknown. But since D is an enzyme of reaction 1 it follows that the rate $v_1$ is zero if the concentration of species D is zero, and that $v_1$ increases if the concentration of species D increases. Furthermore, since A is a substrate of reaction 1 it follows that $v_1$ is zero if the concentration of species A is zero, and that $v_1$ increases if the concentration of species A increases. This means that the following nonlinear constraint holds after difference abstraction to $Δ_6$:

$$v_1 = A * D$$

For reactions 3 and 4 which may be knocked out, we have the following constraints about their
<figure><img src="image_5.png" /><figcaption>Figure 5: Two changes leading to an increase of the outflow of B.</figcaption></figure>

difference abstraction to $\Delta_6$:

$$v_3 \in \{\downarrow, \sim\} \\ v_4 \in \{\downarrow, \sim\}$$

So the rates of these reactions may either decrease to zero or remain unchanged but different from zero.

A typical question for change prediction is which changes can be applied to the example network in order to increase the outflow of B, that is $v_{out-B} \doteq \uparrow$. The set of potential changes is to increase or decrease the inflow of A, i.e., $v_{in-A} \in \{\uparrow, \downarrow\}$, or to shut down reactions 3 or 4, that is $v_3 = \downarrow$ or $v_4 = \downarrow$. The two single-change predictions that answer this question are:

1. increase the inflow of A, that is $v_{in-A} \doteq \uparrow$, or

2. knock down reaction 4, i.e., $v_4 \doteq \downarrow$ and thus of the gene expression of enzyme E.

These two predictions correspond to the two abstract solutions over $\Delta_6$ in Figure 5. The first solution in Figure 5a motivates the prediction of an increase of in-A and the second solution in Figure 5b the prediction of a knock down of reaction 4, the gene expression producing enzyme E.

Both abstract solutions are difference abstractions over $\Delta_6$ of real positive solutions of the linear equation system in Figure 4, so that these difference abstractions do also satisfy the nonlinear constraints over $\Delta_6$ given there. We can find both predictions by applying John's overapproximation algorithm [8, 10], that is by computing the $\Delta_6$ solutions of linear equation system and the nonlinear constraints. This can be done in practice by using finite domain constraint programming.

Qualitative reasoning can also be performed manually for this simple example. For increasing out-B be must increase the concentration of B and thus the rate of reaction 1. For this, we must either increase the concentration of enzyme D which is impossible by the available changes, or increase the concentration of A. The latter requires to either increase the inflow of A, leading to the first abstract solution in Figure 5a, or else decrease the rate of reaction 2. This is possible by decreasing the concentration of E by knocking out the reaction 4, the gene expression producing this enzyme. This yields the second abstract solution in Figure 5b.

John's algorithm does not lead to any overapproximation for this example. The main reason is that the graph of the reaction network in Figure 3 is acyclic, even in the absence of partial
<figure><img src="image_6.png" /><figcaption>Figure 6: A reaction network with a simple loop.</figcaption></figure>

$$v_1 \doteq v_{in-A} + v_2 \\ v_1 \doteq v_{out-B} + v_2$$

<figure><img src="image_7.png" /><figcaption>Figure 8: Elementary flux modes of the simple loop network.</figcaption></figure>

kinetic information. The situation changes for reaction networks with cycles. The simplest counterexample is the simple loop in Figure 6. The linear equation system of this network is exactly the system from the introduction, where John's algorithm predicts unjustified changes.

This network has two species A and B and four reactions: an inflow of A, an outflow of B, a reaction 1 transforming A to B and a inverse reaction 2. So each molecule A that flows into the system may loop for a while, changing to B and back, before eventually outflowing as B. In a steady state, the rate of the inflow of A is equal to the rate of the outflow of B. The argument can be understood more easily, when considering the elementary flux modes [14, 23] of this reaction network, which are shown graphically in Figure 8 in red and respectively in green. An elementary flux mode is a linear combination of reactions that can become steady. The simple loop network has two elementary flux modes, corresponding to the linear combination of reactions $1v_{in-A} + 1v_1 + 1v_{out-B}$ using red edges and the linear combination of reactions $1v_1 + 1v_2$ with green edges respectively.

While some molecules may loop with the green edges, transforming A's to B's and back, all inflowing A's must follow the red edges and thus eventually outflow as B. From an algebraic perspective, the elementary flux modes of a reaction network correspond exactly to the elementary modes of its stoichiometry matrix [13]. An elementary mode of a matrix A is a positive integer solution of $Ax = 0$ where x a sequence of fresh variables. Furthermore, we require that the solution has minimal support, meaning that a minimal subset of the variables is assigned to a nonzero value, and that the solution is normalized (so it cannot be divided by any natural number strictly greater than 1). Note that the stoichiometry matrix of the simple loop network was given within the linear equation system (1) at the beginning of the introduction. Here, the vector of variables x corresponds to the order on reactions adopted by the stoichiometry matrix, so it can be chosen as $(v_{in-A}, v_{out-B}, v_1, v_2)$. Its elementary modes are (1, 1, 1, 0) and (0, 0, 1, 1).

The difference abstraction of any two concrete solutions of the linear equations of the simple loop network must satisfy $v_{in-A} = v_{out-B}$. The corresponding abstract solution over $\Delta_6$ satisfying $v_{in-A} = \uparrow$ and $v_{out-B} = \uparrow$ is illustrated in Figure 9. However, the alternative variable assignment to $\Delta_6$ in Figure 10 is also a solution of all linear equations when interpreted over $\Delta_6$, while not
<figure><img src="image_8.png" /><figcaption>Figure 9: A justified abstract solution.</figcaption></figure>

<caption>Figure 10: An unjustified abstract solution.</caption>

being justified by any pair of concrete solutions over $\mathbb{R}_+$.

The intuitive reason for this failure is that John's overapproximation algorithm performs only local reasoning, considering one linear equation at a time, i.e., one species of the reaction network. In this manner, it cannot see, that $X \doteq Y$ is a logical consequence of the linear equation system of the network over $\mathbb{R}_+$, while it is not a consequence over $\Delta_6$. So what we are searching is way to reason globally with all species of a reaction network at a time. For this we have to take into account all linear combinations of the equations of the system.

# 4. Preliminaries

We present standard notion of sets, partial and total functions, relations, $\Sigma$-algebras and $\Sigma$-structures.

## 4.1. Set and Functions

We start with the usual notation for sets. Let $\mathbb{N}$ be the set of natural numbers and $\mathbb{R}_+$ the set of positive real numbers, both including 0. For any set $A$ and $n \in \mathbb{N}$, the set of $n$-tuples of elements in $A$ is denoted by $A^n$. The $i$-th projection function on $n$-tuples of elements in $A$, where $1 \le i \le n$ is the function $\pi_i : A^n \to A$ such that $\pi_i(a_1, \dots, a_n) = a_i$ for all $a_1, \dots, a_n \in A$. If $A$ is finite the number of elements of $A$ is denoted by $|A|$.

We continue with notation for total and partial functions. A partial function is a relation $f \subseteq A \times B$ such that for all $a \in A$ there exists at most one $b \in B$ such that $(a, b) \in f$. In this case, we write $f(a) = b$. The domain of the partial function is $dom(f) = \{a | \exists b \in B. f(a) = b\}$ and its range $ran(f) = \{b | \exists a \in A. f(a) = b\}$. A total function $f : A \to B$ is a partial function $f \subseteq A \times B$ such that $dom(f) = A$. Given a total function $f : A \to B$ and a partial function $g : B \times C$ such that $ran(f) \subseteq dom(g)$ we define the function composition as the total function $g \circ f : A \to C$ such that $(g \circ f)(x) = g(f(x))$ for all $x \in A$. Furthermore if $R \subseteq \{f : A \to B\}$ then we define:

$$g \circ R = \{g \circ f : A \to C \mid f \in R, ran(f) \subseteq dom(g)\}$$

Note that $g \circ f$ is defined only if $ran(f) \subseteq dom(g)$, so functions $f \in R$ violating this condition will be ignored all over in the composition $g \circ R$. This is since we want all the functions in $g \circ R$ to be total even if $g$ is partial.

## 4.2. $\Sigma$-Algebras and $\Sigma$-Structures

We next recall the notions of $\Sigma$-algebras, $\Sigma$-structures, and homomorphism between $\Sigma$-structures. These classical notions of universal algebra will be fundamental to our algebraic generalization of difference abstractions to the notion of $\Sigma$-abstractions in Definition 8.
Let $\Sigma = \cup_{n \ge 0} F^{(n)} \uplus C$ be a ranked signature. The elements of $f \in F^{(n)}$ are called the $n$-ary function symbols of $\Sigma$ and the elements in $c \in C$ its constants.

**Definition 2.** A $\Sigma$-algebra $S = (dom(S), .^S)$ consists of a set $dom(S)$ and an interpretation .$^S$ such that $c^S \in dom(S)$ for all $c \in C$, and $f^S : dom(S)^n \to dom(S)$ for all $f \in F^{(n)}$ and $n \in \mathbb{N}$.

We next reinterpret $n$-ary function symbols of $\Sigma$ as $n+1$-ary relation symbols, so that we can reuse the same signature $\Sigma$ for defining $\Sigma$-structures.

**Definition 3.** A $\Sigma$-structure $\Delta = (dom(\Delta), .^\Delta)$ consists of a set $dom(\Delta)$ and an interpretation .$^\Delta$ such that $c^\Delta \in dom(\Delta)$ for all $c \in C$ and $f^\Delta \subseteq dom(\Delta)^{n+1}$ for all $f \in F^{(n)}$ and $n \in \mathbb{N}$.

In this manner, any $\Sigma$-algebra is also a $\Sigma$-structure since any $n$-ary function is an $n+1$-ary relation. Note also that symbols in $F^{(0)}$ are interpreted as monadic relations in $\Sigma$-structures, i.e., as subsets of the domain, in contrast to constants in $C$ that are interpreted as elements of the domain.

It is sometimes useful to add the elements of the domain of a $\Sigma$-structure $A$ to the constants. Therefore, we define the extended signature:

$$ \Sigma[dom(A)] = \Sigma \uplus dom(A) $$

The $\Sigma$-structure $A$ can be lifted to a $\Sigma[dom(A)]$-structure by interpreting the new constants by themselves, i.e., $a^A = a$ for all $a \in dom(A)$, and all symbols in $\Sigma$ as before.

**Definition 4.** A homomorphism between two $\Sigma$-structures $S$ and $\Delta$ is a function $h : dom(S) \to dom(\Delta)$ such that for $c \in C$, $n \in \mathbb{N}$, $f \in F^{(n)}$, and $s_1, \dots, s_{n+1} \in dom(S)$:

1. $h(c^S) = c^\Delta$, and

2. if $(s_1, \dots, s_{n+1}) \in f^S$ then $(h(s_1), \dots, h(s_{n+1})) \in f^\Delta$.

For $\Sigma$-algebras, the second condition is equivalent to $h(f^S(s_1, \dots, s_n)) = f^\Delta(h(s_1), \dots, h(s_n))$.

For any $\Sigma$-structure $S$ we can reinterpret $n+1$ ary relations $f^S$ as $n$-ary set valued functions. In order to do so, we define for any sequence $s_1, \dots, s_n \in dom(S)$ a subset of values:

$$ f^{\Delta}(s_1, \dots, s_n) = \{s \in dom(S) \mid (s_1, \dots, s_n, s) \in f^{\Delta}\} $$

With this set-valued reinterpretation, the second condition of homomorphisms can be rewritten equivalently to:

$$ h(f^S(s_1, \dots, s_n)) \subseteq f^\Delta(h(s_1), \dots, h(s_n)) $$

## 5. $\Sigma$-Abstractions

We introduce the concept of $\Sigma$-abstractions for general signatures. Before doing so, we start with an example for a $\Sigma$-abstraction, which is the boolean abstraction of positive real numbers.

It has the signature of arithmetics $\Sigma = F_{\text{pos-arith}}^{(2)} \uplus C_{\text{pos-arith}}$ with two binary function symbols and two constants such that:

$$ F_{\text{pos-arith}}^{(2)} = \{+, *\} $$

$$ C_{\text{pos-arith}} = \{0, 1\} $$

For all $\Sigma$-algebras considered, the operators $+^S$ and $*^S$ are associative and commutative, with neutral element $0^S$ and $1^S$ respectively.
**Example 5.** The set of positive real numbers $\mathbb{R}_+$ can be turned into a $\Sigma$-algebra with domain $\mathbb{R}_+$, by interpreting $+$ as the addition of positive real numbers $+_{\mathbb{R}_+}$, $*$ as the multiplication of positive real numbers $*_{\mathbb{R}_+}$, and interpreting the constants by themselves $0_{\mathbb{R}_+} = 0$ and $1_{\mathbb{R}_+} = 1$. We will deliberately confuse the set $\mathbb{R}_+$ with the $\Sigma$-algebra $(\mathbb{R}_+, ._{\mathbb{R}_+})$ whose domain $\text{dom}(\mathbb{R}_+)$ is equal to the set of positive reals $\mathbb{R}_+$.

**Example 6.** The set of Booleans $\mathbb{B} = \{0, 1\} \subseteq \mathbb{R}_+$ can be turned into a $\Sigma$-algebra with domain $\mathbb{B}$ by interpreting $+_{\mathbb{B}} = \vee_{\mathbb{B}}$ as disjunction, $*_{\mathbb{B}} = \wedge_{\mathbb{B}}$ as conjunction, and the constants by themselves $0_{\mathbb{B}} = 0$ and $1_{\mathbb{B}} = 1$. We will deliberately confuse the set $\mathbb{B}$ with the $\Sigma$-algebra $(\mathbb{B}, ._{\mathbb{B}})$ whose domain $\text{dom}(\mathbb{B})$ is the set of booleans $\mathbb{B}$.

We can abstract positive real numbers into booleans by defining a function $h_{\mathbb{B}} : \mathbb{R}_+ \to \mathbb{B}$ such that $h_{\mathbb{B}}(0) = 0$ and $h_{\mathbb{B}}(r) = 1$ for all $r \in \mathbb{R}_+ \setminus \{0\}$.

**Lemma 7.** The function $h_{\mathbb{B}} : \mathbb{R}_+ \to \mathbb{B}$ is a homomorphism between $\Sigma$-algebras where $\Sigma = F_{\text{pos-arith}}^{(2)} \cup C_{\text{pos-arith}}$.

**Proof** For all $r, r' \in \mathbb{R}_+$ we have:

$$ \begin{aligned} h_{\mathbb{B}}(r +_{\mathbb{R}_+} r') &= 1 & \Leftrightarrow & r +_{\mathbb{R}_+} r' \neq 0 & \Leftrightarrow & r \neq 0 \lor r' \neq 0 & \Leftrightarrow & h_{\mathbb{B}}(r) = 1 \lor h_{\mathbb{B}}(r') = 1 \\ h_{\mathbb{B}}(r *_{\mathbb{R}_+} r') &= 1 & \Leftrightarrow & r *_{\mathbb{R}_+} r' \neq 0 & \Leftrightarrow & r \neq 0 \land r' \neq 0 & \Leftrightarrow & h_{\mathbb{B}}(r) = 1 \land h_{\mathbb{B}}(r') = 1 \end{aligned} $$

Hence $h_{\mathbb{B}}(r +_{\mathbb{R}_+} r') = h_{\mathbb{B}}(r) +_{\mathbb{B}} h_{\mathbb{B}}(r')$ and $h_{\mathbb{B}}(r *_{\mathbb{R}_+} r') = h_{\mathbb{B}}(r) *_{\mathbb{B}} h_{\mathbb{B}}(r')$. Finally, for both constants $c \in C$ we have that $h_{\mathbb{B}}(c_{\mathbb{R}_+}) = h_{\mathbb{B}}(c) = c = c_{\mathbb{B}}$. $\square$

The boolean abstraction $h_{\mathbb{B}}$ is the prime example of what we will call a $\Sigma$-abstraction. The following definition applies for general signatures.

**Definition 8.** A $\Sigma$-abstraction is a homomorphism between $\Sigma$-structures $S$ and $\Delta$ such that $\text{dom}(\Delta) \subseteq \text{dom}(S)$.

We assume that $\text{dom}(\Delta) \subseteq \text{dom}(S)$ since this will permit us to reason about $\Sigma$-abstractions by talking at the same time about concrete values in $\text{dom}(S)$ and abstract values in $\text{dom}(\Delta)$ by first-order formulas interpreted over the $\Sigma$-structure $S$.

# 6. Abstracting Concrete Differences

Concrete differences are pairs of positive in $\mathbb{R}_+^2$. We show how to abstract concrete differences into abstract differences. For this, we consider $\mathbb{R}_+^2$ as a $\Sigma$-algebra that we then abstract into finite $\Sigma$-structures $\Delta_3$ and $\Delta_6$.

## 6.1. The Tuple $\Sigma$-Algebra $S^n$

For any $\Sigma$-algebra $S$ where $\Sigma = F^{(2)} \cup C$ and natural number $n \in \mathbb{N}$ we define the $\Sigma$-algebra of $n$-tuples $S^n = (\text{dom}(S)^n, ._{S^n})$ such that for all $s_1, \dots, s_n, s'_1, \dots, s'_n \in \text{dom}(S)$ and $\odot \in F^{(2)}$:

$$ (s_1, \dots, s_n) \odot^{S^n} (s'_1, \dots, s'_n) = (s_1 \odot^S s'_1, \dots, s_n \odot^S s'_n) $$

The constants $c \in C$ are interpreted as $c^{S^n} = (c^S, \dots, c^S)$. Note that if $0^S$ is the neutral element of $+^S$, then $0^{S^n}$ is the also the neutral element of $+^{S^n}$. In analogy, if $1^S$ is the neutral element of $*^S$ then $1^{S^n}$ is also the neutral element of $*^{S^n}$. Furthermore, the associativity and commutativity of $+^{S^n}$ and $*^{S^n}$ inherit from $+^S$ and $*^S$ respectively.
Note that we deliberately confuse the set $\mathbb{R}_+^2$ with the $\Sigma$-algebra $(\mathbb{R}_+^2, \mathbb{R}_+^2)$ with our notation. Given this, it follows from the above, that the algebra $\mathbb{R}_+^2$ has the neutral element $(0, 0)$ for $+\mathbb{R}_+$ and the neutral element $(1, 1)$ for $\mathbb{R}_+^2$, and that these operations are associative and commutative.

For any function $h: A \to B$ and $n \in \mathbb{N}$ we define the function $h^n: A^n \to B^n$ such that $h^n(a_1, \dots, a_n) = (h(a_1), \dots, h(a_n))$ for all $a_1, \dots, a_n \in A$.

**Lemma 9.** If $h$ is a $\Sigma$-abstraction from $S$ to $\Delta$ then $h^n$ is a $\Sigma$-abstraction from $S^n$ to $\Delta^n$.

**Proof** Let $\odot \in F^{(2)}$ and $t = (s_1, \dots, s_n)$, $t' = (s'_1, \dots, s'_n) \in \text{dom}(S)^n$. Then we have:

$$ 
\begin{align*}
h^n(t \odot^{S^n} t') &= (h(s_1 \odot^S s'_1), \dots, h(s_n \odot^S s'_n)) & \text{definitions of } h^n \text{ and } S^n \\
&= (h(s_1) \odot^\Delta h(s'_1), \dots, h(s_n) \odot^\Delta h(s'_n)) & \text{since } h \text{ is homomorphism} \\
&= (h(s_1), \dots, h(s_n)) \odot^{\Delta^n} (h(s'_1), \dots, h(s'_n)) & \text{definition of } \Delta^n \\
&= h^n(t) \odot^{\Delta^n} h^n(t') & \text{definition of } h^n
\end{align*}
$$

Finally, for both constants $c \in C$ we have:

$$ 
\begin{align*}
h^n(c^{S^n}) &= h^n(c^S, \dots, c^S) & \text{definition } S^n \\
&= (h(c^S), \dots, h(c^S)) & \text{definition } h^n \\
&= (c^\Delta, \dots, c^\Delta) & \text{since } h \text{ is homomorphism} \\
&= c^{\Delta^n} & \text{definition of } \Delta^n
\end{align*}
$$

□

## 6.2. Abstractions of Concrete Differences

Given that $\mathbb{R}_+$ is a $\Sigma$-algebra with signature $\Sigma = F_{\text{pos-arith}}^{(2)} \cup C_{\text{pos-arith}}$, we have that $\mathbb{R}_+^2$ is also a $\Sigma$-algebra with the same signature.

We now show how to abstract the concrete differences in $\mathbb{R}_+^2$ to abstract difference. A generic manner to do so is to start with some some partition $h: \mathbb{R}_+^2 \to \Delta$ into a finite set $\Delta$. The elements of this set will be called the *abstract differences*. The function $h$ says how to abstract concrete to abstract differences. Since it is a partition, it splits $\mathbb{R}_+^2$ into finitely many equivalence classes.

For any partition $h: \mathbb{R}_+^2 \to \Delta$, there is a unique manner to define an interpretation $\Delta^\Delta$ such that $(\Delta, \Delta^\Delta)$ becomes $\Sigma$-structure with domain $\Delta$ and $h$ a $\Sigma$-abstraction. For any constant $c \in C$ we have to define $c^\Delta = h(c_{\mathbb{R}_+^2})$ and for any function symbol $\odot \in F^{(2)}$ we have to define a ternary relation $\odot^\Delta$, which seen as set-valued function $\odot^\Delta: \Delta \times \Delta \to 2^\Delta$ must satisfy for all abstract values $d_1, d_2 \in \Delta$:

$$ d_1 \odot^\Delta d_2 = \{h(r_1 \odot^{\mathbb{R}_+} r_2, r'_1 \odot^{\mathbb{R}_+} r'_2) \mid h(r_1, r'_1) = d_1, h(r_2, r'_2) = d_2\} $$

**Lemma 10.** $h: \mathbb{R}_+^2 \to \Delta$ is a $\Sigma$-abstraction where $\Sigma = F_{\text{pos-arith}}^{(2)} \cup C_{\text{pos-arith}}$.

**Proof** For any $p_1 = (r_1, r'_1)$, $p_2 = (r_2, r'_2) \in \mathbb{R}_+^2$ the second condition for homomorphisms follows for all $\odot \in F_{\text{pos-arith}}^{(2)}$:

$$ h(p_1 \odot^{\mathbb{R}_+^2} p_2) = h(r_1 \odot^{\mathbb{R}_+} r_2, r'_1 \odot^{\mathbb{R}_+} r'_2) \in h(p_1) \odot^\Delta h(p_2) $$

Finally, for all constants $c \in C_{\text{pos-arith}}$ we have by definition that $h(c_{\mathbb{R}_+^2}) = c^\Delta$. □
<table><thead><tr><th>d</th><th>d'</th><th>d + Δ<sup>3</sup></th><th>d'</th><th>d * Δ<sup>3</sup></th><th>d'</th></tr></thead><tbody><tr><td>Δ</td><td>Δ</td><td>{Δ}</td><td></td><td>{Δ}</td><td></td></tr><tr><td>Δ</td><td>∇</td><td>{Δ, ≈, ∇}</td><td></td><td>{Δ, ≈, ∇}</td><td></td></tr><tr><td>Δ</td><td>≈</td><td>{Δ}</td><td></td><td>{Δ, ≈}</td><td></td></tr></tbody></table>

<table><thead><tr><th>d</th><th>d'</th><th>d + Δ<sup>3</sup></th><th>d'</th><th>d * Δ<sup>3</sup></th><th>d'</th></tr></thead><tbody><tr><td>≈</td><td>≈</td><td>{≈}</td><td></td><td>{≈}</td><td></td></tr><tr><td>∇</td><td>∇</td><td>{∇}</td><td></td><td>{∇}</td><td></td></tr><tr><td>∇</td><td>≈</td><td>{∇}</td><td></td><td>{∇, ≈}</td><td></td></tr></tbody></table>

<table><caption>Figure 11: Interpretation of Σ-structure Δ<sub>3</sub>.</caption><thead><tr><th>c</th><th>c<sup>Δ<sub>3</sub></sup></th></tr></thead><tbody><tr><td>0</td><td>≈</td></tr><tr><td>1</td><td>≈</td></tr></tbody></table>

### 6.3. The Σ-Structure Δ<sub>3</sub>

We continue with the signature of arithmethics $\Sigma = F_{\text{pos-arith}}^{(2)} \uplus C_{\text{pos-arith}}$ Our next objective is to recall the abstraction of concrete differences from the Σ-algebra $\mathbb{R}_+$ into the finite Σ-structure with domain $\Delta_3 = \{\Delta, \nabla, \approx\}$ that is well-known from qualitative reasoning (see e.g. [24]). For this we start with the function $h_{\Delta_3}(r, r') \in \Delta_3$ such that for any $r, r' \in \mathbb{R}_+$:

$$h_{\Delta_3}(r, r') = \begin{cases} \Delta = (0, 1) & \text{if } r < r' \\ \nabla = (1, 0) & \text{if } r > r' \\ \approx = (0, 0) & \text{if } r = r' \end{cases}$$

We define the ternary relation $+^{\Delta_3}$ as the relation that is symmetric in the first two arguments and has the set-valued reinterpretation $d +^{\Delta_3} d' \subseteq \Delta_3$ in Figure 11 for all $d, d' \in \Delta_3$. The definition of $*^{\Delta_3}$ is given in analogy in the same figure. The interpretation of the constants are $1^{\Delta_3} = 0^{\Delta_3} = \approx$. By Lemma 10, $h_{\Delta_3} : \mathbb{R}_+^2 \to \Delta_3$ is a Σ-abstraction.

### 6.4. The Σ-Structure Δ<sub>6</sub>

We next recall the abstraction of concrete differences to the finite Σ-structure with domain $\Delta_6 = \{↑, ↓, ∼, ↑, ↓, ≈\}$ that was introduced for gene knockout prediction in [8]. For defining this Σ-structure, we start with the function $h_{\Delta_6} : \mathbb{R}_+^2 \to \Delta_6$ such that for any two numbers $r, r' \in \mathbb{R}_+$:

$$h_{\Delta_6}(r, r') = \begin{cases} ↑ = (1, 2) & \text{if } 0 \neq r < r' \\ ↓ = (2, 1) & \text{if } r > r' \neq 0 \\ \sim = (1, 1) & \text{if } r = r' \neq 0 \end{cases}$$

$$h_{\Delta_6}(r, r') = \begin{cases} ↑ = (0, 2) & \text{if } 0 = r < r' \\ ↓ = (2, 0) & \text{if } r > r' = 0 \\ \approx = (0, 0) & \text{if } r = r' = 0 \end{cases}$$

We define the ternary relation $+^{\Delta_6}$ as the relation that is symmetric in the first two arguments and has the set-valued reinterpretation $d +^{\Delta_6} d' \subseteq \Delta_6$ in Figure 12 for all $d, d' \in \Delta_6$. The relation $*^{\Delta_6}$ is defined in the same style in Figure 12. The constants are interpreted as $0^{\Delta_6} = \approx$ and $1^{\Delta_6} = \sim$. By Lemma 10, $h_{\Delta_6} : \mathbb{R}_+^2 \to \Delta_6$ is a Σ-abstraction.

## 7. First-Order Logic

We first recall the standard first-order logic and then show how to enhance it with n-tuples without increasing the expressiveness.

### 7.1. Standard First-Order Logic

We fix a set of variables $V$ (for instance $V = \mathbb{N}$). The variables in $V$ will be ranged over by $x$ and $y$. The signature $\Sigma = F^{(2)} \uplus C$ is arbitrary here.

The set of first-order expressions $e \in \mathcal{E}_{\Sigma}$ and first-order formulas $\phi \in \mathcal{F}_{\Sigma}$ are constructed according to the abstract syntax in Figure 13 from the symbols in the signature $\Sigma$, the variables in $V$, the first-order connectives, and the equality symbol $\doteq$. As shortcuts, we define the formula
<figure><img src="image_9.png" /><figcaption>Figure 12: Interpretation of Σ-structure Δ₆.</figcaption></figure>

true =def 1 = 1 and for any sequence of formulas φ₁, ..., φₙ we define ∧ₙᵢ=₁φᵢ as φ₁ ∧ ... ∧ φₙ which is equal to true if n = 0. We define formulas e̸=0 by ¬e = 0.

The semantics of expressions in Figure 13 is defined such that the following formula becomes true in the structure Δ₃ taken with the signature extended with extra constants Σ[dom(Δ₃)]:

$$ \begin{array}{l} \Delta + \nabla \doteq \Delta \\ \wedge \quad \Delta + \nabla \doteq \nabla \\ \wedge \quad \Delta + \nabla \doteq \approx \end{array} $$

The first reason is that relations are reinterpreted as set-valued functions by the semantics of first order logic. In particular, we have Δ + Δ³ ∨ = Δ₃. The second reason is that the meaning of the equality operator = of the logic is nondeterministic equality, that is the nondisjointness. Also note that the following formula is unsatisfiable:

$$ \exists x. (x \doteq \Delta \land x \doteq \nabla) $$

This is since for any variable assignment the expression x must evaluated to a singleton, which cannot contain both Δ and ∨. Another way to see this is that ∃x. (x = Δ ∧ x = ∨) is equivalent to ∨ = Δ which evaluates to false.

More generally, the semantics of a formula φ ∈ ℱ_Σ is a truth value, which depends on the Σ-structures S of interpretation and on a variable assignment α : V → dom(S). Any Σ-expressions e ∈ ℰ_Σ denotes a subset of values in dom(S), which will be singleton in case that S was a Σ-algebra. The semantic of equations e = e' is, as expected when interpreted over Σ-algebras S: the unique values of e and e' in S must be equal. However, we will also need to interpret equations e = e' over Σ-structures. This is why, any expression e denotes a subset of the Σ-structure, not just a single element. We can then interpret equality as nondisjointness, i.e., e = e' holds in a Σ-structure S if e and e' are interpreted as nondisjoint subsets of dom(S).

A variable assignment into a Σ-structure S is a partial function α : V → dom(S) for some subset V ⊆ V. Let S be a Σ-structure and α a variable assignment to S. Any Σ-expression e with fv(e) ⊆ V can be interpreted as an element of dom(S) and any Σ-formula φ ∈ ℱ_Σ with
First-order expressions and formulas:

$$e \in \mathcal{E}_{\Sigma} \quad ::= \quad x \mid c \mid e \odot e' \qquad \text{where } \odot \in F^{(2)}, c \in C$$

$$\phi \in \mathcal{F}_{\Sigma} \quad ::= \quad e = e \mid \exists x. \phi \mid \phi \wedge \phi \mid \neg \phi \qquad \text{where } x \in \mathcal{V}$$

Set-valued interpretation of expressions: $[[e]]^{\alpha,S} \subseteq \text{dom}(S)$, where $S$ is a $\Sigma$-structures and $\alpha: V \to \text{dom}(S)$ where $V$ contains all free variables.

$$[[c]]^{\alpha,S} = \{c^S\} \quad [[x]]^{\alpha,S} = \{\alpha(x)\} \quad [[e \odot e')]^{\alpha,S} = \bigcup \{s \odot^S s' \mid s \in [[e]]^{\alpha,S}, s' \in [[e')]^{\alpha,S}\}$$

Interpretation of formulas as truth values $[[\phi]]^{\alpha,S} \in \mathbb{B}$:

$$[[e \doteq e')]^{\alpha,S} = \begin{cases} 1 & \text{if } [[e]]^{\alpha,S} \cap [[e')]^{\alpha,S} \neq \emptyset \\ 0 & \text{else} \end{cases} \qquad [[\phi \wedge \phi')]^{\alpha,S} = [[\phi]]^{\alpha,S} \wedge \mathbb{B} [[\phi')]^{\alpha,S} \\ \\ [[\neg \phi]]^{\alpha,S} = \neg \mathbb{B} ([[\phi]]^{\alpha,S}) \qquad [[\exists x. \phi]]^{\alpha,S} = \begin{cases} 1 & \text{if exists } s \in \text{dom}(S). \\ \neg \mathbb{B} [[\phi]]^{\alpha[x/s],S} & \text{else} \end{cases}$$

<caption>Figure 13: Syntax and semantics of expressions and formulas of first-order logic.</caption>

$$o \in \mathcal{O}_{\Sigma}^{n} ::= \dot{\pi}_{i}(x) \mid c \mid o \odot o \qquad \text{where } 1 \le i \le n, c \in C \text{ and } \odot \in F^{(2)}.$$

$$\psi \in \mathcal{F}_{\Sigma}^{n} ::= o \doteq o' \mid \exists x. \psi \mid \psi \wedge \psi \mid \neg \psi \qquad \text{where } x \in \mathcal{V}$$

<caption>Figure 14: Expressions and formulas of the first-order logic with n-tuples.</caption>

$fv(\phi) \subseteq V$ as a Boolean value. The set of solutions of a formula $\phi \in \mathcal{F}_{\Sigma}$ over a $\Sigma$-structure $S$ with respect to some set of variables $V \supseteq fv(\phi)$ is defined by:

$$\text{sol}_{V}^{S}(\phi) = \{\alpha : V \to \text{dom}(S) \mid [[\phi]]^{\alpha,S} = 1\}$$

If $V = fv(\phi)$ then we omit the index $V$, i.e., $\text{sol}^S(\phi) = \text{sol}_V^S(\phi)$.

## 7.2. First-Order Tuple Logic

We next extend the first-order logic to n-tuples where the parameter $n$ is fixed. In applications, we will use the case $n = 2$, that is the first-order logic with pairs. Back and forth compilers from first-order logic with and without tuples will be convenient later on.

The syntax of first-order logic with n-tuples is given in Figure 14. The expressions $o \in \mathcal{O}_{\Sigma}^{n}$ are like the expression $e \in \mathcal{E}_{\Sigma}$ except that variables $x$ are now replaced by projection expressions $\dot{\pi}_{i}(x)$ where $1 \le i \le n$. The reason is that any variable does now denote an n-tuple of values, rather than a single value (while the interpretation of constants and function symbols remain unchanged). The only change in the semantics is that variables assignment $\beta$ do now map to n-tuples of values of the domain, and that $[[\pi_{i}(x)]^{S,\beta} = \{\pi_{i}(\beta(x))\}$. The set of solutions of a formula $\psi \in \mathcal{F}_{\Sigma}^{n}$ over a $\Sigma$-structure $S$ is defined as follows:

$$n-\text{sol}^S(\psi) = \{\beta : fv(\psi) \to \text{dom}(S)^n \mid [[\psi]]^{\beta,S} = 1\}$$

We next show how to express any first-order formulas in $\mathcal{F}_{\Sigma}$, interpreted over a tuple algebra $S^n$, by some formulas in $\mathcal{F}_{\Sigma}^n$, interpreted over $S$. In a first step, we convert first-order expression in $e \in \mathcal{E}_{\Sigma}$ – that we will interpret over the $\Sigma$-algebra $S^n$ – to $n$ projected expressions $\Pi_{i}(e) \in \mathcal{O}_{\Sigma}^{n}$ where $1 \le i \le n$. For all operators $\odot \in F^{(2)}$ and constants $c \in C$ we define:

$$\Pi_i(e \odot e') =_{\text{def}} \Pi_i(e) \odot \Pi_i(e') \qquad \Pi_i(x) =_{\text{def}} \dot{\pi}_i(x) \qquad \Pi_i(c) =_{\text{def}} c$$
In the second step, we convert any formula $\phi \in \mathcal{F}_{\Sigma}$ without tuples – that will be interpreted in the tuple algebra $S^n$ – to some formula $\langle\phi\rangle^n \in \mathcal{F}_{\Sigma}^n$ with tuples.

$$ \begin{aligned} \langle e \doteq e' \rangle^n &= \mathit{def} \wedge_{i=1}^n \Pi_i(e) \doteq \Pi_i(e') \\ \langle \neg \phi \rangle^n &= \mathit{def} \neg \langle \phi \rangle^n \\ \langle \exists x. \phi \rangle^n &= \mathit{def} \exists x. \langle \phi \rangle^n \end{aligned} $$

**Lemma 11.** For any $e \in \mathcal{E}_{\Sigma}$, $\Sigma$-algebra $S$, $n \ge 1$, and $\beta: V \to \mathrm{dom}(S)^n$ with $\mathcal{V}(\phi) \subseteq V \subseteq \mathcal{V}$:

$$ \llbracket e \rrbracket^{\beta, S^n} = \llbracket (\Pi_1(e), \dots, \Pi_n(e)) \rrbracket^{\beta, S} $$

*Proof sketch.* By induction on the structure of expressions in $\mathcal{E}_{\Sigma}$.

<figure><img src="image_10.png" /></figure>

**Proposition 12.** For any $\phi \in \mathcal{F}_{\Sigma}$, $\Sigma$-algebra $S$, and $n \ge 1$: $\mathrm{sol}^{S^n}(\phi) = n-\mathrm{sol}^S(\langle\phi\rangle^n)$.

*Proof sketch.* By induction on the structure of formulas in $\mathcal{F}_{\Sigma}$. We only show the base case of $\Sigma$-equations. So let $\phi$ is a $\Sigma$-equation of the form $e \doteq e'$ where $e, e' \in \mathcal{E}_{\Sigma}$ and $\beta$ a variable assignment $\beta: V \to \mathrm{dom}(S)^n$ such that $\mathcal{V}(\phi) \subseteq V \subseteq \mathcal{V}$. Then:

$$ \begin{aligned} \mathrm{sol}^{S^n}(e \doteq e') &= \{\beta \mid \llbracket e \doteq e' \rrbracket^{\beta, S^n} = 1\} \\ \text{Lemma 11} \quad &= \{\beta \mid \llbracket \bigwedge_{i=1}^n \Pi_i(e) \doteq \Pi_i(e') \rrbracket^{\beta, S} = 1\} \\ &= \{\beta \mid \llbracket \langle e \doteq e' \rangle^n \rrbracket^{\beta, S} = 1\} \\ &= n-\mathrm{sol}^S(\langle e \doteq e' \rangle^n) \end{aligned} $$

The inductive cases for the other formulas are straightforward.

<figure><img src="image_11.png" /></figure>

### 7.3. Polynomial Equations

In the case of the arithmetic signature $\Sigma = F_{\mathrm{pos-arith}}^{(2)} \uplus C_{\mathrm{pos-arith}}$, the arithmetic equations $e \doteq e' \in \mathcal{F}_{\Sigma}$ provided by the formulas of standard FO-logic subsume the usual polynomial equations with natural coefficients. We will use the following notation for writing polynomials. For any natural $n$ and expression $e, e_1, \dots, e_n \in \mathcal{E}_{\Sigma}$, we define the expression $\prod_{i=1}^n e_i = e_1 * \dots * e_n$, which is equal to 1 if $n = 0$ and $\sum_{i=1}^n e_i = e_1 + \dots + e_n$ which is equal to 0 if $n = 0$. Furthermore, let $e^n = \prod_{i=1}^n e$ and $ne = \mathit{def} \sum_{i=1}^n e$. The analogous definitions $no$ and $o^n$ can be made for object expression in $o \in \mathcal{O}_{\Sigma}^n$ of the FO-tuple logic instead of expression in $e \in \mathcal{E}_{\Sigma}$ of the standard first-order logic.

**Example 13.** Let $\phi \in \mathcal{F}_{\Sigma}$ be the polynomial equation $3x + 4y^5 \doteq 0$ of the standard FO-logic. Proposition 12 shows that $\phi$ has the same solutions over $\mathbb{R}_+^2$ than the formula $\langle\phi\rangle^2 \in \mathcal{F}_{\Sigma}^2$ of the tuple FO-logic over $\mathbb{R}_+$. The latter is the system of polynomial equations $3\pi_1(x) + 4\pi_1(y)^5 \doteq 0 \wedge 3\pi_2(x) + 4\pi_2(y)^5 \doteq 0$.

Concrete differences can be described by systems of polynomial equations of the standard FO-logic but interpreted over $\mathbb{R}_+^2$. As shown by Proposition 12, such systems can thus be mapped to systems of polynomial equations in the FO-pair logic, but now interpreted over $\mathbb{R}_+$. This is done by copying each equation over $\mathbb{R}_+^2$ into two equations of $\mathbb{R}_+$, as illustrated by the above example.

Our next objective is to introduce fresh variables for projections in order to rewrite equation systems from the FO-pair logic into equation systems from the standard FO-logic. For instance, when given two fresh variable generators $\nu_1$ and $\nu_2$, the system of polynomial equations $3\pi_1(x) + 4\pi_1(y)^5 \doteq 0 \wedge 3\pi_2(x) + 4\pi_2(y)^5 \doteq 0$ in the FO-pair logic can be mapped to the systems of polynomial equations $3\nu_1(x) + 4\nu_1(y)^5 \doteq 0 \wedge 3\nu_2(x) + 4\nu_2(y)^5 \doteq 0$ in the standard FO-logic. The 4 fresh variables such as $\nu_i(x)$ and $\nu_i(y)$ correspond to the projections $\pi_i(x)$ and $\pi_i(y)$ respectively. With respect to the standard FO-logic, we can thus rewrite any system of polynomial equation over $\mathbb{R}_+^2$ to a system of polynomial equation over $\mathbb{R}_+$, so that the solutions correspond. The unique role of the FO-pair logic is to serve us as an intermediate language for this purpose.
### 7.4. From first-order tuple logic to Standard First-order Logic

More generally, we wish to rewrite any FO-tuple formula $\psi \in \mathcal{F}_{\Sigma}^n$ into a standard FO formula $\tilde{\nu}(\psi) \in \mathcal{F}_{\Sigma}$ by introducing fresh variables for projections. For this, we fix $n$ generators of fresh variables $\nu_1, \dots, \nu_n : \mathcal{V} \to \mathcal{V}$. We then map any expression $o \in \mathcal{O}_{\Sigma}^n$ with projections to some expressions $\tilde{\nu}(o) \in \mathcal{E}_{\Sigma}$ without new variables:

$$ \tilde{\nu}(\pi_i(x)) =_{\text{def}} \nu_i(x), \quad \tilde{\nu}(c) =_{\text{def}} c, \quad \tilde{\nu}(o \odot o') =_{\text{def}} \tilde{\nu}(o) \odot \tilde{\nu}(o'). $$

And finally, we map any formula $\psi \in \mathcal{F}_{\Sigma}^n$ with projections to some formula $\tilde{\nu}(\psi) \in \mathcal{F}_{\Sigma}$ with fresh variables:

$$ \begin{aligned} \tilde{\nu}(o = o') &=_{\text{def}} \tilde{\nu}(o) = \tilde{\nu}(o') & \tilde{\nu}(\neg \psi) &=_{\text{def}} \neg \tilde{\nu}(\psi) \\ \tilde{\nu}(\psi \wedge \psi') &=_{\text{def}} \tilde{\nu}(\psi) \wedge \tilde{\nu}(\psi') & \tilde{\nu}(\exists x. \psi) &=_{\text{def}} \exists \nu_1(x) \dots \exists \nu_n(x). \tilde{\nu}(\psi) \end{aligned} $$

Given a variable assignment $\beta : V \to \text{dom}(S)^n$ with $V \subseteq \mathcal{V}$, we define $\nu(\beta) : \biguplus_{i=1}^n \nu_i(V) \to \text{dom}(S)$ such that for all $x \in V$:

$$ \nu(\beta)(\nu_i(x)) = \pi_i(\beta(x)) $$

Function $\nu$ is a bijection with range $\{\alpha | \alpha : \biguplus_{i=1}^n \nu_i(V) \to \text{dom}(S)\}$. The inverse of this function satisfies $\nu^{-1}(\alpha)(x) = (\alpha(\nu_1(x)), \dots, \alpha(\nu_n(x)))$ for all $\alpha$ in the range and all $x \in V$.

**Lemma 14.** For any expression $o \in \mathcal{O}_{\Sigma}^n$ and variable assignment $\beta : V \to \text{dom}(S)^n$ with $\mathcal{V}(o) \subseteq V \subseteq \mathcal{V}$ we have $\llbracket \tilde{\nu}(o) \rrbracket^{S, \nu(\beta)} = \llbracket o \rrbracket^{\beta, S}$.

*Proof sketch.* By induction on the structure of $\Sigma$-expressions $o \in \mathcal{O}_{\Sigma}^n$. $\square$

**Proposition 15.** For any $\psi \in \mathcal{F}_{\Sigma}^n$, $\Sigma$-structure $S$, and $n \ge 1$: $n\text{-sol}^S(\psi) = \nu^{-1}(\text{sol}^S(\tilde{\nu}(\psi)))$.

*Proof* We first prove the following claim is by induction on the structure of $\Sigma$-formulas in $\mathcal{F}_{\Sigma}^n$, where the base case follows from Lemma 14.

**Claim 16.** For any variable assignment $\beta : V \to \text{dom}(S)^n$ with $V \subseteq \mathcal{V}$ and formula $\psi \in \mathcal{F}_{\Sigma}^n$ we have $\llbracket \tilde{\nu}(\psi) \rrbracket^{S, \nu(\beta)} = \llbracket \psi \rrbracket^{\beta, S}$.

The proof of the claim is straightforward by induction on the structure of $\Sigma$-formulas in $\mathcal{F}_{\Sigma}^n$. Finally, the claim implies the proposition as follows:

$$ \begin{aligned} \beta \in n\text{-sol}^S(\psi) &\iff \nu(\beta) \in n\text{-sol}^S(\tilde{\nu}(\psi)) & \text{previous claim} \\ &\iff \nu^{-1}(\nu(\beta)) \in \nu^{-1}(n\text{-sol}^S(\tilde{\nu}(\psi))) \\ &\iff \beta \in \nu^{-1}(n\text{-sol}^S(\tilde{\nu}(\psi))) \end{aligned} $$

$\square$

### 7.5. Commutation Property

As above, we consider $n$ fresh variable generators $\nu_1, \dots, \nu_n$ and the operator $\nu^{-1}$ that maps object assignments of freshly generates variables to $n$-tuple assignments. We next show a commutation property of the operator $\nu^{-1}$ with $\Sigma$-abstractions.

**Lemma 17.** For any $\Sigma$-abstraction $h : S \to \Delta$ and assignment of fresh variables $\alpha : \biguplus_{i=1}^n \nu_i(V) \to \text{dom}(S)$:

$$ \nu^{-1}(h \circ \alpha) = h^n \circ \nu^{-1}(\alpha) $$
**Proof** For any variable $x \in V$ we have:

$$ 
\begin{align*}
\nu^{-1}(h \circ \alpha)(x) &= (h(\alpha(\nu_1(x))), \dots, h(\alpha(\nu_n(x)))) \\
&= h^n((\alpha(\nu_1(x))), \dots, \alpha(\nu_n(x))) \\
&= h^n(\nu^{-1}(\alpha)(x)) \\
&= (h^n \circ \nu^{-1}(\alpha))(x)
\end{align*}
$$

□

**Proposition 18.** For any finite set $V \subseteq \mathcal{V}$, subset $R$ of variable assignments of type $\cup_{i=1}^n \nu_i(V) \to \text{dom}(S)$, and $\Sigma$-abstraction $h : S \to \Delta$:

$$ \nu^{-1}(h \circ R) = h^n \circ \nu^{-1}(R) $$

**Proof** By Lemma 17: $\nu^{-1}(h \circ R) = \{\nu^{-1}(h(\alpha)) | \alpha \in R\} = \{h^n(\nu^{-1}(\alpha)) | \alpha \in R\} = h^n \circ \nu^{-1}(R)$.

□

## 8. Difference Abstraction

We next recast the notions of difference abstractions from [8, 10, 9] by applying our notion of $\Sigma$-abstractions to concrete difference in the $\Sigma$-algebra $\mathbb{R}_+^2$, where $\Sigma = F_{\text{pos-arith}}^{(2)} \cup C_{\text{pos-arith}}$.

More generally, let $S$ be a $\Sigma$-algebra, such as the algebra $\mathbb{R}_+^2$ of concrete differences, and $V \subseteq \mathcal{V}$ a subset of variables. For any two variable assignments $\alpha, \alpha' : V \to \text{dom}(S)$, we define an assignment of variables to pairs of elements in the domain of the structure

$$ \text{diff}(\alpha, \alpha') : V \to \text{dom}(S)^2 $$

that we call the differences of $\alpha$ and $\alpha'$, such that for all variables $x \in V$, $\text{diff}(\alpha, \alpha')(x) = (\alpha(x), \alpha'(x))$. For any subset $R$ of variable assignments of type $V \to \text{dom}(S)$ we define the set of differences of assignments in $R$ by:

$$ \text{diff}(R) = \{\text{diff}(\alpha, \alpha') | \alpha, \alpha' \in R\} $$

**Definition 19.** For any $\Sigma$-abstraction $h : S^2 \to \Delta$ and formula $\phi \in \mathcal{F}_{\Sigma}$ we define the difference abstraction of the $S$-solution set of $\phi$ by: $\text{sol}^S(\phi)^{\Delta} = h \circ \text{diff}(\text{sol}^S(\phi))$.

The original definition of $\text{sol}(\phi)^{\Delta_6}$ in [8] was similar, but did not make the respective roles of $\text{diff}$ and $h_{\Delta_6} : \mathbb{R}_+^2 \to \Delta_6$ explicit. By having done so, we can now state that the difference abstraction of the $\mathbb{R}_+$-solution sets of a formula is the $\mathbb{R}_+^2$-solution set of the same formula.

**Lemma 20.** For any formula $\phi \in \mathcal{F}_{\Sigma}$ and $\Sigma$-algebra $S$: $\text{diff}(\text{sol}^S(\phi)) = \text{sol}^{S^2}(\phi)$.

**Proof** For all $\alpha : \mathcal{V} \to \text{dom}(S), \alpha' : \mathcal{V} \to \text{dom}(S), \alpha, \alpha' \in \text{sol}^S(\phi)$ we can construct the variable assignment $\alpha'' : \mathcal{V} \to \text{dom}(S)^2$ with $\text{diff}(\alpha, \alpha') = (\alpha(x), \alpha'(x)) = \alpha''(x)$. So we have $\text{diff}(\text{sol}^S(\phi)) \subseteq \text{sol}^{S^2}(\phi)$.

Conversely, for all variable assignment $\alpha'' : \mathcal{V} \to \text{dom}(S)^2$, $\alpha'' \in \text{sol}^{S^2}(\phi)$ we can generate two variable assignments $\alpha : \mathcal{V} \to \text{dom}(S), \alpha' : \mathcal{V} \to \text{dom}(S) \in \text{sol}^S(\phi)$ with $\forall x \in \mathcal{V}, \alpha(x) = \pi_1(\alpha''(x)) \land \alpha'(x) = \pi_2(\alpha''(x))$. So we have $\text{sol}^{S^2}(\phi) \subseteq \text{diff}(\text{sol}^S(\phi))$, and thus finally $\text{diff}(\text{sol}^S(\phi)) = \text{sol}^{S^2}(\phi)$. □

As an immediate consequence, we have for any $\Sigma$-abstraction $h : S^2 \to \Delta$ that $\text{sol}(\phi)^{\Delta} = h \circ \text{sol}^{S^2}(\phi)$. Our next objective is to show that we can overapproximate the set $\text{sol}(\phi)^{\Delta}$ by $\text{sol}^{\Delta}(\phi)$ (Corollary 24).
**Lemma 21.** Let $h: S' \to \Delta$ be a $\Sigma$-abstraction and $\alpha: V \to \text{dom}(S')$ and a variable assignment. For any expression $e \in \mathcal{E}_\Sigma$ with $V(e) \subseteq V: h(\llbracket e \rrbracket^{S',\alpha}) \subseteq \llbracket e \rrbracket^{\Delta, h \circ \alpha}$.

*Proof sketch.* Straightforward by induction on the structure of expressions $e \in \mathcal{E}_\Sigma$. $\square$

**Proposition 22.** Let $h: S' \to \Delta$ be a $\Sigma$-abstraction and $\alpha: V \to \text{dom}(S')$ and a variable assignment. For any positive formula $\phi \in \mathcal{F}_\Sigma$ with $V(\phi) \subseteq V: \llbracket \phi \rrbracket^{S',\alpha} \le \llbracket \phi \rrbracket^{\Delta, h \circ \alpha}$.

*Proof.* The proof is by induction on the structure positive $\Sigma$-formulas $\phi$. If $\phi$ is some equation $e \equiv e'$ then it holds by Lemma 21 that: $h(\llbracket e \rrbracket^{S',\alpha}) \subseteq \llbracket e \rrbracket^{\Delta, h \circ \alpha}$ and $h(\llbracket e' \rrbracket^{S',\alpha}) \subseteq \llbracket e' \rrbracket^{\Delta, h \circ \alpha}$. Hence:

$$ \begin{align*} \llbracket e \doteq e' \rrbracket^{S',\alpha} = 1 &\Leftrightarrow \llbracket e \rrbracket^{S',\alpha} \cap \llbracket e' \rrbracket^{S',\alpha} \neq \emptyset \\ &\Leftrightarrow h(\llbracket e \rrbracket^{S',\alpha}) \cap h(\llbracket e' \rrbracket^{S',\alpha}) \neq \emptyset \\ &\Rightarrow \llbracket e \rrbracket^{\Delta, h \circ \alpha} \cap \llbracket e' \rrbracket^{\Delta, h \circ \alpha} \neq \emptyset \quad \text{Lemma 21} \\ &\Leftrightarrow \llbracket e \doteq e' \rrbracket^{\Delta, h \circ \alpha} = 1 \end{align*} $$

This shows that $\llbracket e \doteq e' \rrbracket^{S',\alpha} \le \llbracket e \doteq e' \rrbracket^{\Delta, h \circ \alpha}$ as required. We next consider the case where $\phi$ is a conjunction of the form $\phi' \wedge \phi''$.

$$ \begin{align*} \llbracket \phi' \wedge \phi'' \rrbracket^{S',\alpha} &= \llbracket \phi' \rrbracket^{S',\alpha} \wedge \llbracket \phi'' \rrbracket^{S',\alpha} \\ &\le \llbracket \phi' \rrbracket^{\Delta, h \circ \alpha} \wedge \llbracket \phi'' \rrbracket^{\Delta, h \circ \alpha} \quad \text{induction hypothesis} \\ &= \llbracket \phi' \wedge \phi'' \rrbracket^{\Delta, h \circ \alpha} \end{align*} $$

The last case is where $\phi$ is an existentially quantified formula of the form $\exists x. \phi'$.

$$ \begin{align*} \llbracket \exists x. \phi' \rrbracket^{S',\alpha} = 1 &\Leftrightarrow (\text{exists } s \in \text{dom}(S'). \llbracket \phi' \rrbracket^{\alpha[x/s],S'}) = 1 \\ &\Rightarrow (\text{exists } s \in \text{dom}(S'). \llbracket \phi' \rrbracket^{h \circ \alpha[x/s],\Delta}) = 1 \quad \text{induction hypothesis} \\ &\Leftrightarrow \llbracket \exists x. \phi' \rrbracket^{\Delta, h \circ \alpha} = 1 \end{align*} $$

This shows that $\llbracket \exists x. \phi' \rrbracket^{S',\alpha} \le \llbracket \exists x. \phi' \rrbracket^{\Delta, h \circ \alpha}$ as required. $\square$

**Theorem 23.** Let $h: S' \to \Delta$ be a $\Sigma$-abstraction and $\alpha: V \to \text{dom}(S')$ and a variable assignment. For any positive formula $\phi \in \mathcal{F}_\Sigma$ with $V(\phi) \subseteq V$:

$$ h \circ \text{sol}^{S'}(\phi) \subseteq \text{sol}^{\Delta}(\phi) $$

*Proof.* Let $h$ be $\Sigma$-abstraction from $S'$ to $\Delta$ and $\phi \in \mathcal{F}_\Sigma$ a positive formula. For any variable assignment $\alpha$ to $\text{dom}(S')$, we know that $\llbracket \phi \rrbracket^{S',\alpha} \le \llbracket \phi \rrbracket^{\Delta, h \circ \alpha}$ by Proposition 22 since $\phi$ is positive. This is equivalent to $\{h \circ \alpha | \alpha \in \text{sol}^{S'}(\phi)\} \subseteq \text{sol}^{\Delta}(\phi)$ and thus $h \circ \text{sol}^{S'}(\phi) \subseteq \text{sol}^{\Delta}(\phi)$ as required. $\square$

**Corollary 24 (John's Theorem [8, 10]).** For any $\Sigma$-abstraction $h: S^2 \to \Delta$ and positive first-order formula $\phi \in \mathcal{F}_\Sigma$:

$$ \text{sol}^{S}(\phi)^{\Delta} \subseteq \text{sol}^{\Delta}(\phi) $$

*Proof.* With the $\Sigma$-structure $S' = S^2$, this follows from Lemma 20 and Theorem 23.

$$ \text{sol}^{S}(\phi)^{\Delta} = h \circ \text{diff}(\text{sol}^{S}(\phi)) = h \circ \text{sol}^{S^2}(\phi) \subseteq \text{sol}^{\Delta}(\phi) $$

If $\Delta$ is finite then the set $\text{sol}^{\Delta}(\phi)$ is finite, while $\text{sol}^{\mathbb{R}+}(\phi)$ is usually infinite. If furthermore $\phi$ is a conjunctive formula, we can compute the set $\text{sol}^{\Delta}(\phi)$ by a finite domain constraint solver
from $\phi$ and the tables of $\Delta$ (such as e.g. Minizinc [12]). In contrast, it remains unclear how to compute the finite set $h \circ \text{diff}(\text{sol}^S(\phi))$ for infinite structures $S$. The problem is open, even if $\phi$ is a system of homogeneous linear equations and $S = \mathbb{R}_+$, so that the infinite set $\text{sol}^S(\phi)$ can be finitely represented by a triangular matrix.

This is the core of the problem that we will solve in the present paper. Our approach will be to rewrite formulas $\phi$ to $\mathbb{R}_+$-equivalent formulas that are $h$-exact in the following sense:

**Definition 25.** Let $h: S \to \Delta$ be a $\Sigma$-abstraction. We call a $\Sigma$-formula $\phi$ $h$-exact if:

$$h(\text{sol}^S(\phi)) = \text{sol}^\Delta(\phi).$$

For $h$-exact formulas $\phi$, $h(\text{sol}_V^S(\phi))$ can be computed exactly by computing $\text{sol}_V^\Delta(\phi)$ as described above.

## 9. Exact Boolean Abstraction

We recall a recent result from [15] that permits to characterize the boolean abstraction of the $\mathbb{R}_+$-solution set of a mixed linear and nonlinear systems by some $h_{\mathbb{B}}$-exact and $\mathbb{B}$-equivalent formula, so that the boolean abstraction can be computed exactly by finite domain constraint programming.

The development of this result was motivated by the needs of the present paper, but was presented independently for two reasons. First, these results require considerable effort with complementary techniques based on elementary modes, and second, they are of interest elsewhere, in particular for computing the sign abstraction as needed for the abstract interpretation of programming languages.

A linear equation with natural coefficients and no constant term is a formula of $\mathcal{F}_\Sigma$ with the arithmetic signature $\Sigma = F_{\text{pos-arith}}^{(2)} \uplus C_{\text{pos-arith}}$ of the form:

$$n_1x_1 + \dots + n_mx_m = n_{m+1}x_{m+1} + \dots + n_px_p$$

where $m, p, n_1, \dots, n_p \in \mathbb{N}$ and $x_1, \dots, x_p \in \mathcal{V}$. An equation $e = e'$ is positive if the right-hand side $e'$ is equal to 0. It is called quasi-positive if it is positive or the right-hand side has the form $nx$ for some natural $n$ and some variable $x$. A system of equations is a conjunction of equations.

**Proposition 26 (Elementary Modes Theorem 15 of [15]).** For any system of linear equations $L$ of size $n$ with $m$ variables we can compute in time $O(2^m \text{poly}(n))$ an $\mathbb{R}_+$-equivalent formula of the form $\exists x. L'$ of size $O(n + m2^m)$ such that $L'$ is a system of quasi-positive linear equations, in which all variables on the left hand-side belong to $x$ and all variables on the right-hand side occur exactly once.

*Proof sketch.* An $\mathbb{R}_+$-EFM of $\phi$ is a variable assignment in $\alpha \in \text{sol}^{\mathbb{R}_+}(\phi)$ with a minimal support, i.e. with a minimal number of variables $x$ such that $\alpha(x) \neq 0$. It is also well-known that the set of all $\mathbb{R}_+$-EFM of $\phi$ can be computed in $O(2^m \text{poly}(n))$ from $\phi$ by using for example the reverse search method for the enumeration of polytope vertices and extreme rays [25]. Furthermore, any solution in $\text{sol}^{\mathbb{R}_+}(\phi)$ is equal to a positive linear combination of $\mathbb{R}_+$-EFM of $\phi$. This can be expressed by an $\mathbb{R}_+$-equivalent formula $\exists x. \phi'$ such that $\phi'$ is a system of quasi-positive equations, in which all variables on some left-hand side belong to $x$ and all variables on some right-hand side occur exactly once. $\square$

**Definition 27.** Consider the signature of arithmetics $\Sigma = F_{\text{pos-arith}}^{(2)} \uplus C_{\text{pos-arith}}$. A product-zero-equation in $\mathcal{F}_\Sigma$ is a positive polynomial equation of the form $z * z' = 0$ where $z, z' \in \mathcal{V}$. A (simple) $h_{\mathbb{B}}$-mixed system is a conjunctive formula in $\mathcal{F}_\Sigma$ of the form $\exists z. L \wedge P$ where $L$ is a system of linear equations and $P$ a system of product-zero-equations.
Note that $h_{\mathbb{B}}$-mixed systems may contain non-positive equations in the linear part $L$ and non-linear equations in the positive part $P$. We could also consider more general $h_{\mathbb{B}}$-mixed systems in which $P$ may be any system of polynomial equations without constant terms, but this will not be needed in the present paper.

**Theorem 28 (Theorem 39 of [15]).** For any $h_{\mathbb{B}}$-mixed system $\phi$ of size $n$ with $m$ variables we can compute in $O(2^m \text{poly}(n))$ time an $h_{\mathbb{B}}$-exact formula $\phi'$ of size $O(n + m2^m)$ that is $\mathbb{R}_+$-equivalent to $\phi$.

*Proof sketch.* Consider a $h_{\mathbb{B}}$-mixed system $\phi = \exists \mathbf{z}. (L \wedge P)$. We can then replace $L$ by the $\mathbb{R}_+$-equivalent formula $\exists \mathbf{x}. L'$ from Proposition 26. Since $L'$ is quasi-positive, the variables on the right hand-side of some equation in $L'$ occur exactly once, and the variables on the left-hand sides belong to $\mathbf{x}$, and $P$ is restricted, it can be shown with considerable effort, that the formula $\exists \mathbf{z}. ((\exists \mathbf{x}. L') \wedge P)$ is indeed $h_{\mathbb{B}}$-exact. So we can chose $\phi'$ equal to this formula. $\square$

In order to compute the $h_{\mathbb{B}}$-abstraction of a $h_{\mathbb{B}}$-mixed system $\phi$ exactly, we first compute $\phi'$ along the lines of the sketch of the proof ideas of Theorem 28 and Proposition 26. We can then compute $\text{sol}_{\mathbb{B}}(\phi')$ by finite domain constraint programming.

# 10. Characterizing Difference Abstractions

We next show how to characterize the difference abstractions to $\Delta_3$ and $\Delta_6$ of the solution set of a linear equation system by the solution set of some first-order formulas interpreted over the finite structure $\mathbb{B}$. We do not know how to find exact equivalent formulas as provided by in Theorem 28 in the case of boolean abstraction. Instead, we will use this theorem to find a finitary characterisation of also in the case of difference abstractions. Hereby, we will strongly rely on properties of definition in the first-order tuple logic, so we introduce the first.

## 10.1. First-Order Definitions

Our strategy for computing difference abstractions to $\Delta_3$ and $\Delta_6$ will be to decompose those into the $\mathbb{B}$-abstraction and first-order definable functions. Therefore, we define next what it means for function or relation to be defined by a formula of first-order tuple logic.

**Definition 29.** A $\mathcal{F}_{\Sigma}^n$-definition of arity $m$ is a function $F: \mathcal{V}^m \to \mathcal{F}_{\Sigma}^n$ for which there exists a formula $\psi \in \mathcal{F}_{\Sigma}^n$ and a sequence of distinct variables $\mathbf{x} \in \mathcal{V}^m$ such that $\mathcal{V}(\psi) = \{\mathbf{x}\}$ and $F(\mathbf{y}) = \psi[\mathbf{x}/\mathbf{y}]$ for all $\mathbf{y} \in \mathcal{V}^m$. For any $\Sigma$-structure $S$, $F$ defines the following $m$-ary relation $F^{S^n}$ on $\text{dom}(S)^n$:

$$F^{S^n} = \{(\alpha(\pi_1(\mathbf{x})), \dots, \alpha(\pi_m(\mathbf{x}))) \mid \alpha \in \text{n-sol}^S(\psi)\}$$

The formula $F(\mathbf{y})$ states that the values of $\mathbf{y}$ are in the relation defined by the formula $\psi$. Which precise sequence $\mathbf{y}$ of distinct variables is chosen, does not matter since $F(\mathbf{y}) = F(\mathbf{x})[\mathbf{x}/\mathbf{y}]$, since the solutions of $F(\mathbf{y})$ and $F(\mathbf{x})$ over structure $S$ correspond to each other modulo renaming of variable

**Lemma 30.** For any first-order definition $F: \mathcal{V}^m \to \mathcal{F}_{\Sigma}^n$ and sequence $\mathbf{y} = y_1 \dots y_m$ of distinct variables:

$$\text{n-sol}^S(F(\mathbf{y})) = \{[y_1/s_1, \dots, y_m/s_m] \mid (s_1, \dots, s_m) \in F^{S^n}\}.$$

**Proof** This is straightforward.
<figure><img src="image_12.png" /><figcaption>Figure 15: Two examples for the minimal support projection: $y_1 = msp_{\mathbb{R}_+^2}(x_1)$ and $y_2 = msp_{\mathbb{R}_+^2}(x_2)$.</figcaption></figure>

## 10.2. Defining Function Application

We will frequently have to apply functions to relations defined in first-order tuple logic. Let $S$ be the structure of interest. In the simplest case, we are given a FO-definition $F: \mathcal{V}^2 \to \mathcal{F}_{\Sigma}^n$ that defines a total function $F^{S^n}: \text{dom}(S^n) \to \text{dom}(S^n)$, and a first-order definition $G: \mathcal{V}^m \to \mathcal{F}_{\Sigma}^n$ that defines an $m$-ary relation $G^S$ on $\text{dom}(S)^n$. We can then define the application of $F^S$ to all $m$ components $G^S$ by the first-order definition $F^m(G)$ such that for all $\mathbf{y} = y_1 \dots y_m$:

$$F^m(G)(\mathbf{y}) =_{\text{def}} \exists \mathbf{z}. G(\mathbf{z}) \wedge \bigwedge_{i=1}^m F(z_i, y_i)$$

where $\mathbf{z} = z_1 \dots z_m$ are fresh variables. A more general definition where $F^S: \text{dom}(S^n)^k \to \text{dom}(S^n)^l$ will be needed later on. It will be given in Section 10.1 together with formal properties of such first-order definitions.

## 10.3. Exact $\Delta_3$-Abstraction of Linear Systems

We start with the abstraction of $\Delta_3$. We first decompose the abstraction $h_{\Delta_3}$ into the boolean abstraction $h_{\mathbb{B}}$ and the minimal support projection in $\mathbb{R}_+^2$ defined by the following $h_{\mathbb{B}}$-mixed system in $\mathcal{F}_{\Sigma}^2$, containing a non-positive linear equation and a product-zero equation, that is non-linear but positive. For any two variables $x, y \in \mathcal{V}$ we define:

$$msp(x, y) =_{\text{def}} \dot{\pi}_1(x) + \dot{\pi}_2(y) \doteq \dot{\pi}_2(x) + \dot{\pi}_1(y) \wedge \dot{\pi}_1(y) * \dot{\pi}_2(y) \doteq 0$$

The function $msp_{\mathbb{R}_+^2}$ serves for minimal support projection, as illustrated geometrically in Figure 15. The value of $msp_{\mathbb{R}_+^2}(z)$ is the intersection point of the parallel of the diagonal through $z$ with either the $x$-axis or else the $y$-axis. For any solution $\alpha \in \text{sol}_{\mathbb{R}_+^2}(msp(x, y))$, some component of $\alpha(y)$ must be equal to zero since $\pi_1(\alpha(y)) * \pi_2(\alpha(y)) = 0$. The other component must be equal to $|\pi_1(\alpha(x)) - \pi_2(\alpha(x))|$ since $\pi_1(\alpha(x)) - \pi_2(\alpha(x)) = \pi_1(\alpha(y)) - \pi_2(\alpha(y))$. Hence:

$$msp_{\mathbb{R}_+^2} = \{((r, r'), (0, r' - r)) \mid r \le r'\} \\ \cup \{((r, r'), (r - r', 0)) \mid r \ge r'\}$$

**Lemma 31.** $msp_{\mathbb{R}_+^2}$ is a total function of type $\mathbb{R}_+^2 \to \mathbb{R}_+^2$ satisfying $h_{\Delta_3} = h_{\mathbb{B}}^2 \circ msp_{\mathbb{R}_+^2}$.

*Proof* By definition $msp_{\mathbb{R}_+^2}$ is a binary relation on $\mathbb{R}_+^2$. This binary relation is a total function satisfying the equation from the lemma due to the equation before the lemma. $\square$
For any first-order definition $G: \mathcal{V}^m \to \mathcal{F}_\Sigma^2$ we defined in Section 10.1 a first-order definition $msp^m(G) : \mathcal{V}^m \to \mathcal{F}_\Sigma^2$ that describes the application of function defined by $msp$ to the $m$ components of the relation defined by $G$.

**Lemma 32.** For any first-order definition $G: \mathcal{V}^m \to \mathcal{F}_\Sigma^2$ and sequence $\mathbf{y} \in \mathcal{V}^m$:

$$ msp^{\mathbb{R}_+^2} \circ 2\text{-sol}^{\mathbb{R}_+}(G(\mathbf{y})) = 2\text{-sol}^{\mathbb{R}_+}(msp^m(G)(\mathbf{y})) $$

**Proof** This lemma is a consequence of the fact that $msp^{\mathbb{R}_+^2}$ defines a total function by Lemma 31 and a general property of first-order definitions that will be state in Proposition 47 of Section 14. We could have given it directly after the section on the first-order tuple logic, but prefered to do it only at the end, when the full generality of such result needed in this paper has become clear. As parameters for the application of Proposition 47 we choose $F = msp: \mathcal{V}^2 \to \mathcal{F}_\Sigma^2$, $\ell = 1$, $k = 1, n = 2$. $\square$

We fix two fresh variable generators $\nu_1, \nu_2: \mathcal{V} \to \mathcal{V}$ and define $\nu(x)$ and $\nu^{-1}(x)$ as before.

**Theorem 33.** For any any linear formula $L(\mathbf{y}) \in \mathcal{F}_\Sigma$ with $m$ free variables $\{\mathbf{y}\}$ and size $n$ we can compute in time in time $O(2^{2m}\text{poly}(n))$ a positive conjunctive formula with existential quantifiers $\phi(\nu(\mathbf{y})) \in \mathcal{F}_\Sigma$ with free variables $\{\nu(\mathbf{y})\}$ and of size $O(n + m2^{2m})$ such that:

$$ h_{\Delta_3} \circ \text{diff}(\text{sol}^{\mathbb{R}_+}(L(\mathbf{y}))) = \nu^{-1}(\text{sol}^{\mathbb{B}}(\phi(\nu(\mathbf{y})))) $$

**Proof** Let $L: \mathcal{V}^m \to \mathcal{F}_\Sigma$ be the first-order definition which when applied to $\mathbf{y}$ returns the linear formula $L(\mathbf{y})$.

$$
\begin{array}{l@{\qquad}l}
\textit{Proposition 20} & h_{\Delta_3} \circ \text{diff}(\text{sol}^{\mathbb{R}_+}(L(\mathbf{y}))) \\
\textit{Pair FO Proposition 12} & = h_{\Delta_3} \circ \text{sol}^{\mathbb{R}_+^2}(L(\mathbf{y})) \\
\textit{Decomposition Lemma 31} & = h_{\mathbb{B}}^2 \circ msp^{\mathbb{R}_+^2} \circ 2\text{-sol}^{\mathbb{R}_+}(L_2(\mathbf{y})) \text{ with } L_2(\mathbf{y}) = \langle L(\mathbf{y}) \rangle^2 \\
\textit{FO-Definition Lemma 32} & = h_{\mathbb{B}}^2 \circ 2\text{-sol}^{\mathbb{R}_+}(msp^m(L_2)(\mathbf{y})) \\
\textit{Proposition 15} & = h_{\mathbb{B}}^2 \circ \nu^{-1}(\text{sol}^{\mathbb{R}_+}(\tilde{\nu}(msp^m(L_2)(\mathbf{y})))) \\
\textit{Proposition 18} & = \nu^{-1}(h_{\mathbb{B}} \circ \text{sol}^{\mathbb{R}_+}(\tilde{\nu}(msp^m(L_2)(\mathbf{y})))) \\
\textit{Definition of msp}^m(L_2(\mathbf{y})) & = \nu^{-1}(h_{\mathbb{B}} \circ \text{sol}^{\mathbb{R}_+}(\tilde{\nu}(\exists \mathbf{z}. L_2(\mathbf{z}) \wedge \bigwedge_{i=1}^m msp(z_i, y_i)))) \\
& \text{where } \mathbf{z} = z_1 \dots z_m \text{ fresh} \\
h_{\mathbb{B}}\text{-Mixed systems Theorem 28} & = \nu^{-1}(\text{sol}^{\mathbb{B}}(\phi(\nu(\mathbf{y})))) \text{ where } \phi(\nu(\mathbf{y})) \text{ is a conjunctive} \\
& \text{formula that is } h_{\mathbb{B}}\text{-exact and } \mathbb{R}_+\text{-equivalent to} \\
& \text{the } h_{\mathbb{B}}\text{-mixed system } \tilde{\nu}(\exists \mathbf{z}. L_2(\mathbf{z}) \wedge \bigwedge_{i=1}^m msp(z_i, y_i)) \qquad \square
\end{array}
$$

By the $h_{\mathbb{B}}$-mixed systems Theorem 28, the size of $\phi(\nu(\mathbf{y}))$ is in $O(n + m2^{2m})$ and the time of its computation in $O(2^{2m}\text{poly}(n))$. $\square$

This theorem induces a new algorithm for the exact computation of $h_{\Delta_3} \circ \text{diff}(\text{sol}^{\mathbb{R}_+}(L(\mathbf{y})))$ in time $O(\text{poly}(n)2^{8m})$ where $n$ is the size of $L(\mathbf{y})$ and $m$ the number of variables in $\mathbf{y}$. Note that this upper bound is simply exponential in the worst case, such as the alternative algorithm sketched in Section 2.

The new algorithm applies Theorem 37 in order to create the formula $\phi(\nu(\mathbf{y}))$ in time $O(2^{2m}\text{poly}(n))$. This formula has size $O(n + m2^{2m})$ and $2m$ variables $\nu(\mathbf{y})$. The set of solutions $\text{sol}^{\mathbb{B}}(\phi(\nu(\mu(\mathbf{y}))))$ can then be computed by a naive generate and test algorithm in time $O(2^{2m}(n + m2^{2m}))$: Given that this set is of cardinality at most $2^{2m}$, we can compute $h_{\Delta_6} \circ \text{diff}(\text{sol}^{\mathbb{R}_+}(L(\mathbf{y})))$ from $\text{sol}^{\mathbb{B}}(\phi(\nu(\mathbf{y})))$ in time $2^{2m}$ by using the equality of the theorem. The overall time for computing $h_{\Delta_3} \circ \text{diff}(\text{sol}^{\mathbb{R}_+}(L(\mathbf{y})))$ is in $O(\text{poly}(n)2^{2m} + m2^{4m})$ and thus in $O(\text{poly}(n)2^{4m})$. In practice, we can improve this algorithm by computing the set boolean solutions of $\phi(\nu(\mathbf{y}))$ by finite domain constraint programming, rather than by a naive generate and test algorithm.
### 10.4. Exact $\Delta_6$-Abstraction of Linear Systems

The case of $\Delta_6$ following the same approach that for $\Delta_3$, but is considerably more evolved in the usage of first-order definitions.

We consider the abstraction $h_{\Delta_6}$ as an element of the $\Sigma$-algebra of total functions of type $\mathbb{R}_+^2 \to \mathbb{R}_+^2$, where $\Sigma = F_{\text{pos-arith}}^{(2)} \uplus C_{\text{pos-arith}}$. For any two functions $f, f' : \mathbb{R}_+^2 \to \mathbb{R}_+^2$, the addition is defined by $f + \mathbb{R}_+^2 \to \mathbb{R}_+^2 f'(p) = f(p) + \mathbb{R}_+^2 f'(p)$ for every $p \in \mathbb{R}_+^2$, and similarly the multiplication is by $f * \mathbb{R}_+^2 \to \mathbb{R}_+^2 f'(p) = f(p) * \mathbb{R}_+^2 f'(p)$. The following lemma shows that $h_{\Delta_6}$ is the sum of $h_{\Delta_3}$ and $h_{\mathbb{B}}^2$ in this $\Sigma$-algebra.

**Lemma 34.** $h_{\Delta_6} = h_{\mathbb{B}}^2 + h_{\Delta_3}$ where $\dagger = + \mathbb{R}_+^2 \to \mathbb{R}_+^2$

**Proof** Let $p = (r, r') \in \mathbb{R}_+^2$. We distinguish the cases for all possible values for $h_{\Delta_6}(p) \in \Delta_6$.

**Case** $h_{\Delta_6}(p) = \uparrow$. Then $0 < r < r'$ so that $h_{\mathbb{B}}^2(p) = (1, 1)$ and $h_{\Delta_3}(p) = \triangle = (0, 1)$. It follows that $(h_{\mathbb{B}}^2 + h_{\Delta_3})(p) = (1, 2) = \uparrow = h_{\Delta_6}(p)$.

**Case** $h_{\Delta_6}(p) = \Uparrow$. Then $0 = r < r'$ so that $h_{\mathbb{B}}^2(p) = (0, 1)$ and $h_{\Delta_3}(p) = \triangle = (0, 1)$. It follows that $(h_{\mathbb{B}}^2 + h_{\Delta_3})(p) = (0, 2) = \Uparrow = h_{\Delta_6}(p)$.

**Case** $h_{\Delta_6}(p) = \downarrow$. Then $0 < r' < r$ so that $h_{\mathbb{B}}^2(p) = (1, 1)$ and $h_{\Delta_3}(p) = \triangledown = (1, 0)$. It follows that $(h_{\mathbb{B}}^2 + h_{\Delta_3})(p) = (2, 1) = \downarrow = h_{\Delta_6}(p)$.

**Case** $h_{\Delta_6}(p) = \Downarrow$. Then $0 = r' < r$ so that $h_{\mathbb{B}}^2(p) = (1, 0)$ and $h_{\Delta_3}(p) = \triangledown = (1, 0)$. It follows that $(h_{\mathbb{B}}^2 + h_{\Delta_3})(p) = (2, 0) = \Downarrow = h_{\Delta_6}(p)$.

**Case** $h_{\Delta_6}(p) = \sim$. Then $0 < r = r'$ so that $h_{\mathbb{B}}^2(p) = (1, 1)$ and $h_{\Delta_3}(p) = \approx = (0, 0)$. It follows that $(h_{\mathbb{B}}^2 + h_{\Delta_3})(p) = (1, 1) = \sim = h_{\Delta_6}(p)$.

**Case** $h_{\Delta_6}(p) = \approx$. Then $0 = r = r'$ so that $h_{\mathbb{B}}^2(p) = (0, 0)$ and $h_{\Delta_3}(p) = \approx = (0, 0)$. It follows that $(h_{\mathbb{B}}^2 + h_{\Delta_3})(p) = (0, 0) = \approx = h_{\Delta_6}(p)$.

Let $\text{id-msp}^{\mathbb{R}_+^2} : \mathbb{R}_+^2 \to (\mathbb{R}_+^2)^2$ such that for any $p \in \mathbb{R}_+^2$ $\text{id-msp}^{\mathbb{R}_+^2}(p) = (p, \text{msp}^{\mathbb{R}_+^2}(p))$. Furthermore, we define for any two functions $g : A \to B \times C$ and $f : B \times C \to D$ the pseudo composition $f \bullet g : A \to D$ such that for all $a \in A$: $(f \bullet g)(a) = f(\pi_1(g(a)), \pi_2(g(a)))$. The $\Sigma$-abstraction $h_{\mathbb{B}}^2 : \mathbb{R}_+^2 \to \mathbb{B}^2$ allows us to define $(h_{\mathbb{B}}^2)^2 : (\mathbb{R}_+^2)^2 \to (\mathbb{B}^2)^2$

**Lemma 35 Decomposition.** $h_{\Delta_6} = + \mathbb{R}_+^2 \bullet (h_{\mathbb{B}}^2)^2 \circ \text{id-msp}^{\mathbb{R}_+^2}$.

**Proof** For any $p \in \mathbb{R}_+^2$, we have:

$$ 
\begin{align*}
h_{\Delta_6}(p) &= h_{\mathbb{B}}^2(p) + \mathbb{R}_+^2 h_{\mathbb{B}}^2(\text{msp}^{\mathbb{R}_+^2}(p)) \\
&= + \mathbb{R}_+^2(h_{\mathbb{B}}^2(p), h_{\mathbb{B}}^2(\text{msp}^{\mathbb{R}_+^2}(p))) \\
&= + \mathbb{R}_+^2((h_{\mathbb{B}}^2)^2(p, \text{msp}^{\mathbb{R}_+^2}(p))) \\
&= + \mathbb{R}_+^2((h_{\mathbb{B}}^2)^2(\text{id}(p), \text{msp}^{\mathbb{R}_+^2}(p))) \\
&= + \mathbb{R}_+^2 \bullet (h_{\mathbb{B}}^2)^2 \circ \text{id-msp}^{\mathbb{R}_+^2}(p)
\end{align*}
$$

We can define the ternary relation $\text{id-msp}^{\mathbb{R}_+^2} : \mathbb{R}_+^2 \to \mathbb{R}_+^2 \times \mathbb{R}_+^2$ in the first-order pair logic by $\text{id-msp} : \mathcal{V} \times \mathcal{V}^2 \to \mathcal{F}_{\Sigma}^2$ such that for all $x, y_1, y_2 \in \mathcal{V}$:

$$ \text{id-msp}(x, y_1, y_2) =_{\text{def}} \langle x = y_1 \rangle^2 \wedge \text{msp}(x, y_2) $$
We next define applications of function defined by id-msp in the first-order logic. In order to deal with the two output arguments, we use two generators of fresh variables $\mu_1, \mu_2 : \mathcal{V} \to \mathcal{V}$. For any first-order definition $G : \mathcal{V}^m \to \mathcal{F}_{\Sigma}^2$ we define a first-order definition $\text{id-msp}_{\mu}^m(G) : \mathcal{V}^{2m} \to \mathcal{F}_{\Sigma}^2$, such that for any sequence of variables $\mathbf{y} \in \mathcal{V}^m$ and with $\mu(\mathbf{y}) = \mu_1(\mathbf{y})\mu_2(\mathbf{y})$:

$$ \text{id-msp}_{\mu}^m(G)(\mu(\mathbf{y})) =_{\text{def}} \exists \mathbf{y}. G(\mathbf{y}) \wedge \bigwedge_{i=1}^m \text{id-msp}(y_i, \mu_1(y_i), \mu_2(y_i)) $$

**Lemma 36.** $\text{id-msp}_{\mathbb{R}_+}^2 \circ 2\text{-sol}_{\mathbb{R}_+}(G(\mathbf{y})) = \left\{ \begin{array}{l} [\mathbf{y}/(\alpha(\mu_1(\mathbf{y})), \alpha(\mu_2(\mathbf{y}))) | \\ \qquad \alpha \in 2\text{-sol}_{\mathbb{R}_+}(\text{id-msp}_{\mu}^m(G)(\mu(\mathbf{y}))) \end{array} \right\}.$

**Proof** This lemma is consequence of the property of first-order definition in the FO-tuple logic that we will state in Proposition 49 of Section 14. Here we choose as parameters the first-order definition $F = \text{id-msp}_{\mu} : \mathcal{V} \times \mathcal{V}^2 \to \mathcal{F}_{\Sigma}^2$, and $\ell = 1, k = 2, n = 2$. $\square$

We continue with $\mu_1, \mu_2, \nu_1, \nu_2$ four generators of fresh variables from which we define $\mu$ and $\nu$ as before.

**Theorem 37.** For any linear formula $L(\mathbf{y})$ with $m$ free distinct variable $\mathbf{y}$ and size $n$ we can compute in time $O(2^{4m}\text{poly}(n))$ a positive conjunctive formula with existential quantifiers $\phi(\nu(\mu(\mathbf{y}))) \in \mathcal{F}_{\Sigma}$ with free variables in $\nu(\mu(\mathbf{y}))$ and of size $O(n + m2^{4m})$ such that:

$$ h_{\Delta_6} \circ \text{diff}(\text{sol}_{\mathbb{R}_+}^R(L(\mathbf{y}))) = \{[y/(\beta^2(\nu(\mu_1(y))) + \mathbb{R}_+^2 \beta^2(\nu(\mu_2(y)))) | y \in \{\mathbf{y}\} | \beta \in \text{sol}_{\mathbb{B}}^R(\phi(\nu(\mu(\mathbf{y}))))\} $$

**Proof** Let $L : \mathcal{V}^m \to \mathcal{F}_{\Sigma}$ be the first-order definition which when applied to $\mathbf{y}$ returns the linear formula $L(\mathbf{y})$.

$$ \begin{array}{rcl} & & h_{\Delta_6} \circ \text{diff}(\text{sol}_{\mathbb{R}_+}^R(L(\mathbf{y}))) \\ \textit{Proposition 20} & = & h_{\Delta_6} \circ \text{sol}_{\mathbb{R}_+}^R(L(\mathbf{y})) \\ \textit{Proposition 12} & = & h_{\Delta_6} \circ 2\text{-sol}_{\mathbb{R}_+}^R(L_2(\mathbf{y})) \text{ with } L_2(\mathbf{y}) = (\langle L(\mathbf{y}) \rangle)^2 \\ \textit{Dec. Lemma 35} & = & +_{\mathbb{R}_+}^2 \bullet (h_{\mathbb{B}}^2)^2 \circ \text{id-msp}_{\mathbb{R}_+}^2 \circ 2\text{-sol}_{\mathbb{R}_+}^R(L_2(\mathbf{y})) \\ \textit{FO Lemma 36} & = & +_{\mathbb{R}_+}^2 \bullet (h_{\mathbb{B}}^2)^2 \circ \{[\mathbf{y}/(\alpha(\mu_1(\mathbf{y})), \alpha(\mu_2(\mathbf{y}))) | \alpha \in 2\text{-sol}_{\mathbb{R}_+}^R(\text{id-msp}_{\mu}^m(L_2)(\mu(\mathbf{y}))) \\ & & \qquad = +_{\mathbb{R}_+}^{h_{\mathbb{B}}^2} \bullet \{[\mathbf{y}/(\beta(\mu_1(\mathbf{y})), \beta(\mu_2(\mathbf{y}))) | \beta \in h_{\mathbb{B}}^2 \circ 2\text{-sol}_{\mathbb{R}_+}^R(\text{id-msp}_{\mu}^m(L_2)(\mu(\mathbf{y}))) \\ & & \qquad = \{[\mathbf{y}/(\beta(\mu_1(\mathbf{y}))+\mathbb{R}_+^2 \beta(\mu_2(\mathbf{y}))) | \beta \in h_{\mathbb{B}}^2 \circ 2\text{-sol}_{\mathbb{R}_+}^R(\text{id-msp}_{\mu}^m(L_2)(\mu(\mathbf{y})))\} \end{array} $$

We can compute the $h_{\mathbb{B}}^2$ abstraction of the above solution set similarly to the case of $\Delta_3$.

$$ \begin{array}{rcl} & & h_{\mathbb{B}}^2 \circ 2\text{-sol}_{\mathbb{R}_+}^R(\text{id-msp}_{\mu}^m(L_2)(\mu(\mathbf{y}))) \\ \textit{Proposition 15} & = & h_{\mathbb{B}}^2 \circ \nu^{-1}(\text{sol}_{\mathbb{R}_+}^R(\tilde{\nu}(\text{id-msp}_{\mu}^m(L_2)(\mu(\mathbf{y})))) \\ \textit{Proposition 18} & = & \nu^{-1}(h_{\mathbb{B}} \circ \text{sol}_{\mathbb{R}_+}^R(\tilde{\nu}(\text{id-msp}_{\mu}^m(L_2)(\mu(\mathbf{y})))) \\ \textit{Def. of id-msp}_{\mu}^m & = & \nu^{-1}(h_{\mathbb{B}} \circ \text{sol}_{\mathbb{R}_+}^R(\tilde{\nu}(\exists \mathbf{y}. L_2(\mathbf{y}) \wedge \bigwedge_{i=1}^m \text{id-msp}(y_i, \mu_1(y_i), \mu_2(y_i)))) \\ \textit{Theorem 28} & = & \nu^{-1}(\text{sol}_{\mathbb{B}}^R(\phi(\nu(\mu(\mathbf{y})))) \\ \textit{on } h_{\mathbb{B}}\text{-mixed systems} & & \text{where } \phi(\nu(\mu(\mathbf{y}))) \text{ is a conjunctive formula equivalent to the } \\ & & \qquad h_{\mathbb{B}}\text{-mixed system } \tilde{\nu}(\exists \mathbf{y}. L_2(\mathbf{y}) \wedge \bigwedge_{i=1}^m \text{id-msp}(y_i, \mu_1(y_i), \mu_2(y_i))) \end{array} $$

The combination of the above two calculations and the moving of $\nu^{-1}$ to the left yields the equation stated in the theorem. By the $h_{\mathbb{B}}$-mixed systems Theorem 28, the size of $\phi(\nu(\mu(\mathbf{y})))$ is in $O(n + m2^{4m})$ and the time of its computation in $O(2^{4m}\text{poly}(n))$. $\square$

Note that upper complexity bound of Theorem 37 is slightly different to that of Theorem 33, since we have to create $4m$ variables for $\Delta_6$, in contrast to $2m$ variables for $\Delta_3$. Theorem
37 induces a new algorithm for the exact computation of $h_{\Delta_6} \circ \text{diff}(\text{sol}^{\mathbb{R}_+}(L(\mathbf{y})))$. It requires time in $O(\text{poly}(n)2^{8m})$ where $n$ is the size of $L(\mathbf{y})$. Hence it is simply exponential in the worst case, such as the existing algorithm sketched in Section 2. But now we can use finite domain constraint programming to avoid the naive generate and test approach. This will prove beneficial in practice.

# 11. Exact Computation of Difference Abstraction with Constraints

We now formalize the general problem of difference abstraction with constraints, and show how to solve it for $h_{\Delta_3}$ and $h_{\Delta_6}$.

## 11.1. General Problem

Let $\Sigma = F_{\text{pos-arith}}^{(2)} \uplus C_{\text{pos-arith}}$. The parameter of the problem is a $\Sigma$-abstraction $h: \mathbb{R}_+^2 \to \Delta$ into some finite $\Sigma$-structure $\Delta$. We recall that $\Sigma[\text{dom}(\Delta)]$ is the extension of signature $\Sigma$ with additional constants from $\text{dom}(\Delta)$.

**Definition 38.** The algorithmic problem of difference abstraction with constraints is parameterized by a $\Sigma$-abstraction $h: \mathbb{R}_+^2 \to \Delta$ and has the following three inputs:

**System of linear equations** $L \in \mathcal{F}_{\Sigma}$: this system is to be interpreted over $\mathbb{R}_+$.

**Constraint** $C \in \mathcal{F}_{\Sigma[\text{dom}(\Delta)]}$: a first-order formula which is to be interpreted over $\Delta$.

**Set of observable variables** $V \subseteq \mathcal{V}(L) \cup \mathcal{V}(C)$: a finite subset of the free variables of the linear equation system and the constraint.

The output is the $h$-abstraction of differences of $\mathbb{R}_+$-solutions of $L$, constrained to the $\Delta$-solutions of $C$, and projected to the observable variables in $V$. With $V' = \mathcal{V}(L) \cup \mathcal{V}(C)$ this is:

$$ \{\beta|_V | \beta \in h \circ \text{sol}_{V'}^{\mathbb{R}_+^2}(L) \cap \text{sol}_{V'}^{\Delta}(C)\} $$

In the example of the introductory reaction network in Figure 3, the system of linear equations $L \in \mathcal{F}_{\Sigma}$ is given in Figure 4. As non nonlinear constraint $C \in \mathcal{F}_{\Sigma[\text{dom}(\Delta)]}$ we can choose the kinetic constraints in Figure 4 in conjunction with the overproduction target $v_{\text{out-B}} \doteq \uparrow$. As set observable variables, we may choose whose values represent changes that are controlled externally, which is the inflow of $A$ and the reactions subject to knockout 3 and 4.

$$ V = \{v_{\text{in-A}}, v_3, v_4\} $$

In contrast to the system of linear equation system $L$, the constraint $C$ may contain arbitrary arithmetic formulas including non-linear polynomial equations and universal quantifiers. This is needed to deal with nonlinear kinetic information. This does not make increase the difficulty of the problem to much, since the constraints are to be interpreted over the finite structure $\Delta$, so that the universal quantifiers in $C$ can be replaced by conjunctions, and the existential quantifiers by disjunctions.

The general problem could be simplified, if we could compute an $h$-exact formula $\phi$ that is $\mathbb{R}_+^2$-equivalent to $L$. In this case, it would be sufficient to compute:

$$ \text{sol}^{\Delta}(\exists V. \phi \wedge C) $$

which can be done by finite domain constraint programming. However, the characterizations of the difference abstractions to $\Delta_3$ and $\Delta_6$ in Theorems 33 and 37 do not provide such $h$-exact formulas, so further efforts are needed to solve the above problem. This is what we will do next for $h_{\Delta_3}$ and $h_{\Delta_6}$.
## 11.2. Mixed Structures

For adding a treatment of kinetic constraints over $\Delta_n$ where $n \in \{3, 6\}$, we consider the union $\mathbb{B} \cup \Delta_n$ as a relational structure, unifying the functionalities of both structures $\mathbb{B}$ and $\Delta_n$. For this, we defined the mixed signature by:

$$ \Sigma_n^{\text{mixed}} = \{+^{\mathbb{B}}, *^{\mathbb{B}}, +^{\Delta_n}, *^{\Delta_n}\} \cup \mathbb{B} \cup \Delta_n $$

Here we reuse the binary functions of $\mathbb{B}$ and $\Delta_n$ as the binary function symbols of $\Sigma_n^{\text{mixed}}$ and the values of $\mathbb{B} \cup \Delta_n$ as the constants of $\Sigma_n^{\text{mixed}}$.

**Definition 39.** For any $n \in \{3, 6\}$, the mixed structure $\mathbb{B} \cup \Delta_n$ is the $\Sigma_n^{\text{mixed}}$-structure with the mixed domain $\mathbb{B} \cup \Delta_n$ in which all symbols of $\Sigma_n^{\text{mixed}}$ are by themselves, but now with respect to the mixed domain.

## 11.3. Difference Abstraction with Constraints for $\Delta_3$

Any pair of booleans in $\mathbb{B}^2 \setminus (1, 1)$ is an element in $\Delta_3$, and vice versa. For solving the general problem for $\Delta_3$ we need to capture this relationship in the mixed first-order logic over $\mathbb{B} \cup \Delta_3$. For this we consider the partial function $pair_{\Delta_3} \subseteq (\mathbb{B} \cup \Delta_3)^2 \times (\mathbb{B} \cup \Delta_3)$ such that for all $v_1, v_2 \in \mathbb{B} \cup \Delta_3$:

$$ pair_{\Delta_3}(v_1, v_2) = \begin{cases} (v_1, v_2) & \text{if } v_1 *^{\mathbb{B}} v_2 = 0 \text{ so that } (v_1, v_2) \in \Delta_3 \\ \text{undefined} & \text{else} \end{cases} $$

The domain of this partial function is $dom(pair_{\Delta_3}) = \mathbb{B}^2 \setminus \{(1, 1)\} = \Delta^3$. Any pair from the domain is mapped to itself. We can define the ternary relation $pair_{\Delta_3}$ in the first-order logic of the mixed structure $\mathbb{B} \cup \Delta_3$ by the function $Pair_{\Delta_3} : \mathcal{V}^2 \times \mathcal{V} \to \mathcal{F}_{\Sigma_3^{\text{mixed}}}$ such that for all variables $y_1, y_2, y \in \mathcal{V}$:

$$ \begin{align*} Pair_{\Delta_3}(y_1, y_2, y) &= \text{def} \quad (y_1 = 0 \land y_2 = 0 \land y = \approx) \\ &\lor \quad (y_1 = 0 \land y_2 = 1 \land y = \triangle) \\ &\lor \quad (y_1 = 1 \land y_2 = 0 \land y = \nabla) \end{align*} $$

According to definition 29, the first-order definition $Pair_{\Delta_3}$ indeed defines the relation $pair_{\Delta_3}$ in the mixed structure, that is $pair_{\Delta_3} = Pair_{\Delta_3}^{\mathbb{B} \cup \Delta_3}$. In order to deal with the two inputs of $pair_{\Delta_3}$, we reconsider two new variable generators $\nu_1, \nu_2 : \mathcal{V} \to \mathcal{V}$. Recall that for any subset $V \subseteq \mathcal{V}$, structure $S$, and variable assignment $\alpha : \nu_1(V) \cup \nu_2(V) \to dom(S)$ we defined $\nu^{-1}(\alpha) : V \to dom(S)^2$ such that $\nu^{-1}(\alpha)(y) = (\alpha(\nu_1(y)), \alpha(\nu_2(y)))$ for all $y \in \mathcal{V}$. Next we define for any first-order definition $G : \mathcal{V}^{2m} \to \mathcal{F}_{\Sigma_3^{\text{mixed}}}$ a first-order definition $Pair_{\Delta_3}^m(G) : \mathcal{V}^m \to \mathcal{F}_{\Sigma_3^{\text{mixed}}}$ such that $Pair_{\Delta_3}^m(G)(\mathbf{y})$ describes an application of $Pair_{\Delta_3}$ to the all component of solutions of $G(\mathbf{y})$ for all sequence of variables $\mathbf{y} = y_1 \dots y_m$:

$$ Pair_{\Delta_3}^m(G)(\mathbf{y}) = \exists \nu(\mathbf{y}). G(\nu(\mathbf{y})) \wedge \bigwedge_{i=1}^m Pair_{\Delta_3}(\nu_1(y_i), \nu_2(y_i), y_i) $$

**Lemma 40.** Let $m \in \mathbb{N}$, $G : \mathcal{V}^{2m} \to \mathcal{F}_{\Sigma_3^{\text{mixed}}}$ be a first-order definition, $\mathbf{y}$ be a sequence of variables and $\nu(\mathbf{y}) = \nu_1(\mathbf{y})\nu_2(\mathbf{y})$.

$$ \nu^{-1}(sol^{\mathbb{B}}(G(\nu(\mathbf{y}))) \cap \{\alpha : \{\mathbf{y}\} \to \Delta_3\}) = sol^{\mathbb{B} \cup \Delta_3}(Pair_{\Delta_3}^m(G)(\mathbf{y})) $$
**Proof** The function $pair_{\Delta_3}$ maps all pairs of booleans in $\Delta_3$ to themselves, while being undefined for all elements of $(\Delta_3 \cup \mathbb{B})^2 \setminus \Delta_3$. Hence:

$$ \nu^{-1}(sol_{\mathbb{B}}(G(\nu(\mathbf{y})))) \cap \{\alpha : \{\mathbf{y}\} \to \Delta_3\} = pair_{\Delta_3} \circ \nu^{-1}(sol_{\mathbb{B}\cup\Delta_3}(G(\nu(\mathbf{y})))) $$

The composition with the partial function $pair_{\Delta_3}$ on the right is defined in Section 4.1. As stated there, the composition $pair_{\Delta_3} \circ \alpha$ is defined only for total functions $\alpha$ such that $ran(\alpha) \subseteq dom(pair_{\Delta_3}) = \Delta_3$. So a total function $pair_{\Delta_3} \circ \alpha$ may belong to the composition on the right only if $\alpha$ satisfies this condition.

Proposition 48 on first-order definitions with $F = Pair_{\Delta_3} : \mathcal{V}^2 \times \mathcal{V} \to \mathcal{F}_{\Sigma_3^{\text{mixed}}}^*$ shows that:

$$ Pair_{\Delta_3}^{\mathbb{B}\cup\Delta_3} \circ \nu^{-1}(sol_{\mathbb{B}\cup\Delta_3}(G(\nu(\mathbf{y})))) = sol_{\mathbb{B}\cup\Delta_3}(Pair_{\Delta_3}^m(G)(\mathbf{y})) $$

Here, the parameters are $\ell = 2$, $k = 1$ and $n = 1$. In combination with $pair_{\Delta_3} = Pair_{\Delta_3}^{\mathbb{B}\cup\Delta_3}$, these two equations yield the lemma. $\square$

Since we will work on the structure $\mathbb{B} \cup \Delta_3$, we need to introduce for any $\phi \in \mathcal{F}_{\Sigma}$ the formulas $\phi^{\mathbb{B}}$ and $\phi^{\Delta_3}$ that impose the use of $*^{\mathbb{B}}$ and $+^{\mathbb{B}}$, and respectively $*^{\Delta_3}$ and $+^{\Delta_3}$ when interpreting $\phi$. It follows that $sol_{\mathbb{B}\cup\Delta_3}(\phi^{\mathbb{B}}) = sol_{\mathbb{B}}(\phi)$.

**Theorem 41 (Solving Difference Abstraction with Constraints for $h_{\Delta_3}$).** For any linear formula $L(\mathbf{y}) \in \mathcal{F}_{\Sigma}$ with free variable set $\{\mathbf{y}\}$, and constraint $C(\mathbf{y}') \in \mathcal{F}_{\Sigma[dom(\Delta_3)]}$ with free variable set $\{\mathbf{y}'\}$, and $V \subseteq \{\mathbf{y}\} \cup \{\mathbf{y}'\} = V'$ we can compute at most exponential time a formula over the mixed signature $M \in \mathcal{F}_{\Sigma_3^{\text{mixed}}}^*$ such that:

$$ sol_{\mathbb{B}\cup\Delta_3}(M) = \{\beta|_V | \beta \in h_{\Delta_3} \circ sol_{V^+}^{\mathbb{R}_+^2}(L(\mathbf{y})) \cap sol_{V'}^{\Delta_3}(C(\mathbf{y}'))\} $$

**Proof** Without loss of generality we can assume that $\mathbf{y} = \mathbf{y}'$. If not this can be obtained adding by for all $z \in V'$ a redundant equation $\nu(z) = \nu(z)$ conjunctively to both $L(\mathbf{y})$ and $C(\mathbf{y}')$. Once this is done we have $V' = \{\mathbf{y}\} = \{\mathbf{y}'\}$.

By Theorem 33 we can compute in at most exponential time a formula $\phi(\nu(\mathbf{y})) \in \mathcal{F}_{\Sigma}$ such that:

$$ h_{\Delta_3} \circ \text{diff}(sol_{\mathbb{R}^+}(L)) = \nu^{-1}(sol_{\mathbb{B}}(\phi(\nu(\mathbf{y})))) $$

The formula $M \in \mathcal{F}_{\Sigma_3^{\text{mixed}}}^*$ can then be defined as follows:

$$ M = \text{def} \exists V' \setminus V. Pair_{\Delta_3}^m(\phi(\nu(\mathbf{y})))^{\mathbb{B}} \wedge C(\mathbf{y}')^{\Delta_3} $$

Note that $M$ can be computed in linear time from $\phi(\nu(\mathbf{y}))$ and $C(\mathbf{y}')$. We need to show that formula $M$ satisfies the equation from the theorem. First note that:

$$ sol_{\mathbb{B}}(\phi(\mathbf{y})) = sol_{\mathbb{B}\cup\Delta_3}(\phi(\mathbf{y})^{\mathbb{B}}) $$

Lemma 40 on the first-order definition of $pair_{\Delta_3}$ shows that:

$$ \nu^{-1}(sol_{\mathbb{B}\cup\Delta_3}(\phi(\mathbf{y})^{\mathbb{B}})) \cap \{\alpha : \{\mathbf{y}\} \to \Delta_3\} = sol_{\mathbb{B}\cup\Delta_3}(Pair_{\Delta_3}^m(\phi(\mathbf{y})^{\mathbb{B}})) $$

Hence:

$$ \nu^{-1}(sol_{\mathbb{B}\cup\Delta_3}(\phi(\mathbf{y})^{\mathbb{B}})) \cap sol_{\mathbb{B}\cup\Delta_3}(C(\mathbf{y})^{\Delta_3}) = sol_{\mathbb{B}\cup\Delta_3}(Pair_{\Delta_3}^m(\phi(\mathbf{y})^{\mathbb{B}})) \cap sol_{\mathbb{B}\cup\Delta_3}(C(\mathbf{y})^{\Delta_3}) $$
With the equations we can now conclude as follows:

$$
\begin{align*}
& \{\beta|_V | \beta \in \nu^{-1}(\mathrm{sol}^{\mathbb{B}}(\phi(\mathbf{y}))) \cap \mathrm{sol}^{\Delta_3}(C(\mathbf{y}))\} \\
&= \{\beta|_V | \beta \in \nu^{-1}(\mathrm{sol}^{\mathbb{B}\cup\Delta_3}(\phi(\mathbf{y})^{\mathbb{B}}) \cap \mathrm{sol}^{\mathbb{B}\cup\Delta_3}(C(\mathbf{y})^{\Delta_3})\} \\
&= \{\beta|_V | \beta \in \mathrm{sol}^{\mathbb{B}\cup\Delta_3}(\mathrm{Pair}_{\Delta_3}^m(\phi(\mathbf{y})^{\mathbb{B}}) \cap \mathrm{sol}^{\mathbb{B}\cup\Delta_3}(C(\mathbf{y})^{\Delta_3})\} \\
&= \{\beta' | \beta' \in \mathrm{sol}^{\mathbb{B}\cup\Delta_3}(\exists V' \setminus V. \mathrm{Pair}_{\Delta_3}^m(\phi(\mathbf{y})^{\mathbb{B}}) \wedge C(\mathbf{y})^{\Delta_3})\} \\
&= \mathrm{sol}^{\mathbb{B}\cup\Delta_3}(M)
\end{align*}
$$

□

The set $\mathrm{sol}^{\mathbb{B}\cup\Delta_3}(M)$ can be computed by a finite domain constraint programming, since $\mathbb{B} \cup \Delta_3$ is a finite structure. Therefore Theorem 41 yields an algorithm for solving the general problem of difference abstraction with constraints in the case of $\Delta_3$.

### 11.4. Difference Abstraction with Constraints for $\Delta_6$

We next consider the partial function $\mathrm{pair-sum}_{\Delta_6} \subseteq (\mathbb{B} \cup \Delta_6)^4 \times (\mathbb{B} \cup \Delta_6)$ that maps 2 pairs of booleans to abstract difference in $\Delta_6$ in the sense that for all $\mathbf{b}_1, \mathbf{b}_2 \in \mathbb{B}^2$:

$$ \mathrm{pair-sum}_{\Delta_6}(\mathbf{b}_1, \mathbf{b}_2) = \begin{cases} \mathbf{b}_1 + \mathbb{R}_+^2 & \mathbf{b}_2 \text{ if } \mathbf{b}_1, \mathbf{b}_2 \in \mathbb{B}^2 \text{ and } \mathbf{b}_1 + \mathbb{R}_+^2 \mathbf{b}_2 \in \Delta_6 \\ \text{undefined} & \text{else} \end{cases} $$

By using this partial function and Theorem 37 we can rewrite $h_{\Delta_6} \circ \mathrm{diff}(\mathrm{sol}^{\mathbb{R}_+}(L(\mathbf{y})))$ for any system of linear equation $L(\mathbf{y})$ as follows where $\mu, \nu, \phi$ can be chosen as stated by the theorem:

$$ \{[y/\mathrm{pair-sum}_{\Delta_6}(\beta^2(\nu(\mu_1(y))), \beta^2(\nu(\mu_2(y)))) | y \in \{\mathbf{y}\}] | \beta \in \mathrm{sol}^{\mathbb{B}}(\phi(\nu(\mu(\mathbf{y}))))\} $$

We next define the relations on pairs $\mathrm{pair-sum}_{\Delta_6}$ in the mixed pair FO-logic $\mathbb{B} \cup \Delta_6$ by the function $\mathrm{Pair-Sum}_{\Delta_6} : \mathcal{V}^4 \times \mathcal{V} \in \mathcal{F}_{\Sigma_6^{\mathrm{mixed}}}^*$ such that for all variables $y_1, y_2, y_3, y_4, y \in \mathcal{V}$:

$$
\begin{align*}
\mathrm{Pair-Sum}_{\Delta_6}(y_1, y_2, y_3, y_4, y) =_{\mathrm{def}} & (y_1 \doteq 0 \land y_2 \doteq 0 \land y_3 \doteq 0 \land y_4 \doteq 0 \land y \doteq \approx) \\
& \lor (y_1 \doteq 1 \land y_2 \doteq 1 \land y_3 \doteq 0 \land y_4 \doteq 0 \land y \doteq \sim) \\
& \lor (y_1 \doteq 1 \land y_2 \doteq 0 \land y_3 \doteq 0 \land y_4 \doteq 1 \land y \doteq \uparrow) \\
& \lor (y_1 \doteq 1 \land y_2 \doteq 1 \land y_3 \doteq 0 \land y_4 \doteq 1 \land y \doteq \uparrow) \\
& \lor (y_1 \doteq 0 \land y_2 \doteq 1 \land y_3 \doteq 1 \land y_4 \doteq 0 \land y \doteq \downarrow) \\
& \lor (y_1 \doteq 1 \land y_2 \doteq 1 \land y_3 \doteq 1 \land y_4 \doteq 0 \land y \doteq \downarrow)
\end{align*}
$$

According to Definition 29, the first-order definition $\mathrm{Pair-Sum}_{\Delta_6}$ indeed defines the partial function $\mathrm{pair-sum}_{\Delta_6}$ in the mixed structure, that is

$$ \mathrm{pair-sum}_{\Delta_6} = \mathrm{Pair-Sum}_{\Delta_6}^{\mathbb{B}\cup\Delta_6} $$

We continue with four generators of new variables $\mu_1, \mu_2, \nu_1, \nu_2 : \mathcal{V} \to \mathcal{V}$. For any first-order definition $G : \mathcal{V}^{4m} \to \mathcal{F}_{\Sigma_6^{\mathrm{mixed}}}^*$ we next define a first-order definition $\mathrm{Pair-Sum}_{\Delta_6}^m(G) : \mathcal{V}^m \to \mathcal{F}_{\Sigma_6^{\mathrm{mixed}}}^*$. For all sequence of variables $\mathbf{y} = y_1 \dots y_m$, the formula $\mathrm{Pair-Sum}_{\Delta_6}^m(G)(\mathbf{y})$ describes the application of the partial function defined by $\mathrm{Pair-Sum}_{\Delta_6}$ to the pairs of pairs defined by $G(\nu(\mu(\mathbf{y})))$, i.e.:

$$ \mathrm{Pair-Sum}_{\Delta_6}^m(G)(\mathbf{y}) = \exists \nu(\mu(\mathbf{y})). G(\nu(\mu(\mathbf{y}))) \wedge \bigwedge_{i=1}^m \mathrm{Pair-Sum}_{\Delta_6}(\nu(\mu_1(y_i)), \nu(\mu_2(y_i)), y_i) $$

### Lemma 42.

$$ \mathrm{sol}^{\mathbb{B}\cup\Delta_6}(\mathrm{Pair-Sum}_{\Delta_6}^m(G)(\mathbf{y})) = \left\{ \begin{array}{l} [y/\mathrm{pair-sum}_{\Delta_6}(\beta^2(\nu(\mu_1(\mathbf{y}))), \beta^2(\nu(\mu_2(\mathbf{y})))) | y \in \{\mathbf{y}\}] \\ | \beta \in \mathrm{sol}^{\mathbb{B}\cup\Delta_6}(G(\nu(\mu(\mathbf{y})))) \end{array} \right\} $$
**Proof** We use the fact that pair-sum<sub>Δ<sub>6</sub></sub> = Pair-Sum<sub>Δ<sub>6</sub></sub><sup>Б∪Δ<sub>6</sub></sup> and the general property of first-order definition from Proposition 48 with F = Pair-Sum<sub>Δ<sub>6</sub></sub>, ℓ = 4, k = 1 and n = 1. As four new variable generators there we use {ν<sub>i</sub> ∘ μ<sub>j</sub> | i, j ∈ {1, 2}}.

$$
\mathrm{sol}^{\mathbb{B}\cup\Delta_6}(\mathrm{Pair-Sum}_{\Delta_6}^m(G)(\mathbf{y})) = \mathrm{pair-sum}_{\Delta_6} \circ \left\{ \begin{array}{l} \alpha : \{\mathbf{y}\} \to \mathbb{B} \cup \Delta_6 \mid \exists \beta \in \mathrm{sol}^{\mathbb{B}\cup\Delta_6}(G(\nu(\mu(\mathbf{y})))) \\ \forall \mathbf{y} \in \{\mathbf{y}\}. \alpha(\mathbf{y}) = \beta^2(\nu(\mu_1(\mathbf{y}))), \beta^2(\nu(\mu_2(\mathbf{y}))) \end{array} \right\}
$$

**Proposition 43.** For any formula $\phi(\nu(\mu(\mathbf{y}))) \in \mathcal{F}_{\Sigma}$ and constraint $C(\mathbf{y}) \in \mathcal{F}_{\Sigma[\mathrm{dom}(\Delta_6)]}$ with the same free variables $\{\mathbf{y}\}$, and any subset $V \subseteq \{\mathbf{y}\}$ we can compute in linear time a formula $M \in \mathcal{F}_{\Sigma_6^{\mathrm{mixed}}}$ with $fv(M) = V$ such that:

$$
\mathrm{sol}^{\mathbb{B}\cup\Delta_6}(M) = \left\{ \begin{array}{ll} \alpha & \alpha = [y/\mathrm{pair-sum}_{\Delta_6}(\beta^2(\nu(\mu_1(y))), \beta^2(\nu(\mu_2(y)))) | y \in \{\mathbf{y}\}], \\ \alpha|_V & \beta \in \mathrm{sol}^{\mathbb{B}}(\phi(\nu(\mu(\mathbf{y})))) \\ \beta & \alpha \in \mathrm{sol}^{\Delta_6}(C(\mathbf{y})) \end{array} \right\} \cap \{\alpha|_V | \alpha \in \mathrm{sol}^{\Delta_6}(C(\mathbf{y}))\}
$$

**Proof** We can chose $M = \exists\{\mathbf{y}\} \setminus V$. Pair-Sum<sub>Δ<sub>6</sub></sub><sup>m</sup>($L(\mathbf{y})$) ∧ $C(\mathbf{y})^{\Delta_6}$.

$$
\left\{
\begin{array}{l}
\alpha|_V \mid \alpha = [y/\text{pair-sum}_{\Delta_6}(\beta^2(\nu(\mu_1(y))), \beta^2(\nu(\mu_2(y)))) \mid y \in \{\mathbf{y}\}], \\
\beta \in \text{sol}^{\mathbb{B}}(\phi(\nu(\mu(\mathbf{y})))) \\
= \text{sol}^{\mathbb{B}\cup\Delta_6}(\text{Pair-Sum}_{\Delta_6}^m(\phi(\mathbf{y}))) \cap \{\alpha|_V \mid \alpha \in \text{sol}^{\mathbb{B}\cup\Delta_6}(C(\mathbf{y})^{\Delta_6}) \\
= \text{sol}^{\mathbb{B}\cup\Delta_6}(M)
\end{array}
\right\} \cap \{\alpha|_V \mid \alpha \in \text{sol}^{\Delta_6}(C(\mathbf{y}))\}
$$

By Lemma 42

□

**Theorem 44 (Solving Difference Abstraction with Constraints for $h_{\Delta_6}$).** For any linear formula $L(\mathbf{y}) \in \mathcal{F}_{\Sigma}$ with free variable set $\{\mathbf{y}\}$, and constraint $C(\mathbf{y}') \in \mathcal{F}_{\Sigma[\mathrm{dom}(\Delta_6)]}$ with free variable set $\{\mathbf{y}'\}$, and $V \subseteq \{\mathbf{y}\} \cup \{\mathbf{y}'\} = V'$ we can compute in at most exponential time a formula over the mixed signature $M \in \mathcal{F}_{\Sigma_6^{\mathrm{mixed}}}$ such that:

$$
\mathrm{sol}^{\mathbb{B}\cup\Delta_6}(M) = \{\beta|_V \mid \beta \in h_{\Delta_6} \circ \mathrm{sol}_{V'}^{\mathbb{R}^2}(L(\mathbf{y})) \cap \mathrm{sol}_{V'}^{\Delta_6}(C(\mathbf{y}'))\}
$$

**Proof** As for the difference abstraction with constraints for $\Delta_3$, without loss of generality we can assume that $\mathbf{y} = \mathbf{y}'$. Once this is done we have $V' = \{\mathbf{y}\} = \{\mathbf{y}'\}$. By Theorem 37, we can compute it at most exponential time a formula $\phi(\nu(\mu(\mathbf{y}))) \in \mathcal{F}_{\Sigma}$ such that:

$$
h_{\Delta_6} \circ \mathrm{diff}(\mathrm{sol}^{\mathbb{R}_+}(L(\mathbf{y}))) = \{[y/(\beta^2(\nu(\mu_1(\mathbf{y}))) + \beta^2(\nu(\mu_2(\mathbf{y})))) | y \in \{\mathbf{y}\}] | \beta \in \mathrm{sol}^{\mathbb{B}}(\phi(\nu(\mu(\mathbf{y}))))\}
$$

With the definition of pair-sum<sub>Δ<sub>6</sub></sub> we obtain:

$$
h_{\Delta_6} \circ \mathrm{diff}(\mathrm{sol}^{\mathbb{R}_+}(L(\mathbf{y}))) = \left\{ \begin{array}{l} \alpha = [y/\mathrm{pair-sum}_{\Delta_6}(\beta^2(\nu(\mu_1(y))), \beta^2(\nu(\mu_2(y)))) | y \in \{\mathbf{y}\}], \\ \beta \in \mathrm{sol}^{\mathbb{B}}(\phi(\nu(\mu(\mathbf{y})))) \end{array} \right\}
$$

Finally from Proposition 43, we can compute in linear time a formula $M \in \mathcal{F}_{\Sigma_6^{\mathrm{mixed}}}$ such that

$$
\mathrm{sol}^{\mathbb{B}\cup\Delta_6}(M) = \left\{ \begin{array}{ll} \alpha & \alpha = [y/\mathrm{pair-sum}_{\Delta_6}(\beta^2(\nu(\mu_1(\mathbf{y}))), \beta^2(\nu(\mu_2(\mathbf{y})))) | y \in \{\mathbf{y}\}], \\ \alpha|_V & \beta \in \mathrm{sol}^{\mathbb{B}}(\phi(\nu(\mu(\mathbf{y})))) \\ \beta & \alpha \in \mathrm{sol}^{\Delta_6}(C(\mathbf{y})) \end{array} \right\} \cap \{\alpha|_V | \alpha \in \mathrm{sol}^{\Delta_6}(C(\mathbf{y}))\}
$$

□

The set $\mathrm{sol}^{\mathbb{B}\cup\Delta_6}(M)$ can be computed by a finite domain constraint programming, since $\mathbb{B}\cup\Delta_6$ is a finite structure. By combining Theorem 37 and Proposition 43 we obtain an algorithm for solving the general problem of Section 11 in the case of $\Delta_6$.
## 12. Overapproximation Heuristics with Minimal Support Consequences

We propose a new heuristics for approximating the problem of difference abstractions with constraints. Later on, we will see experimentally that this heuristics is close to exact in our main application while requiring considerably less computation time.

Let $h: \mathbb{R}_+^2 \to \Delta$ be some $\Sigma$-abstraction into a finite $\Sigma$-structure $\Delta$. The general idea of the existing heuristics (see e.g. [8]) for approximating the problem of difference abstractions with constraints from Definition 38 is as follows. Given a linear equation system $L \in \mathcal{F}_{\Sigma}$, a constraint $C \in \mathcal{F}_{\Sigma[\text{dom}(\Delta)]}$ and subsets of variable $V \subseteq V' = \mathcal{V}(L) \cup \mathcal{V}(C)$, we first compute some linear equation system $L' \in \mathcal{F}_{\Sigma}$ that is a logical consequence of $L$ over $\mathbb{R}_+$ with $\mathcal{V}(L') \subseteq V'$, and in a second step the set of abstract solutions:

$$ \mathrm{sol}^{\Delta}(\exists V. (L \land L' \land C)) $$

by finite domain constraint programming. By John's theorem in Corollary 24, this set is an overapproximation of the target of the problem $\{\beta|_V | \beta \in \mathrm{sol}_{V'}^{\mathbb{R}_+}(L)^{\Delta} \cap \mathrm{sol}_{V'}^{\Delta'}(C)\}$.

The choice of which $\mathbb{R}_+$-consequence $L'$ of $L$ to add to $L$ is critical. Generally, $L'$ is a finite conjunction of linear equations that are $\mathbb{R}_+$-consequences of $L$. These are all the linear combinations of equations in $L$. Unfortunately, there are infinitely many such linear combinations, of which $L'$ has to choose some finite subset.

We call an equation $E \in \mathcal{F}_{\Sigma}$ linear if $E$ has the form $n_1x_1 + \dots + n_kx_k \doteq m_1y_1 + \dots + m_l y_l$ for some pairwise distinct variables $x_i$ and $y_j$, natural numbers $k, l \ge 0$ and nonzero natural numbers $n_i, m_j > 0$. We call $E$ nontrivial if not $k = 0$ and $l = 0$. The support of $E$ is the set of its free variables $\mathcal{V}(E)$. We call $E$ normalized if there not exists a natural number $p, n'_1, \dots, n'_l, m'_1, \dots, m'_n$ such that $n_i = p *^{\mathbb{N}} n'_i$ and $m_j = p *^{\mathbb{N}} m'_j$ for all $i, j$.

**Definition 45 (Minimal support linear $\mathbb{R}_+$-consequences).** A linear equation $E \in \mathcal{F}_{\Sigma}$ is a minimal support linear $\mathbb{R}_+$-consequence of a system of linear equations $L \in \mathcal{F}_{\Sigma}$ if it satisfies the following three conditions:

* $E$ is a nontrivial $\mathbb{R}_+$-consequence of $L$,

* not other nontrivial $\mathbb{R}_+$-consequence of $L$ has a smaller support than $E$, and

* $E$ is normalized.

It is not difficult to see that no two different minimal support linear $\mathbb{R}_+$-consequences of $L$ may have the same support. Therefore, the set of minimal support linear $\mathbb{R}_+$-consequences of $L$ is finite and of cardinality at most $2^{|\mathcal{V}(E)|}$. Given a system of linear equations $L \in \mathcal{F}_{\Sigma}$ we denote the conjunction of all its minimal support linear $\mathbb{R}_+$-consequences by:

$$ L_{msc} \in \mathcal{F}_{\Sigma} $$

We next show how to compute $L_{msc}$ from $L$. First, we transform $L$ into an integer matrix $A$ in linear time, such $L$ is equivalent to $Ax = 0$, where $\mathcal{V}(L) = \{x\}$. The $\mathbb{R}_+$-consequences of $L$ are thus the linear combination of the rows of $A$. Since we want to combine the rows of $A$ and not its columns, we consider the transposed matrix $A^T$. Given a sequence $z$ of with as many fresh variables as $A$ has rows, the linear combinations of the rows of $A$ (the row space) can be identified with the following set of integer solutions:

$$ \mathrm{sol}^{\mathbb{Z}}(\exists y. A^T y = z) $$
Since the row space is the orthogonal complement of A's nullspace $sol^Z(Ax = 0)$, we have that each vector corresponding to a $R_+$-consequence of L must be orthogonal to every vector in the nullspace, and in particular to any of its bases. Let $A^\perp$ be some basis of the nullspace of A, which can be easily computed by using Gauß algorithm. Then the row space is given by:

$$sol^Z(A^\perp z = 0)$$

Since we are interested only in the subset of solutions of the above system which are nonzero, normalized and with a minimal support, the problem of finding them is simply a particular case of the computation of the elementary modes of the orthogonal complement of the nullspace of A, with basis $A^\perp$, but such that nonpositive solutions are considered too. The usual software packages for computing elementary modes can then be applied to $A^\perp$ to compute such “reversible” elementary modes [26], or equivalently the problem can be reduced to computing the extreme rays of a cone and solved with any library for the analysis of polytopes, such as [27, 25].

# 13. Implementation and Experimentation

We have implemented the algorithm solving the differences abstraction problem with constraints in the case of difference abstraction $h_{\Delta_6}$ and applied them to change prediction in systems biology

## 13.1. Implementation

First, we implemented the exact rewriting of linear equation systems for the boolean abstraction $h_B$. We implemented the rewriting in Python while using the libccd library for computing elementary modes [27, 28].

Second, we implemented a solver for first-order constraint in the mixed structure $B \cup \Delta_6$ by finite domain constraint programming with the Minizinc tool [12].

Third, we implemented the exact computation of difference abstractions for $h_{\Delta_6}$. This was done in Python based on implementation obtained in the first and second step.

Fourth, we use BioComputing's Reaction-Network tool to represent reaction networks with partial kinetic information in XML-format and to infer the linear equation systems and the nonlinear kinetic constraints. The tools does also support John's overapproximation algorithm. We then integrated our exact algorithm for computing difference abstraction with $h_{\Delta_6}$ into the tool, so that it can be applied the systems of linear equation and nonlinear constraints obtained from a reaction network.

Fifth, we implemented the minimal support heuristics again in Python. For this we had to compute “reversible” elementary modes. We again used the libccd library for this, by reducing the computation of reversible elementary modes to the computation of irreversible elementary modes. We used standard Python libraries to applying Gauß algorithm to compute the orthogonal matrix $A^\perp$.

Sixth, we integrated the minimal support heuristics into BioComputing's Reaction-Network tool [29]. We also added a support to compare the solutions sets obtained by John's overapproximation, the minimal support heuristics, and the exact algorithm.

The graphical output of reaction networks is done with BioComputing's Network-Graph tool. It also allows to annotate abstract solution or the elementary flux modes to the network graph, and is integrated into the Reaction-Network tool. BioComputing's Network-Graph tool is publicly available, while the other components of BioComputing Reaction-Network tool are not yet made publicly available.
<table><caption>Figure 16: Predictions for the networks analysed in this paper, obtained respectively by pure abstract interpretation, the heuristics based on minimal support consequences and the exact algorithm.</caption><thead><tr><th>Network</th><th>Count type</th><th>John's over-approx.</th><th>min. support consequences</th><th>exact</th></tr></thead><tbody><tr><td>Simple loop (Figure 6)</td><td>abstract solutions</td><td>19</td><td>6</td><td>6</td></tr><tr><td rowspan="2">Leucine overproduction (Figure 20)</td><td>knockouts</td><td>16</td><td>14</td><td>14</td></tr><tr><td>abstract solutions</td><td>292</td><td>228</td><td>228</td></tr><tr><td>Counter example (Figure 17a)</td><td>abstract solutions</td><td>≥ 10000</td><td>4454</td><td>4374</td></tr></tbody></table>

## 13.2. Application to Change Prediction of Reaction Networks

The main application of the change prediction algorithm for reaction networks with partial kinetic information [8, 10] concerns overproduction of the branched chain amino acid Leucine by the reaction network in Figure 20. Leucine is a predecessor of the surfactin, a nonribosomal peptide, that can be used as a surfactant and produced industrially by the bacteria B. Subtilis. Some of the change predictions obtained for this application where verified successfully in the bioreactor.

We compare the results of John's overapproximation, the minimal support heuristics and the exact algorithm in Figure 16. Beside of the leucine network we also consider the simple loop network and the counter example in Figure 17a.

For the simple loop network, the exact algorithm shows that there are 6 abstract solutions, one for each value of $\Delta_6$. The minimal support heuristics finds the same 6 abstract solutions, while by John's overapproximation returns 19 abstract solutions, of which 13 are not justified.

For the leucine network from Figure 20 the minimal support heuristics finds the same 228 solutions as the exact algorithm. John's overapproximation algorithm produces 292 solutions instead, including the 228 justified solutions.

On the other hand, the minimal support heuristics is remarkably faster than the exact algorithm – in the benchmark on leucine overproduction, we have 5 minutes versus 5 hours.

## 13.3. Counter Example for the Minimal Support Heuristics

We found and implemented the minimal support heuristics some years before finding the exact algorithm. At that time it was impossible to us to see whether the minimal support heuristics was exact or not. After having developed and implemented the exact algorithm, we could eventually evaluate this question. Our experiments showed that the heuristics is indeed exact for all applications to change prediction of reaction networks in systems biology that we tested. We then tried to prove in the case of $\Delta_3$ that the minimal support heuristics was always exact, but failed to do so.

Next, we tried to find a counter example in the case of $\Delta_6$. For this we developed a random generator of reaction networks and compared the minimal support heuristics with the exact algorithm that we implemented for $\Delta_6$ only. This made us indeed find a counter example for $\Delta_6$ that is given in Figure 17a.

Why the minimal support heuristics admits abstract solutions that are not justified is not easy to understand.

We can see for instance that $v_4 = v_5 + v_{in-B}$ is a minimal support linear consequence, by looking at the elementary flux modes of the counter example network in Figure 17b. The list of all other minimal support linear consequences are given in Figure 18. We can also recognize,
<figure><img src="image_13.png" /><figcaption>Figure 17: Counter example for exactness of the minimal support heuristics for $\Delta_6$.</figcaption></figure>

<figure><img src="image_14.png" /><figcaption>Figure 18: Minimal support consequences</figcaption></figure>

which of the abstract solutions are unjustified. An example is given in Figure 19. But we could not explain why this solution is unjustified, or find some nonminimal support consequence that it violates.
<figure><img src="image_15.png" /><figcaption>Figure 19: An unjustified solution found with the minimal support heuristics.</figcaption></figure>

## 14. First-Order Function Application

Our next objective is to generalize the definition of function application in first-order logic to functions with higher arities, as used already in special cases, and to prove formal properties of such definitions.

We will use vector notation all over. We fix $\ell, k, n \in \mathbb{N}$ and consider first-order definitions $F: \mathcal{V}^{\ell} \times \mathcal{V}^k \to \mathcal{F}_{\Sigma}^n$ that define a partial function $F^{S^n} \subseteq \text{dom}(S^n)^{\ell} \times \text{dom}(S^n)^k$ for the $\Sigma$-structure $S$ under consideration. For any $m$, we can lift the first-order definition $F$ to a first-order definition $F^m: \mathcal{V}^{m\ell} \times \mathcal{V}^{mk} \to \mathcal{F}_{\Sigma}^n$ where $F$ is applied $m$-times, such that for all sequences $\mathbf{x}^1, \dots, \mathbf{x}^\ell, \mathbf{y}^1, \dots, \mathbf{y}^k \in \mathcal{V}^m$:

$$F^m(\mathbf{x}^1 \dots \mathbf{x}^\ell \mathbf{y}^1 \dots \mathbf{y}^k) =_{\text{def}} \bigwedge_{i=1}^m F(\mathbf{x}_i^1 \dots \mathbf{x}_i^\ell \mathbf{y}_i^1 \dots \mathbf{y}_i^k)$$

For any first-order definition $G: \mathcal{V}^{m\ell} \to \mathcal{F}_{\Sigma}^n$, we introduce a first-order definition $F^m(G): \mathcal{V}^{mk} \to \mathcal{F}_{\Sigma}^n$ such that for all $\bar{\mathbf{y}} \in \mathcal{V}^{mk}$:

$$F^m(G)(\bar{\mathbf{y}}) =_{\text{def}} \exists \bar{\mathbf{x}}. G(\bar{\mathbf{x}}) \wedge F^m(\bar{\mathbf{x}}, \bar{\mathbf{y}})$$

where $\bar{\mathbf{x}} = (\mathbf{x}^1 \dots \mathbf{x}^\ell) \in \mathcal{V}^{m\ell}$ is some sequence of fresh variables. Note that $fv(F^m(G)(\bar{\mathbf{y}})) = \{\bar{\mathbf{y}}\}$ so that the precise choice of $\mathbf{x}$ is irrelevant.

**Lemma 46.** Let $F: \mathcal{V}^{\ell+k} \to \mathcal{F}_{\Sigma}^n$ and $G: \mathcal{V}^{m\ell} \to \mathcal{F}_{\Sigma}^n$ be first-order definitions and $S$ a $\Sigma$-structure $S$. If the relation $F^{S^n} \subseteq \text{dom}(S^n)^{\ell+k}$ is a partial function of type $\text{dom}(S^n)^\ell \times \text{dom}(S^n)^k$ then the relation $(F^m)^{S^n}$ is a partial function of type $\text{dom}(S^n)^{m\ell} \times \text{dom}(S^n)^{mk}$ such that:

$$(F^m)^{S^n}(G^{S^n}) = F^m(G)^{S^n}$$

**Proof** Let $\bar{\mathbf{x}} = \mathbf{x}^1 \dots \mathbf{x}^\ell \in \mathcal{V}^{m\ell}$ and $\bar{\mathbf{y}} = \mathbf{y}^1 \dots \mathbf{y}^k \in \mathcal{V}^{mk}$ be sequences of variables such that no
variables occurs twice in $\bar{\mathbf{xy}}$. Then:

$$
\begin{align*}
(F^m)^{S^n}(G^{S^n}) &= \{(F^m)^{S^n}(\alpha(\bar{\mathbf{x}})) \mid \alpha \in \mathrm{n-sol}^S(G(\bar{\mathbf{x}}))\} \\
&= \{\alpha'(\bar{\mathbf{y}}) \mid \alpha' \in \mathrm{n-sol}^S(F^m(\bar{\mathbf{y}})), \alpha'_{\{|\bar{\mathbf{x}}|} \in \mathrm{n-sol}^S(G(\bar{\mathbf{x}}))\}\} \\
&= \{\alpha'(\bar{\mathbf{y}}) \mid \alpha' \in \mathrm{n-sol}^S(G(\bar{\mathbf{x}}) \wedge F^m(\bar{\mathbf{y}}))\} \\
&= \{\alpha''(\bar{\mathbf{y}}) \mid \alpha'' \in \mathrm{n-sol}^S(\exists \bar{\mathbf{x}}. G(\bar{\mathbf{x}}) \wedge F^m(\bar{\mathbf{y}}))\} \\
&= F^m(G)^{S^n}
\end{align*}
$$

For the previous last step note that for any $\alpha' \in n\text{-sol}^S(G(\bar{\mathbf{x}}) \wedge F^m(\bar{\mathbf{y}}))$ we can chose $\alpha''$ as the restriction $\alpha'_{|V\setminus\{\bar{\mathbf{x}}\}}$. Conversely, for any $\alpha'' \in n\text{-sol}^S(\exists \bar{\mathbf{x}}. G(\bar{\mathbf{x}}) \wedge F^m(\bar{\mathbf{y}}))$ there must exist a solution $\alpha' \in n\text{-sol}^S(G(\bar{\mathbf{x}}) \wedge F^m(\bar{\mathbf{y}}))$ such that $\alpha''$ is the restriction $\alpha'_{|V\setminus\{\bar{\mathbf{x}}\}}$. $\square$

For the case $k = 1$ and $\ell = 1$ Lemma 46 yields the following consequence.

**Proposition 47** ($\ell = 1$ and $k = 1$). For any FO definition $G: \mathcal{V}^m \to \mathcal{F}_{\Sigma}^n$ and $F: \mathcal{V} \times \mathcal{V} \to \mathcal{F}_{\Sigma}^n$, sequence of variables $\mathbf{y} \in \mathcal{V}^m$ and $\Sigma$-structure $S$ for which the relation $F^{S^n}$ is a partial function of type $\mathrm{dom}(S^n) \times \mathrm{dom}(S^n)$:

$$F^{S^n} \circ n\text{-sol}^S(G(\mathbf{y})) = n\text{-sol}^S(F^m(G)(\mathbf{y}))$$

**Proof** From Lemmata 30 and 46:

$$
\begin{array}{l@{\qquad}l}
\text{Lemma 30} & F^{S^n} \circ n\text{-sol}^S(G(\mathbf{y})) \\
& = F^{S^n} \circ \{[\mathbf{y}/\mathbf{s}] \mid \mathbf{s} \in G^{S^n}\} \\
& = \{[\mathbf{y}/\mathbf{s}] \mid \mathbf{s} \in (F^m)^{S^n}(G^{S^n})\} \\
\text{Lemma 46} & = \{[\mathbf{y}/\mathbf{s}] \mid \mathbf{s} \in F^m(G)^{S^n}\} \\
\text{Lemma 30} & = n\text{-sol}^S(F^m(G)(\mathbf{y}))
\end{array}
$$

$\square$

For the case of general $\ell$ and $k = 1$, Proposition 47 can be generalized as follows:

**Proposition 48** ($\ell \ge 1$ and $k = 1$). Let $G: \mathcal{V}^{\ell m} \to \mathcal{F}_{\Sigma}^n$ and $F: \mathcal{V}^{\ell} \times \mathcal{V} \to \mathcal{F}_{\Sigma}^n$ be a first-order definition, and $S$ a $\Sigma$-structure such that the relation $F^{S^n}$ is a partial function of type $\mathrm{dom}(S^n)^{\ell} \times \mathrm{dom}(S^n)$. Then for any $\mathbf{y} \in \mathcal{V}^m$ and fresh variable generators $\nu_1, \dots, \nu_\ell$ the sequence of variables $\nu(\mathbf{y}) = \nu_1(\mathbf{y}) \dots \nu_\ell(\mathbf{y})$ satisfies:

$$F^{S^n} \circ \nu^{-1}(n\text{-sol}^S(G(\nu(\mathbf{y})))) = n\text{-sol}^S(F^m(G)(\mathbf{y}))$$

where $\nu^{-1}(\alpha)(y) = (\alpha(\nu_1(y)), \dots, \alpha(\nu_\ell(y)))$ for all $y \in \mathcal{V}(\mathbf{y})$ and $\alpha: \cup_{i=1}^\ell \mathcal{V}(\nu_i(\mathbf{y})) \to \mathrm{dom}(S^n)$.

**Proof** Again from Lemmata 30 and 46, by generalizing and adpatation of the proof of Proposition 47:

$$
\begin{array}{l@{\qquad}l}
F^{S^n} \circ \nu^{-1}(n\text{-sol}^S(G(\nu(\mathbf{y})))) & \\
\text{Lemma 30} & = F^{S^n} \circ \{\nu^{-1}[\nu(\mathbf{y})/\mathbf{s}] \mid \mathbf{s} \in G^{S^n}\} \\
& = \{[\mathbf{y}/\mathbf{s}] \mid \mathbf{s} \in (F^m)^{S^n}(G^{S^n})\} \\
\text{Lemma 46} & = \{[\mathbf{y}/\mathbf{s}] \mid \mathbf{s} \in F^m(G)^{S^n}\} \\
\text{Lemma 30} & = n\text{-sol}^S(F^m(G)(\mathbf{y}))
\end{array}
$$

$\square$

For general $k \ge 1$ and $l = 1$, Lemma 46 yields the following generalization of Proposition 47:

**Proposition 49** ($\ell = 1$ and $k \ge 1$). For any first-order definition $G: \mathcal{V}^m \to \mathcal{F}_{\Sigma}^n$ and $F: \mathcal{V} \times \mathcal{V}^k \to \mathcal{F}_{\Sigma}^n$ and any structure $S$ such that the relation $F^{S^n}$ is a partial function of type $\mathrm{dom}(S^n) \times \mathrm{dom}(S^n)^k$, and any sequences of fresh variables $\mathbf{y}, \mathbf{y}^1, \dots, \mathbf{y}^k \in \mathcal{V}^m$:

$$(F^m)^{S^n} \circ n\text{-sol}^S(G(\mathbf{y})) = \{[\mathbf{y}/(\alpha(\mathbf{y}^1), \dots, \alpha(\mathbf{y}^k))] \mid \alpha \in n\text{-sol}^S(F^m(G)(\mathbf{y}^1, \dots, \mathbf{y}^k))\}$$
**Proof** This is another generalization of the proof of Proposition 47:

$$
\begin{array}{l@{\qquad}l}
\text{Lemma 30} & F^{S^n} \circ n\text{-sol}^S(G(\mathbf{y})) \\
& = F^{S^n} \circ \{[\mathbf{y}/\mathbf{s}] \mid \mathbf{s} \in G^{S^n}\} \\
& = \{[\mathbf{y}/(\mathbf{s}^1, \dots, \mathbf{s}^k)] \mid (\mathbf{s}^1, \dots, \mathbf{s}^k) \in (F^m)^{S^n} (G^{S^n})\} \\
\text{Lemma 46} & = \{[\mathbf{y}/(\mathbf{s}^1, \dots, \mathbf{s}^k)] \mid (\mathbf{s}^1, \dots, \mathbf{s}^k) \in F^m(G)^{S^n}\} \\
\text{Lemma 30} & = \{[\mathbf{y}/(\alpha(\mathbf{y}^1), \dots, \alpha(\mathbf{y}^k))] \mid \alpha \in n\text{-sol}^S(F^m(G)(\mathbf{y}^1, \dots, \mathbf{y}^k))\}
\end{array}
$$

<figure><img src="image_16.png" /></figure>

15. Conclusion

We presented a new algorithm for computing the difference abstraction over $\Delta_3$ and $\Delta_6$ of the
solution set of a system of linear equation systems with nonlinear constraints on the difference
abstractions. The algorithm relies on an exact rewriting of linear equation systems with respect
to the boolean abstraction, which can be based on elementary modes. Our reduction uses
decompositions of the difference abstractions $h_{\Delta_3}$ and $h_{\Delta_6}$ into the boolean abstractions and
functions on pair algebra $\mathbb{R}_+^2$ that can be defined in first-order logic with pairs. Eventually,
we can compute the difference abstractions for systems of linear equation with constraints by
finite domain constraint programming. We implemented our algorithm and applied it to change
prediction of reaction networks with partial kinetic information in systems biology.

We also presented the minimal support heuristics, for approximating the difference abstrac-
tion over $\Delta_3$ and $\Delta_6$ of the solution set of a system of linear equation systems with nonlinear
constraints. It turns out that the minimal support heuristics is exact for the prime application of
change prediction while requiring much less computation time. It was difficult to find a counter-
example shown that the minimal support heuristics is not always exact. We finally succeeded in
for the case of $\Delta_6$ by randomly generating and testing reaction networks. In the case of $\Delta_3$ the
question remains open though.

We believe that the presented algorithms are fundamental to develop better change prediction
methods in the future. For this, it is important to not only deal with cycles in the metabolic
parts of reaction networks but also deal with cycles through the regulatory part. An important
challeange in practice is to provide multiple changes prediction. The current approaches, however,
are not sufficiently precise to do so. This is due to the lack of kinetic information. Furthermore,
the current approach can only abstract the differences of steady states, but not account for their
relationship to initial states.

In the longer run, it would be of interest to obtain more quantitative predictions and not only
qualitative predictions. But this would require more precise kinetic information in the reaction
networks and to use more refined difference abstractions for the abstract interpretation.

*Acknowledgements.* We thank the anonymous reviewers of this journal version and also the reviewers of the CMSB’2019 version for their helpful and constructive feedback.

References

[1] Emilie Allart, Joachim Niehren, and Cristian Versari. Computing difference abstractions of metabolic networks under kinetic constraints. In Luca Bortolussi and Guido Sanguinetti, editors, *Computational Methods in Systems Biology - 17th International Conference, CMSB 2019, Trieste, Italy, September 18-20, 2019, Proceedings*, volume 11773 of Lecture Notes in Computer Science, pages 266–285. Springer, 2019. doi: 10.1007/978-3-030-31304-3_14. URL https://doi.org/10.1007/978-3-030-31304-3_14.
[2] Jeffrey D Orth, Ines Thiele, and Bernhard O Palsson. What is flux balance analysis? *Nature biotechnology*, 28(3):245-248, 2010.

[3] Jason A Papin, Joerg Stelling, Nathan D Price, Steffen Klamt, Stefan Schuster, and Bernhard O Palsson. Comparison of network-based pathway analysis methods. *Trends in biotechnology*, 22(8):400-405, 2004.

[4] Martin Feinberg. Chemical reaction network structure and the stability of complex isothermal reactors. *Chemical Engineering Science*, 42(10):2229-2268, 1987. ISSN 0009-2509. doi: http://dx.doi.org/10.1016/0009-2509(87)80099-4. URL http://www.sciencedirect.com/science/article/pii/0009250987800994.

[5] Laurence Calzone, Francois Fages, and Sylvain Soliman. BIOCHAM: an environment for modeling biological systems and formalizing experimental knowledge. *Bioinformatics*, 22 (14):1805-1807, July 2006. doi: 10.1093/bioinformatics/btl172. URL http://dx.doi.org/10.1093/bioinformatics/btl172.

[6] Stefan Hoops, Sven Sahle, Ralph Gauges, Christine Lee, Jürgen Pahle, Natalia Simus, Mutdita Singhal, Liang Xu, Pedro Mendes, and Ursula Kummer. Copasi—a complex pathway simulator. *Bioinformatics*, 22(24):3067-3074, 2006.

[7] François Fages, Steven Gay, and Sylvain Soliman. Inferring reaction systems from ordinary differential equations. *Theor. Comput. Sci.*, 599:64-78, 2015. doi: 10.1016/j.tcs.2014.07.032. URL http://dx.doi.org/10.1016/j.tcs.2014.07.032.

[8] Joachim Niehren, Cristian Versari, Mathias John, François Coutte, and Philippe Jacques. Predicting Changes of Reaction Networks with Partial Kinetic Information. *BioSystems*, 149:113-124, July 2016. URL https://hal.inria.fr/hal-01239198.

[9] François Coutte, Joachim Niehren, Debarun Dhali, Mathias John, Cristian Versari, and Philippe Jacques. Modeling Leucine's Metabolic Pathway and Knockout Prediction Improving the Production of Surfactin, a Biosurfactant from Bacillus Subtilis. *Biotechnology Journal*, 10(8):1216-134, August 2015. doi: 10.1002/biot.201400541. URL https://hal.inria.fr/hal-01153704.

[10] Mathias John, Mirabelle Nebut, and Joachim Niehren. Knockout Prediction for Reaction Networks with Partial Kinetic Information. In *14th International Conference on Verification, Model Checking, and Abstract Interpretation*, Rom, Italy, January 2013. URL http://hal.inria.fr/hal-00692499.

[11] Kim Marriott, Peter J. Stuckey, and Mark Wallace. Constraint logic programming. In Francesca Rossi, Peter van Beek, and Toby Walsh, editors, *Handbook of Constraint Programming*, volume 2 of *Foundations of Artificial Intelligence*, pages 409-452. Elsevier, 2006. doi: 10.1016/S1574-6526(06)80016-7. URL https://doi.org/10.1016/S1574-6526(06)80016-7.

[12] Nicholas Nethercote, Peter J. Stuckey, Ralph Becket, Sebastian Brand, Gregory J. Duck, and Guido Tack. Minizinc: Towards a standard CP modelling language. In Christian Bessiere, editor, *Principles and Practice of Constraint Programming - CP 2007, 13th International Conference, CP 2007, Providence, RI, USA, September 23-27, 2007, Proceedings*, volume 4741 of *Lecture Notes in Computer Science*, pages 529-543. Springer, 2007. doi: 10.1007/978-3-540-74970-7_38. URL https://doi.org/10.1007/978-3-540-74970-7_38.
[13] Julien Gagneur and Steffen Klamt. Computation of elementary modes: a unifying framework and the new binary approach. *BMC bioinformatics*, 5(1):1, 2004.

[14] Dr.Jürgen Zanghellini, David E. Ruckerbauer, Michael Hanscho, and Christian Jungreuthmayer. Elementary flux modes in a nutshell: Properties, calculation and applications. *Biotechnology Journal*, pages 1009–1016, 2013.

[15] Emilie Allart, Joachim Niehren, and Cristian Versari. Reaction Networks to Boolean Networks: Exact Boolean Abstraction for Linear Equation Systems. In *Preprint*, May 2021. URL https://hal.archives-ouvertes.fr/hal-02279942.

[16] Narendra Karmarkar. A new polynomial-time algorithm for linear programming. *Comb.*, 4(4):373–396, 1984. doi: 10.1007/BF02579150. URL https://doi.org/10.1007/BF02579150.

[17] K. Lotz, A. Hartmann, E. Grafahrend-Belau, and B.H. Schreiber, F.and Junker. Elementary flux modes, flux balance analysis, and their application to plant metabolism. *Plant Metabolism. Methods in Molecular Biology (Methods and Protocols)*, 2014.

[18] Costas D. Maranas and Ali R. Zomorrodi. *Flux Balance Analysis and LP Problems*, chapter 3, pages 53–80. Wiley-Blackwell, 2016. ISBN 9781119188902. doi: 10.1002/9781119188902.ch3. URL https://onlinelibrary.wiley.com/doi/abs/10.1002/9781119188902.ch3.

[19] Giuseppe Facchetti and Claudio Altafini. Partial inhibition and bilevel optimization in flux balance analysis. *BMC Bioinformatics*, pages 344–344, 2013.

[20] Patrick Cousot and Radhia Cousot. Systematic design of program analysis frameworks. In *POPL*, pages 269–282, 1979.

[21] François Fages and Sylvain Soliman. Abstract interpretation and types for systems biology. *Theor. Comput. Sci.*, 403(1):52–70, 2008.

[22] Vincent Danos, Jérôme Feret, Walter Fontana, Russell Harmer, and Jean Krivine. Abstracting the differential semantics of rule-based models: Exact and automated model reduction. In *LICS*, pages 362–381. IEEE Computer Society, 2010. ISBN 978-0-7695-4114-3.

[23] Stefan Schuster, Thomas Dandekar, and David A Fell. Detection of elementary flux modes in biochemical networks: a promising tool for pathway analysis and metabolic engineering. *Trends in biotechnology*, 17(2):53–60, 1999.

[24] Kenneth D. Forbus. Qualitative reasoning. In Allen B. Tucker, editor, *The Computer Science and Engineering Handbook*, pages 715–733. CRC Press, 1997. ISBN 0-8493-2909-4.

[25] David Avis. A revised implementation of the reverse search vertex enumeration algorithm. In *Polytopes—combinatorics and computation*, pages 177–198. Springer, 2000.

[26] Marco Terzer and Jörg Stelling. Large-scale computation of elementary flux modes with bit pattern trees. *Bioinformatics*, 24(19):2229–2235, 2008.

[27] Komei Fukuda and Alain Prodon. Double description method revisited. In *Franco-Japanese and Franco-Chinese Conference on Combinatorics and Computer Science*, pages 91–111. Springer, 1995.

[28] M Troffaes. pycddlib-a python wrapper for komei fukudals cddlib, 2018.
[29] BioComputing. Biocomputing's network-graph tool. http://researchers.lille.inria.fr/~niehren/BioComputing/Network-Graph/doc.html. 2018-07-10.
<figure><img src="image_17.png" /><figcaption>Figure 20: Graphical representation of the model that represents a part of the metabolism of the bacteria B. Subtilis, the branched chain amino-acid: Isoleucine, Leucine and Valine.</figcaption></figure>
## Appendix A. Proofs for Section 7 (First-Order Logic)

**Lemma 11.** For any $e \in \mathcal{E}_\Sigma$, $\Sigma$-algebra $S$, $n \ge 1$, and $\beta: V \to \text{dom}(S)^n$ with $\mathcal{V}(\phi) \subseteq V \subseteq \mathcal{V}$:

$$ \llbracket e \rrbracket^{\beta,S^n} = \llbracket (\Pi_1(e), \dots, \Pi_n(e)) \rrbracket^{\beta,S} $$

*Proof.* By induction on the structure of expressions in $\mathcal{E}_\Sigma$.

**Cas** of constants $c \in C$.

$$ \llbracket c \rrbracket^{\beta,S^n} = c^{S^n} = (c^S, \dots, c^S) = \llbracket (\Pi_1(c), \dots, \Pi_n(c)) \rrbracket^{\beta,S} $$

**Cas** of variables $x \in \mathcal{V}$.

$$ \llbracket x \rrbracket^{\beta,S^n} = \beta(x) = \beta((\pi_1(x), \dots, \pi_n(x))) = \llbracket (\Pi_1(x), \dots, \Pi_n(x)) \rrbracket^{\beta,S} $$

**Cas** of expressions $e_1 \odot e_2$ where $e_1, e_2 \in \mathcal{E}_\Sigma$ and $\odot \in \mathcal{F}^{(2)}$.

$$ \begin{align*} \llbracket e_1 \odot e_2 \rrbracket^{\beta,S^n} &= \bigcup \{ (s_1 \odot^{S^n} s_2) \mid s_j \in \llbracket e_j \rrbracket^{\beta,S^n} \} \\ \text{ind.hyp.} \quad &= \bigcup \{ (s_1 \odot^{S^n} s_2) \mid s_j \in \llbracket (\Pi_1(e_j), \dots, \Pi_n(e_j)) \rrbracket^{\beta,S} \} \\ &= \llbracket (\Pi_1(e_1) \odot^S \Pi_1(e_2), \dots, \Pi_n(e_1) \odot^S \Pi_n(e_2)) \rrbracket^{\beta,S} \end{align*} $$

□

**Proposition 12.** For any $\phi \in \mathcal{F}_\Sigma$, $\Sigma$-algebra $S$, and $n \ge 1$: $\text{sol}^{S^n}(\phi) = \text{n-sol}^S(\langle\phi\rangle^n)$.

*Proof.* By induction on the structure of formulas in $\mathcal{F}_\Sigma$. The base case of $\Sigma$-equations follows essentially from Lemma 11. Let $\beta$ be an assignment variables $\beta: V \to \text{dom}(S)^n$ with $V \subseteq \mathcal{V}$.

**Cas** $e = e'$ where $e, e' \in \mathcal{E}_\Sigma$.

$$ \begin{align*} \text{sol}^{S^n}(e = e') &= \{\beta \mid \llbracket e = e' \rrbracket^{\beta,S^n} = 1\} \\ \text{by prev. claim} \quad &= \{\beta \mid \llbracket \bigwedge_{i=1}^n \Pi_i(e) = \Pi_i(e') \rrbracket^{\beta,S} = 1\} \\ &= \{\beta \mid \llbracket \langle e = e' \rangle^n \rrbracket^{\beta,S} = 1\} \\ &= \text{n-sol}^S(\langle e = e' \rangle^n) \end{align*} $$

**Cas** $\phi \wedge \phi'$ where $\phi, \phi' \in \mathcal{F}_\Sigma$.

$$ \begin{align*} \text{sol}^{S^n}(\phi \wedge \phi') &= \{\beta \mid \llbracket \phi \wedge \phi' \rrbracket^{\beta,S^n} = 1\} \\ &= \{\beta \mid \llbracket \phi \rrbracket^{\beta,S^n} \wedge \llbracket \phi' \rrbracket^{\beta,S^n} = 1\} \\ \text{ind.hyp.} \quad &= \{\beta \mid \llbracket \langle \phi \rangle^n \rrbracket^{\beta,S} \wedge \llbracket \langle \phi' \rangle^n \rrbracket^{\beta,S} = 1\} \\ &= \{\beta \mid \llbracket \langle \phi \wedge \phi' \rangle^n \rrbracket^{\beta,S} = 1\} \\ &= \text{n-sol}^S(\langle \phi \wedge \phi' \rangle^n) \end{align*} $$

**Cas** $\neg\phi$ were $\phi \in \mathcal{F}_\Sigma$.

$$ \begin{align*} \text{sol}^{S^n}(\neg\phi) &= \{\beta \mid \llbracket \neg\phi \rrbracket^{\beta,S^n} = 1\} \\ &= \{\beta \mid \neg \llbracket \phi \rrbracket^{\beta,S^n} = 1\} \\ \text{ind.hyp.} \quad &= \{\beta \mid \neg \llbracket \langle \phi \rangle^n \rrbracket^{\beta,S} = 1\} \\ &= \{\beta \mid \neg \llbracket \neg\phi \rrbracket^{\beta,S} = 1\} \\ &= \{\beta \mid \llbracket \neg\phi \rrbracket^{\beta,S} = 1\} \\ &= \text{n-sol}^S(\neg\phi^n) \end{align*} $$
Cas $\exists x. \phi$ were $\phi \in \mathcal{F}_{\Sigma}$.

$$
\begin{align*}
\mathit{sol}^{S^n}(\exists x. \phi) &= \{\beta \mid [\exists x. \phi]^{\beta, S^n} = 1\} \\
&= \{\beta \mid \text{exists } s \in \mathit{dom}(S)^n. [\phi]^{\beta[x/s], S^n} = 1\} \\
\mathit{ind.hyp.} &= \{\beta \mid \text{exists } s \in \mathit{dom}(S)^n. [\langle\phi\rangle^n]^{\beta[x/s], S} = 1\} \\
&= \{\beta \mid [\exists x. \langle\phi\rangle^n]^{\beta, S} = 1\} \\
&= \{\beta \mid [\langle\exists x. \phi\rangle^n]^{\beta, S} = 1\} \\
&= n-\mathit{sol}^S(\langle\exists x. \phi\rangle^n)
\end{align*}
$$

□

**Lemma 14.** For any expression $o \in \mathcal{O}_{\Sigma}^n$ and variable assignment $\beta : V \to \mathit{dom}(S)^n$ with $V(o) \subseteq V \subseteq V$ we have $[\tilde{\nu}(o)]^{S,\nu(\beta)} = [o]^{\beta,S}$.

*Proof.* By induction on the structure of $\Sigma$-expressions $o \in \mathcal{O}_{\Sigma}^n$.

Cas of constants $c \in C$.

$$[\tilde{\nu}(c)]^{S,\nu(\beta)} = [c]^{\beta,S}$$

Cas $\pi_i(x)$ where $x \in \mathcal{V}$ and $1 \le i \le n$.

$$
\begin{align*}
[\tilde{\nu}(\pi_i(x))]^{S,\nu(\beta)} &= \{\nu(\beta)(\nu_i(x))\} \\
&= \{\pi_i(\beta(x))\} \\
&= [o]^{\beta,S}
\end{align*}
$$

Cas $o_1 \odot o_2$ where $o_1, o_2 \in \mathcal{O}_{\Sigma}^n$ and $\odot \in F^{(2)}$.

$$
\begin{align*}
[\tilde{\nu}(o_1 \odot o_2)]^{S,\nu(\beta)} &= [\tilde{\nu}(o_1) \odot \tilde{\nu}(o_2)]^{S,\nu(\beta)} \\
&= \cup \{(s_1 \odot^S s_2 \mid s_i \in [\tilde{\nu}(o_i)]^{S,\nu(\beta)})\} \\
\mathit{ind.hyp.} \qquad &= \cup \{(s_1 \odot^S s_2 \mid s_i \in [o_i]^{\beta,S}\} \\
&= [o_1 \odot o_2]^{\beta,S}
\end{align*}
$$

Cas $\pi_i(o_1, \dots, o_n)$ where $o_1, \dots, o_n \in \mathcal{O}_{\Sigma}^n$.

$$
\begin{align*}
[\tilde{\nu}(\pi_i(o_1, \dots, o_n))]^{S,\nu(\beta)} &= [\tilde{\nu}(o_i)]^{S,\nu(\beta)} \\
\mathit{ind.hyp.} \qquad &= [o_i]^{\beta,S} \\
&= [\pi_i(o_1, \dots, o_n)]^{\beta,S}
\end{align*}
$$

□

**Claim 16.** For any variable assignment $\beta : V \to \mathit{dom}(S)^n$ with $V \subseteq V$ and formula $\psi \in \mathcal{F}_{\Sigma}^n$ we have $[\tilde{\nu}(\psi)]^{S,\nu(\beta)} = [\psi]^{\beta,S}$.

*Proof.* The proof of the claim is by induction on the structure of $\Sigma$-formulas in $\mathcal{F}_{\Sigma}^n$.

Cas $o \doteq o'$ where $o, o' \in \mathcal{O}_{\Sigma}^n$.

$$
\begin{align*}
[o \doteq o']^{\beta,S} &= 1 && \Leftrightarrow [o]^{\beta,S} \cap [o]^{\beta,S} \neq \emptyset \\
\text{Lemma 14} \qquad & \Leftrightarrow [\tilde{\nu}(o)]^{S,\nu(\beta)} \cap [\tilde{\nu}(o)]^{S,\nu(\beta)} \neq \emptyset \\
& \Leftrightarrow [\tilde{\nu}(o) \doteq \tilde{\nu}(o')]^{S,\nu(\beta)} = 1 \\
& \Leftrightarrow [\tilde{\nu}(o \doteq o')]^{S,\nu(\beta)} = 1
\end{align*}
$$

Cas $\psi \wedge \psi'$ where $\psi, \psi' \in \mathcal{F}_{\Sigma}^n$.

$$
\begin{align*}
[\psi \wedge \psi']^{\beta,S} &= 1 && \Leftrightarrow [\psi]^{\beta,S} \wedge [\psi']^{\beta,S} = 1 \\
\mathit{ind.hyp} \qquad & \Leftrightarrow [\tilde{\nu}(\psi)]^{S,\nu(\beta)} \wedge [\tilde{\nu}(\psi)']^{S,\nu(\beta)} = 1 \\
& \Leftrightarrow [\tilde{\nu}(\psi) \wedge \tilde{\nu}(\psi)']^{S,\nu(\beta)} = 1 \\
& \Leftrightarrow [\tilde{\nu}(\psi \wedge \psi')]^{S,\nu(\beta)} = 1
\end{align*}
$$
Cas $\neg\psi$ where $\psi \in \mathcal{F}_{\Sigma}^{n}$.

$$
\begin{array}{l}
\llbracket \neg\psi \rrbracket^{\beta,S} = 1 \quad \Leftrightarrow \quad \llbracket \neg\psi \rrbracket^{\beta,S} = 1 \\
\text{ind.hyp.} \qquad \Leftrightarrow \quad \llbracket \tilde{\nu}(\psi) \rrbracket^{S,\nu(\beta)} = 1 \\
\qquad \Leftrightarrow \quad \llbracket \neg\tilde{\nu}(\psi) \rrbracket^{S,\nu(\beta)} = 1 \\
\qquad \Leftrightarrow \quad \llbracket \tilde{\nu}(\neg\psi) \rrbracket^{S,\nu(\beta)} = 1
\end{array}
$$

Cas $\exists x. \psi$ where $\psi \in \mathcal{F}_{\Sigma}^{n}$.

$$
\begin{array}{l}
\llbracket \exists x. \psi \rrbracket^{\beta,S} = 1 \quad \Leftrightarrow \quad \text{exist } s \in \operatorname{dom}(S)^n . \llbracket \psi \rrbracket^{S,\beta[x/s]} = 1 \\
\text{ind.hyp.} \qquad \Leftrightarrow \quad \text{exist } s \in \operatorname{dom}(S)^n . \llbracket \tilde{\nu}(\psi) \rrbracket^{S,\nu(\beta[x/s])} = 1 \\
\qquad \Leftrightarrow \quad \text{exist } s_1 \in \operatorname{dom}(S) \dots s_n \in \operatorname{dom}(S) . \llbracket \psi \rrbracket^{S,\nu(\beta[\nu_i(x)/s_i])} = 1 \\
\qquad \Leftrightarrow \quad \llbracket \exists \nu_1(x) \dots \exists \nu_n(x) . \tilde{\nu}(\psi) \rrbracket^{S,\nu(\beta)} = 1 \\
\qquad \Leftrightarrow \quad \llbracket \exists x. \tilde{\nu}(\psi) \rrbracket^{S,\nu(\beta)} = 1
\end{array}
$$

□

**Appendix B. Proofs for Section 8 (Difference Abstraction)**

**Lemma 21.** Let $h: S' \to \Delta$ be a $\Sigma$-abstraction and $\alpha: V \to \operatorname{dom}(S')$ and a variable assignment.
For any expression $e \in \mathcal{E}_{\Sigma}$ with $V(e) \subseteq V$: $h(\llbracket e \rrbracket^{S',\alpha}) \subseteq \llbracket e \rrbracket^{\Delta,h \circ \alpha}$.

*Proof.* The proof is by induction on the structure of expressions $e \in \mathcal{E}_{\Sigma}$. Let $\alpha$ be a variable assignment into $\operatorname{dom}(S')$. For any expressions $e = e_1 \odot e_2$ where $\odot \in F^{(2)}$ we have:

$$
\begin{align*}
h'([e_1 \odot e_2]^{S',\alpha}) &= h'([e_1]^{S',\alpha} \odot' [e_2]^{S',\alpha}) \\
&\subseteq h'([e_1]^{S',\alpha}) \odot^{\Delta} h'([e_2]^{S',\alpha}) & \text{homomorph.} \\
&\subseteq [e_1]^{\Delta,h\circ\alpha} \odot^{\Delta} [e_2]^{\Delta,h\circ\alpha} & \text{ind. hyp.} \\
&= [e_1 \odot e_2]^{\Delta,h\circ\alpha}
\end{align*}
$$

For any expression $e = x \in V$ we have:

$$
h'([x]^{S',\alpha}) = h'({\alpha(x)}) = [x]^{\Delta,h\circ\alpha}
$$

For constant expressions $e = c \in C$ we have:

$$
h'([c]^{S',\alpha}) = h(c^{S'}) = c^{\Delta} = [c]^{\Delta,h \circ \alpha} \quad \text{homomorphism}
$$

□