×

Complete semialgebraic invariant synthesis for the Kannan-Lipton orbit problem. (English) Zbl 1461.37028

Summary: The Orbit Problem consists of determining, given a matrix \(A\) on \(\mathbb{Q}^{d}\), together with vectors \(x\) and \(y\), whether the orbit of \(x\) under repeated applications of \(A\) can ever reach \(y\). This problem was famously shown to be decidable by R. Kannan and R. J. Lipton’s Orbit Problem [in: Proceedings of the 12th annual ACM symposium on theory of computing, STOC ’80. New York, NY: Association for Computing Machinery (ACM). 252–261 (1980; doi:10.1145/800141.804673); J. Assoc. Comput. Mach. 33, 808–821 (1986; Zbl 1326.68162)] in the 1980s. In this paper, we are concerned with the problem of synthesising suitable invariants \(\mathcal{P} \subseteq \mathbb{R}^{d}\), i.e., sets that are stable under \(A\) and contain \(x\) but not \(y\), thereby providing compact and versatile certificates of non-reachability. We show that whether a given instance of the Orbit Problem admits a semialgebraic invariant is decidable, and moreover in positive instances we provide an algorithm to synthesise suitable succinct invariants of polynomial size. Our results imply that the class of closed semialgebraic invariants is closure-complete: there exists a closed semialgebraic invariant if and only if \(y\) is not in the topological closure of the orbit of \(x\) under \(A\).

MSC:

37C35 Orbit growth in dynamical systems
37C79 Symmetries and invariants of dynamical systems
68U05 Computer graphics; computational geometry (digital and algorithmic aspects)

Citations:

Zbl 1326.68162

References:

[1] Bochnak, J., Coste, M., Roy, M.-F.: Real Algebraic Geometry, Volume 36 of A Series of Modern Surveys in Mathematics. Springer, Berlin (1998) · Zbl 0633.14016
[2] Cai, J.-Y.: Computing Jordan Normal Forms Exactly for Commuting Matrices in Polynomial Time. Technical report, SUNY at Buffalo (2000)
[3] Cassels, J.W.S.: An Introduction to Diophantine Approximation. Cambridge University Press, Cambridge (1965) · Zbl 0077.04801
[4] Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL, pp. 84-96. ACM Press (1978)
[5] Cai, J.-Y., Lipton, R.J., Zalcstein, Y.: The complexity of the A B C problem. SIAM J. Comput. 29(6), 1878-1888 (2000) · Zbl 0967.20029 · doi:10.1137/S0097539794276853
[6] Colón, M.: Polynomial approximations of the relational semantics of imperative programs. Sci. Comput. Program. 64(1), 76-96 (2007) · Zbl 1171.68541 · doi:10.1016/j.scico.2006.03.004
[7] van den Dries, LPD: Tame Topology and O-minimal Structures. London Mathematical Society Lecture Note Series. Cambridge University Press, Cambridge (1998) · Zbl 0953.03045 · doi:10.1017/CBO9780511525919
[8] Ge, G.: Testing equalities of multiplicative representations in polynomial time. In: SFCS, pp. 422-426. IEEE Computer Society (1993)
[9] Harrison, M.A.: Lectures on Linear Sequential Machines. Academic Press, New York-Londres (1969) · Zbl 0212.34002
[10] Kannan, R., Lipton, R.J.: The orbit problem is decidable. In: STOC, pp. 252-261 (1980)
[11] Kannan, R., Lipton, R.J.: Polynomial-time algorithm for the orbit problem. J. ACM 33(4), 808-821 (1986) · Zbl 1326.68162 · doi:10.1145/6490.6496
[12] Masser, D.W.: Linear relations on algebraic groups. In: Baker, A. (ed.) New Advances in Transcendence Theory, pp 248-262. Cambridge University Press, Cambridge (1988) · Zbl 0656.10031
[13] Mignotte, M.: Some useful bounds. In: Computer Algebra, Volume 4 of Computing Supplementum 4. Springer, Vienna (1982) · Zbl 0498.12019
[14] Müller-Olm, M., Seidl, H.: A note on Karr’s algorithm. In: ICALP, Volume 3142 of Lecture Notes in Computer Science, pp. 1016-1028. Springer (2004) · Zbl 1099.68022
[15] Müller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: POPL, pp. 330-341. ACM (2004) · Zbl 1325.68068
[16] Ouaknine, J., Worrell, J.: Ultimate positivity is decidable for simple linear recurrence sequences. In: ICALP, pp. 330-341 (2014) · Zbl 1410.11135
[17] Tao, T.: Structure and Randomness. AMS (2008) · Zbl 1245.00024
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.