Invariants for Continuous Linear Dynamical Systems
Continuous linear dynamical systems are used extensively in mathematics, computer science, physics, and engineering to model the evolution of a system over time. A central technique for certifying safety properties of such systems is by synthesising inductive invariants. This is the task of finding a set of states that is closed under the dynamics of the system and is disjoint from a given set of error states. In this paper we study the problem of synthesising inductive invariants that are definable in o-minimal expansions of the ordered field of real numbers. In particular, assuming Schanuel’s conjecture in transcendental number theory, we establish effective synthesis of o-minimal invariants in the case of semi-algebraic error sets. Without using Schanuel’s conjecture, we give a procedure for synthesizing o-minimal invariants that contain all but a bounded initial segment of the orbit and are disjoint from a given semi-algebraic error set. We further prove that effective synthesis of semi-algebraic invariants that contain the whole orbit, is at least as hard as a certain open problem in transcendental number theory.
Invariants
continuous linear dynamical systems
continuous Skolem problem
safety
o-minimality
Theory of computation~Logic and verification
Computing methodologies~Algebraic algorithms
Mathematics of computing~Continuous mathematics
Mathematics of computing~Continuous functions
Theory of computation~Finite Model Theory
Software and its engineering~Formal software verification
107:1-107:15
Track B: Automata, Logic, Semantics, and Theory of Programming
A full version of the paper is available at [Shaull Almagor et al., 2020] https://arxiv.org/abs/2004.11661.
Shaull
Almagor
Shaull Almagor
Department of Computer Science, Technion, Haifa, Israel
https://orcid.org/0000-0001-9021-1175
Supported by a European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 837327.
Edon
Kelmendi
Edon Kelmendi
Department of Computer Science, Oxford University, UK
Joël
Ouaknine
Joël Ouaknine
Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany
Department of Computer Science, Oxford University, UK
Supported by ERC grant AVS-ISS (648701) and DFG grant 389792660 as part of TRR 248 (see https://perspicuous-computing.science).
James
Worrell
James Worrell
Department of Computer Science, Oxford University, UK
Supported by EPSRC Fellowship EP/N008197/1.
10.4230/LIPIcs.ICALP.2020.107
Shaull Almagor, Dmitry Chistikov, Joël Ouaknine, and James Worrell. O-minimal invariants for linear loops. In 45th International Colloquium on Automata, Languages, and Programming ICALP, pages 1-14. Schloss Dagstuhl, 2018.
Shaull Almagor, Dmitry Chistikov, Joël Ouaknine, and James Worrell. O-minimal invariants for discrete-time dynamical systems, 2020.
Shaull Almagor, Edon Kelmendi, Joël Ouaknine, and James Worrell. Invariants for continuous linear dynamical systems, 2020. URL: http://arxiv.org/abs/2004.11661.
http://arxiv.org/abs/2004.11661
Rajeev Alur. Principles of cyber-physical systems. MIT Press, 2015.
Hirokazu Anai and Volker Weispfenning. Reach set computations using real quantifier elimination. In International Workshop on Hybrid Systems: Computation and Control, pages 63-76. Springer, 2001.
Paul C. Bell, Jean-Charles Delvenne, Raphaël M. Jungers, and Vincent D. Blondel. The continuous skolem-pisot problem. Theor. Comput. Sci., 411(40–42):3625–3634, September 2010.
Mireille Broucke. Reachability analysis for hybrid systems with linear dynamics. Mathematical Theory of Networks and Systems (MTNS’02), 2002.
John W.S. Cassels. An Introduction to Diophantine Approximation. Cambridge University Press, 1965.
Ventsislav Chonev, Joël Ouaknine, and James Worrell. On recurrent reachability for continuous linear dynamical systems. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, pages 515-524, 2016.
Ventsislav Chonev, Joël Ouaknine, and James Worrell. On the skolem problem for continuous linear dynamical systems. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2016.
Peter Franek, Stefan Ratschan, and Piotr Zgliczynski. Quasi-decidability of a fragment of the first-order theory of real numbers. Journal of Automated Reasoning, 57(2):157-185, 2016.
Khalil Ghorbal, Andrew Sogokon, and André Platzer. A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets. Comput. Lang. Syst. Struct., 47:19-43, 2017.
Sumit Gulwani and Ashish Tiwari. Constraint-based approach for analysis of hybrid systems. In Computer Aided Verification, 20th International Conference, CAV 2008, Proceedings, volume 5123 of Lecture Notes in Computer Science, pages 190-203. Springer, 2008.
Emmanuel Hainry. Reachability in linear dynamical systems. In Arnold Beckmann, Costas Dimitracopoulos, and Benedikt Löwe, editors, Logic and Theory of Algorithms, pages 241-250. Springer Berlin Heidelberg, 2008.
Gerardo Lafferriere, George J. Pappas, and Sergio Yovine. Symbolic reachability computation for families of linear vector fields. J. Symb. Comput., 32(3):231-253, 2001.
Jiang Liu, Naijun Zhan, and Hengjun Zhao. Computing semi-algebraic invariants for polynomial dynamical systems. In Proceedings of the 11th International Conference on Embedded Software, EMSOFT 2011, pages 97-106. ACM, 2011.
Angus Macintyre. Turing meets schanuel. Annals of Pure and Applied Logic, 167(10):901-938, 2016.
Angus Macintyre and Alex J. Wilkie. On the decidability of the real exponential field. In Piergiorgio Odifreddi, editor, Kreiseliana. About and Around Georg Kreisel, pages 441-467. A K Peters, 1996.
David W Masser. Linear relations on algebraic groups. New Advances in Transcendence Theory, pages 248-262, 1988.
Enric Rodríguez-Carbonell and Ashish Tiwari. Generating polynomial invariants for hybrid systems. In Hybrid Systems: Computation and Control, 8th International Workshop, HSCC 2005, Proceedings, volume 3414 of Lecture Notes in Computer Science, pages 590-605. Springer, 2005.
Andrew Sogokon, Khalil Ghorbal, Paul B. Jackson, and André Platzer. A method for invariant generation for polynomial continuous systems. In Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI, Proceedings, volume 9583 of Lecture Notes in Computer Science, pages 268-288. Springer, 2016.
Andrew Sogokon and Paul B Jackson. Direct formal verification of liveness properties in continuous and hybrid dynamical systems. In International Symposium on Formal Methods, pages 514-531. Springer, 2015.
Thomas Sturm and Ashish Tiwari. Verification and synthesis using real quantifier elimination. In Symbolic and Algebraic Computation, International Symposium, ISSAC 2011, Proceedings, pages 329-336. ACM, 2011.
Alfred Tarski. A decision method for elementary algebra and geometry. RAND Corporation, R-109, 1951.
Lou van den Dries, Angus Macintyre, and David Marker. The elementary theory of restricted analytic fields with exponentiation. Annals of Mathematics, 140(1):183-205, 1994.
Lou Van den Dries, Chris Miller, et al. Geometric categories and o-minimal structures. Duke Math. J, 84(2):497-540, 1996.
A. J. Wilkie. Model completeness results for expansions of the ordered field of real numbers by restricted pfaffian functions and the exponential function. Journal of the American Mathematical Society, 9(4):1051-1094, 1996.
Shaull Almagor, Edon Kelmendi, Joël Ouaknine, and James Worrell
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode