Termination analysis for linear constraint loops using Z3

We work with two real-valued variables \(x,y\). Given \(A \in \mathbb{Q}^{k \times 4}\) and \(b \in \mathbb{Q}^k\), the program decides whether the non-deterministic loop \(A \cdot (x, y, x', y') \ge b\) admits an infinite trajectory. Let \(K \subseteq \mathbb{R}^4\) be the transition relation of the loop.

Guilmant et al. (The 2-Dimensional Constraint Loop Problem Is Decidable, ICALP 2024) show that such a loop does not terminate if and only if there exist a matrix \(M \in \mathbb{R}^{2 \times 2}\), a closed convex cone \(C \subseteq \mathbb{R}^2\), and vectors \(v,w \in \mathbb{R}^2\) such that

\[ \begin{aligned} M \cdot C &\subseteq C \\ (u, M u) &\in \operatorname{rec}(K) \quad \text{for every } u \in C \\ (v,w) &\in K \\ w-v &\in C \end{aligned} \]

where \(\operatorname{rec}(K) = \{(x,y,x',y') \colon A \cdot (x,y,x',y') \ge 0\}\) is the recession cone of \(K\). The loop then has the infinite run

\[ v,\quad w,\quad w + M(w-v),\quad w + M(w-v) + M^2(w-v),\quad \ldots \]

We give a polynomial-time algorithm to check this condition (arXiv link coming soon) and implement it using Z3.

Must have 4 columns, with each row on a new line, of integers or rationals \(p/q\) (without any spaces around /) separated by commas.

Integers or rationals \(p/q\) in one line, separated by commas.