Document Open Access Logo

On LTL Model Checking for Low-Dimensional Discrete Linear Dynamical Systems

Authors Toghrul Karimov, Joël Ouaknine, James Worrell

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2020.54.pdf
  • Filesize: 0.5 MB
  • 14 pages

Document Identifiers

Author Details

Toghrul Karimov
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany
Joël Ouaknine
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany
  • Department of Computer Science, University of Oxford, UK
James Worrell
  • Department of Computer Science, University of Oxford, UK

Funding

  • 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

Toghrul Karimov, Joël Ouaknine, and James Worrell. On LTL Model Checking for Low-Dimensional Discrete Linear Dynamical Systems. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 54:1-54:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.MFCS.2020.54

Abstract

Consider a discrete dynamical system given by a square matrix M ∈ ℚ^{d × d} and a starting point s ∈ ℚ^d. The orbit of such a system is the infinite trajectory ⟨ s, Ms, M²s, …⟩. Given a collection T₁, T₂, …, T_m ⊆ ℝ^d of semialgebraic sets, we can associate with each T_i an atomic proposition P_i which evaluates to true at time n if, and only if, M^ns ∈ T_i. This gives rise to the LTL Model-Checking Problem for discrete linear dynamical systems: given such a system (M,s) and an LTL formula over such atomic propositions, determine whether the orbit satisfies the formula. The main contribution of the present paper is to show that the LTL Model-Checking Problem for discrete linear dynamical systems is decidable in dimension 3 or less.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Linear dynamical systems
  • Orbit Problem
  • LTL model checking

Metrics

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

Related Versions

References

  1. Manindra Agrawal, S. Akshay, Blaise Genest, and P. S. Thiagarajan. Approximate verification of the symbolic dynamics of Markov chains. J. ACM, 62(1):2:1-2:34, 2015. Google Scholar
  2. S. Almagor, J. Ouaknine, and J. Worrell. The Polytope-Collision Problem. In 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, pages 24:1-24:14, 2017. Google Scholar
  3. Shaull Almagor, Joël Ouaknine, and James Worrell. The Semialgebraic Orbit Problem. In 36th International Symposium on Theoretical Aspects of Computer Science, STACS 2019, March 13-16, 2019, Berlin, Germany, pages 6:1-6:15, 2019. Google Scholar
  4. Shaull Almagor, Joël Ouaknine, and James Worrell. First-order orbit queries. Theory Comput Syst, 2020. Google Scholar
  5. S. Basu, R. Pollack, and M-F. Roy. Algorithms in real algebraic geometry, volume 20033. Springer, 2005. Google Scholar
  6. V. Chonev, J. Ouaknine, and J. Worrell. The Orbit Problem in higher dimensions. In Proceedings of the forty-fifth annual ACM symposium on Theory of computing, pages 941-950. ACM, 2013. Google Scholar
  7. V. Chonev, J. Ouaknine, and J. Worrell. The Polyhedron-Hitting Problem. In Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms, pages 940-956. SIAM, 2015. Google Scholar
  8. V. Chonev, J. Ouaknine, and J. Worrell. On the complexity of the Orbit Problem. J. ACM, 63(3):23:1-23:18, 2016. Google Scholar
  9. H. Cohen. A course in computational algebraic number theory, volume 138. Springer Science & Business Media, 2013. Google Scholar
  10. V. Halava, T. Harju, M. Hirvensalo, and J. Karhumäki. Skolem’s Problem - on the border between decidability and undecidability. Technical Report 683, Turku Centre for Computer Science, 2005. Google Scholar
  11. M. A Harrison. Lectures on linear sequential machines. Technical report, DTIC Document, 1969. Google Scholar
  12. R. Kannan and R. J. Lipton. The Orbit Problem is decidable. In Proceedings of the twelfth annual ACM symposium on Theory of computing, pages 252-261. ACM, 1980. Google Scholar
  13. R. Kannan and R. J. Lipton. Polynomial-time algorithm for the Orbit Problem. Journal of the ACM (JACM), 33(4):808-821, 1986. Google Scholar
  14. Zachary Kincaid, John Cyphert, Jason Breck, and Thomas W. Reps. Non-linear reasoning for invariant synthesis. Proc. ACM Program. Lang., 2(POPL):54:1-54:33, 2018. Google Scholar
  15. Martin Leucker and Christian Schallhart. A brief account of runtime verification. J. Log. Algebr. Program., 78(5):293-303, 2009. Google Scholar
  16. Nicolas Markey and Philippe Schnoebelen. Model checking a path. In CONCUR 2003 - Concurrency Theory, 14th International Conference, Proceedings, volume 2761 of Lecture Notes in Computer Science, pages 248-262. Springer, 2003. Google Scholar
  17. M. Mignotte. Some useful bounds. In Computer algebra, pages 259-263. Springer, 1983. Google Scholar
  18. M. Mignotte, T. Shorey, and R. Tijdeman. The distance between terms of an algebraic recurrence sequence. J. für die reine und angewandte Math., 349, 1984. Google Scholar
  19. J. Ouaknine and J. Worrell. Ultimate positivity is decidable for simple linear recurrence sequences. In International Colloquium on Automata, Languages, and Programming, pages 330-341. Springer, 2014. Google Scholar
  20. Alexander Rabinovich and Wolfgang Thomas. Decidable theories of the ordering of natural numbers with unary predicates. In Zoltán Ésik, editor, Computer Science Logic, pages 562-574, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. Google Scholar
  21. J. Renegar. A faster PSPACE algorithm for deciding the existential theory of the reals. In 29th Annual Symposium on Foundations of Computer Science, White Plains, New York, USA, 24-26 October 1988, pages 291-295, 1988. Google Scholar
  22. Alexei Semenov. Decidability of monadic theories, volume 176, pages 162-175. Springer Berlin Heidelberg, April 2006. Google Scholar
  23. T. Tao. Structure and randomness: pages from year one of a mathematical blog. American Mathematical Soc., 2008. Google Scholar
  24. N. K. Vereshchagin. Occurrence of zero in a linear recursive sequence. Mathematical notes of the Academy of Sciences of the USSR, 38(2):609-615, 1985. 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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact