Document Open Access Logo

Invariants for Continuous Linear Dynamical Systems

Authors Shaull Almagor , Edon Kelmendi, Joël Ouaknine, James Worrell

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2020.107.pdf
  • Filesize: 0.54 MB
  • 15 pages

Document Identifiers

Author Details

Shaull Almagor
  • Department of Computer Science, Technion, Haifa, Israel
Edon Kelmendi
  • Department of Computer Science, Oxford University, UK
Joël Ouaknine
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany
  • Department of Computer Science, Oxford University, UK
James Worrell
  • Department of Computer Science, Oxford University, UK

Funding

  • Almagor, Shaull: Supported by a European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 837327.
  • Ouaknine, Joël: Supported by ERC grant AVS-ISS (648701) and DFG grant 389792660 as part of TRR 248 (see https://perspicuous-computing.science).
  • Worrell, James: Supported by EPSRC Fellowship EP/N008197/1.

Cite AsGet BibTex

Shaull Almagor, Edon Kelmendi, Joël Ouaknine, and James Worrell. Invariants for Continuous Linear Dynamical Systems. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 107:1-107:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.ICALP.2020.107

Abstract

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.

Subject Classification

ACM Subject Classification
  • 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
Keywords
  • Invariants
  • continuous linear dynamical systems
  • continuous Skolem problem
  • safety
  • o-minimality

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. 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. Google Scholar
  2. Shaull Almagor, Dmitry Chistikov, Joël Ouaknine, and James Worrell. O-minimal invariants for discrete-time dynamical systems, 2020. Google Scholar
  3. Shaull Almagor, Edon Kelmendi, Joël Ouaknine, and James Worrell. Invariants for continuous linear dynamical systems, 2020. URL: http://arxiv.org/abs/2004.11661.
  4. Rajeev Alur. Principles of cyber-physical systems. MIT Press, 2015. Google Scholar
  5. 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. Google Scholar
  6. 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. Google Scholar
  7. Mireille Broucke. Reachability analysis for hybrid systems with linear dynamics. Mathematical Theory of Networks and Systems (MTNS’02), 2002. Google Scholar
  8. John W.S. Cassels. An Introduction to Diophantine Approximation. Cambridge University Press, 1965. Google Scholar
  9. 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. Google Scholar
  10. 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. Google Scholar
  11. 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. Google Scholar
  12. 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. Google Scholar
  13. 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. Google Scholar
  14. 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. Google Scholar
  15. 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. Google Scholar
  16. 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. Google Scholar
  17. Angus Macintyre. Turing meets schanuel. Annals of Pure and Applied Logic, 167(10):901-938, 2016. Google Scholar
  18. 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. Google Scholar
  19. David W Masser. Linear relations on algebraic groups. New Advances in Transcendence Theory, pages 248-262, 1988. Google Scholar
  20. 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. Google Scholar
  21. 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. Google Scholar
  22. 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. Google Scholar
  23. 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. Google Scholar
  24. Alfred Tarski. A decision method for elementary algebra and geometry. RAND Corporation, R-109, 1951. Google Scholar
  25. 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. Google Scholar
  26. Lou Van den Dries, Chris Miller, et al. Geometric categories and o-minimal structures. Duke Math. J, 84(2):497-540, 1996. Google Scholar
  27. 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. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact