Reachability for Multi-Priced Timed Automata with Positive and Negative Rates

The proposition was proved in [12] under the assumption that observers have nonnegative slope. The general case follows easily. Indeed, given an arbitrary MPTA $𝒜=⟨L,{\mathrm{\ell }}_0,L_f,𝒳,𝒴,E,R⟩$, we define a new MPTA ${𝒜}^{\prime }$, differing from $𝒜$ only in its set of observers and rate function, such that all observers in ${𝒜}^{\prime }$ have non-negative rates. The set of observers of ${𝒜}^{\prime }$ is ${𝒴}^{\prime }:=\{y_{+},y_{-}:y\in 𝒴\}$ and the rate function $R^{\prime }$ is given by

for all $y\in 𝒴$ and all $\mathrm{\ell }\in L$.

Define $\mathrm{\Phi }:{\mathbb{Z}}^{{𝒴}^{\prime }}\to {\mathbb{Z}}^{𝒴}$ by $\mathrm{\Phi }(\gamma )(y)=\gamma (y_{+})-\gamma (y_{-})$. If a run $\rho$ of ${𝒜}^{\prime }$ has cost vector $\gamma$ then $\rho$ has cost vector $\mathrm{\Phi }(\gamma )$ considered as a run of $𝒜$. Thus if we define ${𝒮}_{𝒜}:=\mathrm{\Phi }({𝒮}_{{𝒜}^{\prime }})$, where $\mathrm{\Phi }$ has been lifted pointwise to a linear map $\mathrm{\Phi }:{({\mathbb{Z}}^{{𝒴}^{\prime }})}^{d+1}\to {({\mathbb{Z}}^{𝒴})}^{d+1}$, then ${𝒮}_{𝒜}$ satisfies the requirements of the proposition. $◀$

The following is immediate from Proposition 1.

In the following two sections we analyse systems of constraints of the above form, obtaining a general result that allows us to solve the Gap Domination Problem.

We reduce from the following version of Hilbert’s 10th Problem (see [12, Proposition 1]): given a finite system $𝒮$ of equations in variables $x_1,\mathrm{\dots },x_n$, with each equation either having the form $x_i=x_j+x_k$ or $x_i=x_j{x}_k$, determine whether $𝒮$ has a solution in the set of strictly positive integers.

The reduction involves transforming the system $𝒮$ into an equisatisfiable MIB system ${𝒮}^{\prime }$ over a set of integer variables $x_0,\mathrm{\dots },x_n\ge 0$ (i.e, the variables of $𝒮$ plus a new variable $x_0$) and real variables $y_1,\mathrm{\dots },y_n\ge 0$. The construction is such that every solution of $𝒮$ extends to a solution of ${𝒮}^{\prime }$ and, conversely, every solution of ${𝒮}^{\prime }$ restricts to a solution of $𝒮$.

The system ${𝒮}^{\prime }$ includes equations $x_0=1$ and $x_i{y}_i=1$ for $i=1,\mathrm{\dots },n$. The linear equations $x_i=x_j+x_k$ from $𝒮$ are carried over to ${𝒮}^{\prime }$ and, for each equation $x_i=x_j{x}_k$ in $𝒮$, we include an equation $(x_j+x_k)y_i=x_0(y_j+y_k)$ in $𝒮$. The latter is equivalent to $\frac{x_j+x_k}{x_i}=\frac{1}{x_j}+\frac{1}{x_k}$ in the presence of the equations $x_i{y}_i=x_j{y}_j=x_k{y}_k=1$ and $x_0=1$, which in turn is clearly equivalent to $x_i=x_j{x}_k$. By adding constraints $0\le y_i\le 1$ for $i=1,\mathrm{\dots },n$ we furthermore make ${𝒮}^{\prime }$ bounded without affecting the integrity of the reduction. $◀$

The proof is by reduction from the same variant of Hilbert’s Tenth Problem as in the proof of Proposition 3. Recall that an instance of this problem comprises a system $𝒮$ of equations in positive-integer variables $x_1,\mathrm{\dots },x_n$, with each equation having the form either $x_i=x_j+x_k$ or $x_i=x_j{x}_k$, where $i,j,k\in \{1,\mathrm{\dots },n\}$. Given such a system, we construct an MIB system ${𝒮}^{\prime }$ over integer variables $x_0,\mathrm{\dots },x_{n+1}$ and real variables $y_0,\mathrm{\dots },y_{n+1}$ such that every satisfying assignment of $𝒮$ extends to a satisfying assignment of ${𝒮}^{\prime }$ with slack $\frac{1}{2}$ and every satisfying assignment of ${𝒮}^{\prime }$ restricts to a satisfying assignment of $𝒮$.

We include the equations $x_0=1$ and $y_0=1$ in ${𝒮}^{\prime }$. Each linear equation $x_i=x_j+x_k$ in $𝒮$ is carried over to ${𝒮}^{\prime }$. For each equation $x_i=x_j{x}_k$ in $𝒮$ we include the inequality $|x_i{y}_0-x_j{y}_k|\le \frac{1}{2}$ in ${𝒮}^{\prime }$. We then add the following collection of constraints to ${𝒮}^{\prime }$ for all $i\in \{1,\mathrm{\dots },n+1\}$ that intuitively force $x_i$ and $y_i$ to be very close together:

1. 1.

   $|x_i{y}_0-x_0{y}_i|\le 1$;

2. 2.

   $|x_{n+1}{y}_i-x_i{y}_{n+1}|\le 1$;

3. 3.

   $x_{n+1}{y}_0\ge 4(x_0+x_i)(y_0+y_i)+1$.

A satisfying valuation of $𝒮$ can be extended to a valuation that satisfies ${𝒮}^{\prime }$ with slack $\frac{1}{2}$ by setting $x_0:=1$, $x_{n+1}:=4{\max }_{i\in \{1,\mathrm{\dots },n\}}{(1+x_i)}^2+1$, and $y_i:=x_i$ for $i=0,\mathrm{\dots },n+1$.

Conversely, we claim that every satisfying valuation of ${𝒮}^{\prime }$ (with no assumption on the slack) restricts to a satisfying valuation of $𝒮$. Indeed, by Item 2, above, for all $k\in \{1,\mathrm{\dots },n\}$ we have

By Items 1 and 3, this entails that for all $j\in \{1,\mathrm{\dots },n\}$,

and hence $|x_j{x}_k-x_j{y}_k|\le \frac{1}{4}$. Combined with $|x_i-x_j{y}_k|\le \frac{1}{2}$ we conclude that $|x_i-x_j{x}_k|\le \frac{3}{4}$ and hence $x_i=x_j{x}_k$. $◀$

It is shown in [12, Theorem 6] how to solve the Gap Satisfiabililty Problem for a subclass of MIB systems, which we here call positive. A positive MIB system has the form

with all coefficients of $A_i$ being non-negative rational for $i=1,\mathrm{\dots },{\mathrm{\ell }}_2$. This variant can be solved by a naive relaxing and rounding procedure, which does not require the boundedness assumption. However, while suffiicent to handle MPTA with non-negative rates, positive MIB appear insufficient for the case of MPTA with both positive and negative rates.

A necessary condition that ${\mathrm{width}}_{𝒖}(P)\ge c$ is that $P$ be non-empty and hence, since it lies in the positive orthant, contain a vertex. Now each vertex of $P$, being the intersection of $n$ linearly independent bounding hyperplanes, has the form $B^{-1}{𝒃}^{\prime }$, where $B$ is a non-singular $n\times n$ sub-matrix of $\left(\begin{array}{c}A\\ I_n\end{array}\right)$, where $I_n$ denotes the identity matrix of dimension $n$, and ${𝒃}^{\prime }$ is a corresponding sub-vector of $\left(\begin{array}{c}𝒃\\ \mathrm{𝟎}\end{array}\right)$. Hence the vertices of $P$ are definable by quantifier-free formulas.

Assume that $P$ contains a vertex. Then ${\mathrm{width}}_{𝒖}(P)$ is infinite if and only if either $𝒖$ or $-𝒖$ lie in the recession cone of $P$, for which a sufficient and necessary condition is that $A𝒖\ge \mathrm{𝟎}$ or $A𝒖\le \mathrm{𝟎}$. If ${\mathrm{width}}_{𝒖}(P)$ is finite then there exist two vertices ${𝒙}_0,{𝒙}_1$ of $P$ such that ${\mathrm{width}}_{𝒖}(P)={𝒖}^{\top }({𝒙}_0-{𝒙}_1)$. The proposition follows by combining the above observations. $◀$

We now commence the detailed description of the relaxation construction. The input is a bounded MIB program $𝒮$ in standard form (3) and a slack $\epsilon >0$. Assume that $𝒮$ has at least one non-linear constraint. We start with the observation that for a given $𝒚\in {ℝ}^n$ the system (3) admits a solution $𝒙\in {\mathbb{Z}}^m$ if and only if the polyhedral set

contains an integer point.

Let $H$ be an upper bound of the absolute value of the integer constants in the system (3). Since $𝒮$ is bounded, by [14, Lemma 3.1.25] the set $\{𝒚\in {ℝ}^n:D𝒚\le 𝒆\}$ is contained in the ball of radius ${\kappa }_1:=m^{1/2}{H}^{(m^2+m)}$ centred at the origin.

For a matrix $A$, let $\Vert A\Vert$ denote the spectral norm. Recall that if $A$ has entries of absolute value at most $H$ and has $m$ columns then $\Vert A\Vert \le \sqrt{m}H$. Now write

and define , where $\omega (m)$ is as in Theorem 7. Write $U=\{{𝒖}_1,\mathrm{\dots },{𝒖}_s\}$ and consider the following relaxed system ${𝒮}^{\prime }$ of linear and bilinear constraints in exclusively real variables (where the notation $P(𝒚)$ is as in (4) and we use Proposition 8 to formulate the constraint ${\mathrm{width}}_{{𝒖}_j}(P(𝒚))\ge \omega (m)$):

Let ${𝒙}^{\ast },{𝒚}^{\ast }$ be a solution of the system ${𝒮}^{\prime }$, as shown in (6). Consider the set $P({𝒚}^{\ast })$ as defined in (4). By construction we have

But from the fact ${𝒙}^{\ast }$ satisfies each constraint ${𝒙}^{\top }{A}_i{𝒚}^{\ast }+{𝒃}_i^{\top }{𝒚}^{\ast }\le c_i$ with slack $\epsilon$ and that ${𝒙}^{\ast }\ge \mathrm{𝟏}$, we see that the ball $B_{\delta }({𝒙}^{\ast })$ is contained in $P({𝒚}^{\ast })$, for $\delta$ as defined in (5). It follows that

for all $𝒖\notin U$. Together with (7), we have that $\mathrm{width}(P({𝒚}^{\ast }))\ge \omega (m)$ and hence, by Theorem 7, $P({𝒚}^{\ast })$ contains an integer point. This entails that the original system $𝒮$ is satisfiable. $◀$

Assume that ${𝒮}^{\prime }$ has no solution. Let ${𝒙}^{\ast }\in {\mathbb{Z}}^m$ and ${𝒚}^{\ast }\in {ℝ}^n$ be a solution of $𝒮$ with slack $\epsilon$. If some component of ${𝒙}^{\ast }$ is zero then we are done, so we may suppose that ${𝒙}^{\ast }\ge \mathrm{𝟏}$. By assumption, ${𝒙}^{\ast },{𝒚}^{\ast }$ is not a solution of ${𝒮}^{\prime }$ and so it must hold that

where $P({𝒚}^{\ast })$ is as defined in (4).

Let $𝒖\in U$ be the vector achieving the minimum on the left-hand side of (8). We will exhibit an upper bound on $|{𝒖}^{\top }{𝒙}^{\ast }|$ that does not depend on ${𝒚}^{\ast }$.

Assume first that $P({𝒚}^{\ast })$ contains the origin. Then by (8),

Assume now that $P({𝒚}^{\ast })$ does not contain the origin. Let $L$ be the line segment connecting the origin to ${𝒙}^{\ast }$, and denote by $𝒙$ the point at which $L$ intersects the boundary of $P({𝒚}^{\ast })$. Then we have ${𝒙}^{\ast }-𝒙=\lambda 𝒙$ for some $\lambda >0$. Moreover, since $𝒙$ lies on the boundary of $P({𝒚}^{\ast })$ there exists $i_0\in \{1,\mathrm{\dots },\mathrm{\ell }\}$ such that

i.e., one of inequalities that define $P({𝒚}^{\ast })$ is tight at $𝒙$. But since ${𝒙}^{\ast },{𝒚}^{\ast }$ satisfies $𝒮$ with slack $\epsilon$, we also have that ${({𝒙}^{\ast })}^{\top }{A}_{i_0}{𝒚}^{\ast }+{𝒃}_{i_0}^{\top }{𝒚}^{\ast }\le c_{i_0}-\epsilon$. Subtracting Equation (9) from the previous inequality gives

Since $\epsilon ,\lambda >0$ this entails that and hence

We deduce that

Thus, defining

we have $|{𝒖}^{\top }{𝒙}^{\ast }|\le {\kappa }_2$.

In summary, we have that $|{𝒖}^{\top }{𝒙}^{\ast }|\le {\kappa }_2$ for every integer point ${𝒙}^{\ast }$ of $P({𝒚}^{\ast })$, as required in the proposition. $◀$

The procedure to solve the Gap Satisfiability Problem is as follows. Consider an instance of the problem, consisting of an MIB system in the form (3) and slack $\epsilon >0$. If there are no non-linear constraints then the problem instance is just a system of linear inequalities in real and integer variables, whose satisfiability is straightforward to discern. Thus we may assume that there is at least one non-linear constraint. We construct the associated relaxed system ${𝒮}^{\prime }$, which has the form (6). Using a decision procedure for the existential theory of real-closed fields we determine whether the system ${𝒮}^{\prime }$ is satisfiable.

If ${𝒮}^{\prime }$ is satisfiable then Proposition 9 guarantees that the original MIB system $𝒮$ is also satisfiable. We can then find a satisfying assignment of $𝒮$ by enumerating over all values ${𝒙}^{\ast }\in {\mathbb{Z}}^m$ and solving a linear program to decide whether there exists ${𝒚}^{\ast }\in {ℝ}^n$ such that ${𝒙}^{\ast },{𝒚}^{\ast }$ satisfies $𝒮$.

If the relaxed problem has no satisfying assignment then Proposition 10 furnishes a finite set $ℰ$ of linear equations of the form ${𝒖}^{\top }𝒙=b$, with coefficients $𝒖\in {\mathbb{Z}}^m$ and $b\in \mathbb{Z}$, such that for any solution ${𝒙}^{\ast }\in {\mathbb{Z}}^m,{𝒚}^{\ast }\in {ℝ}^n$ of (2) that has slack $\epsilon$, the integer part ${𝒙}^{\ast }$ satisfies an equation in $ℰ$. We iterate through all such equations ${𝒖}^{\top }𝒙=b$ and in each case we apply Proposition 5 to write

as a linear set $L(B,P)$ for some finite set $B\subseteq {\mathbb{Z}}^m$ and matrix $P\in {\mathbb{Z}}^{m\times m-1}$. Then for each vector $𝒘\in B$, we apply the change of variables $𝒙=𝒘+P𝒛$ to obtain a MIB system in one fewer integer variable to which we can recursively apply the procedure to determine satisfiability. $◀$

In the following result we retrace the proof of Theorem 11, this time keeping track of the size of the integers involved. We thereby obtain an upper bound on the smallest satisfying assignment, showing that the gap satisfiability problem can be solved in nondeterministic exponential time.

We first analyse the effect of a single variable-elimination step on the size of the integers in the system (3). Recall that to eliminate an integer variable we assert a linear equation ${𝒖}^{\top }𝒙=b$, where $\Vert 𝒖\Vert \le \frac{2w(m)}{\delta }$ and $|b|\le {\kappa }_2$. Combining the lower bound $\delta \ge \frac{\epsilon }{m^{1/2}H{\kappa }_1}$ from (5), the definition ${\kappa }_1:=m^{1/2}{H}^{(m^2+m)}$, the definition of ${\kappa }_2$ in (11), and the bound $\omega (m)=O(m^{3/2})$, we obtain that $\Vert 𝒖\Vert ,|b|={\kappa }_3^{O(1)}$, for ${\kappa }_3:=\left(\frac{m{H}^{m^2}}{\epsilon }\right)$.

Employing Proposition 5, the equation ${𝒖}^{\top }𝒙=b,𝒙\ge \mathrm{𝟎}$, determines a substitution $𝒙=P𝒛+𝒘$ in which the elements of $P$ and $𝒘$ have absolute value at most ${\kappa }_3^{O(m)}$. Since there are $m$ integer variables, the constants appearing over all MIB instances arising through the process of variable elimination have absolute value at most ${\kappa }_3^{O(m^2)}$.

Consider a version of the relaxed system (6) in which the integer constants have magnitude at most ${\kappa }_3^{O(m^2)}$. For the purposes of our complexity analysis we augment the system with a new variable $r$ and constraints $r\ge \Vert 𝒙\Vert +1$ and $r\ge \Vert 𝒘\pm w(m)𝒖\Vert$ for each vertex $𝒘$ of the polyhedron $P(𝒚)$ (as defined in (4)) and $𝒖\in U$. The integer constants in the resulting system have absolute value at most ${\kappa }_3^{O(m^3)}$ by Hadamard’s determinant inequality. By construction, if ${𝒙}^{\ast },{𝒚}^{\ast }$ is a satisfying assignment of (6) then the convex set $\{𝒙\in P({𝒚}^{\ast }):\Vert 𝒙\Vert \le r\}$ has lattice width at most $w(m)$ and hence contains an integer point. By Proposition 6 an upper bound for $r$ is $2^{{\kappa }_3^{O(m^3(m+n))}}$, which concludes the proof. $◀$

Proposition 1 and Corollary 1 give an exponential-time Turing reduction of the Gap Domination Problem for MPTA to the Gap Satisfiability Problem for bounded MIB systems, such that resulting instances of the Gap Satisfiability Problem have size polynomial in that of the input MPTA. We thus obtain our second main result.