Linear and Affine Escape Problem Over the Reals

Linear and Affine Escape Problem Over the Reals Margret K Tembo and Eike Neumann Swansea University,UK Dynamical systems arise in a wide range of areas, such as control theory, economics, graphics, signal processing, and program verification. When such systems are specified by rational or algebraic data, safety and liveness verification are only known to be decidable in very restricted cases. For example, it is an open problem whether it is decidable if a given point eventually enters a hyperplane under the iteration of a rational matrix, and it is known that an analogous problem for piecewise-linear functions is undecidable. Neumann [2] has shown that over real data, the former problem becomes as close to decidable as one can hope it to be, providing some preliminary evidence that computable analysis is a suitable framework for system verification. Our ultimate goal is to solve termination and escape questions for rich classes of discrete-time dynamical systems such as linear constraint loops, piecewise-linear updates x7→ Aix+bi, or polynomial updates x7→ P(x) whose decidability over the rationals is largely open or known to not hold true. To make progress, we adopt a real-data, Type-2 approach and begin with the simplest nontrivial case: linear loops with polyhedral guards. We focus on the following decision problem. Let K∈ {Q,R}. Given A∈Kn×n, b ∈Kn, P ={x∈Kn:Bx>η},B∈Km×n, η ∈Km, decide whether every trajectory of the linear (resp. affine) update xk+1 =Axkresp. xk+1 =Axk+bstarting in P, eventually exits P. When A, b, B, η are all rational (i.e. over Q), Tiwari [4] proved this polyhedral escape problem decidable for both the linear and affine (b= 0) cases. Allowing arbitrary real data makes the problem undecidable for trivial continuity reasons. However, we show that under Type-2 computability both the linear and affine escape problems admit maximal partial algorithms: partial algorithms which terminate in finite time exactly on the robust problem instances — those instances whose true answer remains invariant under sufficiently small perturbations of the real data — and diverge otherwise. Thus, we establish a robust semidecision result over Rfor the base case of linear loops, paving the way toward handling more complex piecewise-linear or polynomial systems. Our proof requires rather different techniques than Tiwari’s original result over the rationals. The latter heavily relies on operations that are not computable over real data, most notably the real Jordan normal form. We prove our result by characterising the robust instances of the problem via first-order formulas where all universal quantification takes place over uniformly computably compact sets, and all existential quantification takes place over uniformly computably overt sets. Since such formulas are known to be semidecidable, we immediately obtain an algorithm. 1 In the linear case, detecting escape reduces to universally quantifying over the computably compact set of nonnegative eigenvalues and their unit eigenspaces. For trapped instances, we existentially quantify over the computably overt set of positive odd-multiplicity eigenvalues. The following theorem statements capture these necessary and sufficient conditions in exact form. An instance (A,B) is robustly escaping if and only if ∀λ∈σ≥0(A)∀v∈Sn−1: (Av=λv) =⇒ ∃ i∈ {1, . . . , m}:Biv < 0, where σ≥0(A) is the set of nonnegative real eigenvalues of A, and each Biis the i-th row of B. It is robustly trapped if and only if ∃λ∈σodd >0(A)∀v∈Sn−1: (Av=λv) =⇒∀iBiv > 0∨ ∀iBiv < 0, where σodd >0(A) denotes positive eigenvalues of odd multiplicity. An instance (A, b, B, η) of the affine problem with 1 /∈σ(A) is robustly escaping if both ∀λ∈σ≥1(A)∀v∈Sn−1: (Av=λv) =⇒ ∃ iBiv < 0 Linear and ∃i∀x: (I−A)x=b=⇒Bix<ηiFixed-subspace hold. Dually, it is robustly trapped if either ∃λ∈σ>1(A)∀v∈Sn−1: (Av=λv) =⇒(∀iBiv > 0∨ ∀iBiv < 0) or ∃x; (I−A)x=b∀i:Bix>ηiholds. In future work, we intend to solve the remaining case of affine problems that may admit 1 as an eigenvalue. References [1] JP Bell and S Gerhold. The positivity set of a recurrence sequence, 2005. [2] Eike Neumann. Decision problems for linear recurrences involving arbitrary real numbers. Logical Methods in Computer Science, 17, 2021. [3] Eike Neumann. On the complexity of robust eventual inequality testing for c-finite functions. In International Conference on Reachability Problems, pages 98–112. Springer, 2023. [4] Ashish Tiwari. Termination of linear programs. In Computer Aided Verification: 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004. Proceedings 16, pages 70–82. Springer, 2004. [5] Klaus Weihrauch. Computable Analysis: An Introduction. Texts in Theoretical Computer Science. Springer, 2000. 2