Document Open Access Logo

The Orbit Problem for Parametric Linear Dynamical Systems

Authors Christel Baier , Florian Funke , Simon Jantsch , Toghrul Karimov , Engel Lefaucheux , Florian Luca , Joël Ouaknine , David Purser , Markus A. Whiteland , James Worrell

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2021.28.pdf
  • Filesize: 0.77 MB
  • 17 pages

Document Identifiers

Author Details

Christel Baier
  • Technische Universität Dresden, Germany
Florian Funke
  • Technische Universität Dresden, Germany
Simon Jantsch
  • Technische Universität Dresden, Germany
Toghrul Karimov
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany
Engel Lefaucheux
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany
Florian Luca
  • School of Mathematics, Wits University, Johannesburg, South Africa
  • Research Group in Algebraic Structures & Applications, King Abdulaziz University, Thuwal, Saudi Arabia
  • 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
David Purser
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany
Markus A. Whiteland
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany
James Worrell
  • Department of Computer Science, University of Oxford, UK

Funding

This work was funded by DFG grant 389792660 as part of TRR 248 - CPEC (see https://perspicuous-computing.science), the Cluster of Excellence EXC 2050/1 (CeTI, project ID 390696704, as part of Germany’s Excellence Strategy), DFG-projects BA-1679/11-1 and BA-1679/12-1, and the Research Training Group QuantLA (GRK 1763).
  • Ouaknine, Joël: ERC grant AVS-ISS (648701). Also affiliated with Keble College, Oxford as http://emmy.network/ Fellow.
  • Worrell, James: Supported by EPSRC Fellowship EP/N008197/1.

Cite AsGet BibTex

Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Florian Luca, Joël Ouaknine, David Purser, Markus A. Whiteland, and James Worrell. The Orbit Problem for Parametric Linear Dynamical Systems. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 28:1-28:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CONCUR.2021.28

Abstract

We study a parametric version of the Kannan-Lipton Orbit Problem for linear dynamical systems. We show decidability in the case of one parameter and Skolem-hardness with two or more parameters. More precisely, consider a d-dimensional square matrix M whose entries are algebraic functions in one or more real variables. Given initial and target vectors u,v ∈ ℚ^d, the parametric point-to-point orbit problem asks whether there exist values of the parameters giving rise to a concrete matrix N ∈ ℝ^{d× d}, and a positive integer n ∈ ℕ, such that N^{n} u = v. We show decidability for the case in which M depends only upon a single parameter, and we exhibit a reduction from the well-known Skolem Problem for linear recurrence sequences, suggesting intractability in the case of two or more parameters.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Orbit problem
  • parametric
  • linear dynamical systems

Metrics

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

Related Versions

References

  1. S. Akshay, Timos Antonopoulos, Joël Ouaknine, and James Worrell. Reachability problems for Markov chains. Inf. Process. Lett., 115(2):155–158, 2015. URL: https://doi.org/10.1016/j.ipl.2014.08.013.
  2. Shaull Almagor, Joël Ouaknine, and James Worrell. The Polytope-Collision Problem. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017), volume 80 of LIPIcs, pages 24:1-24:14, Dagstuhl, Germany, 2017. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.24.
  3. Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, Amaury Pouly, David Purser, and Markus A. Whiteland. Reachability in Dynamical Systems with Rounding. In Nitin Saxena and Sunil Simon, editors, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020), volume 182 of LIPIcs, pages 36:1-36:17, Dagstuhl, Germany, 2020. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2020.36.
  4. Ezio Bartocci, Radu Grosu, Panagiotis Katsaros, C. R. Ramakrishnan, and Scott A. Smolka. Model repair for probabilistic systems. In Parosh Aziz Abdulla and K. Rustan M. Leino, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 326-340, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. Google Scholar
  5. Saugata Basu, Richard Pollack, and Marie-Françoise Roy. Algorithms in Real Algebraic Geometry (Algorithms and Computation in Mathematics). Springer-Verlag, Berlin, Heidelberg, 2006. Google Scholar
  6. Attila Bérczes, Kálmán Gyory, Jan-Hendrik Evertse, and Corentin Pontreau. Effective results for points on certain subvarieties of tori. Mathematical Proceedings of the Cambridge Philosophical Society, 147(1):69, 2009. Google Scholar
  7. Jean Berstel and Maurice Mignotte. Deux propriétés décidables des suites récurrentes linéaires. Bulletin de la Société Mathématique de France, 104:175-184, 1976. URL: https://doi.org/10.24033/bsmf.1823.
  8. Enrico Bombieri, David Masser, and Umberto Zannier. Intersecting a curve with algebraic subgroups of multiplicative groups. International Mathematics Research Notices, 1999(20):1119-1140, January 1999. URL: https://doi.org/10.1155/S1073792899000628.
  9. Enrico Bombieri, David Masser, and Umberto Zannier. Intersecting curves and algebraic subgroups: conjectures and more results. Transactions of the American Mathematical Society, 358(5):2247-2257, 2006. URL: https://doi.org/10.1090/S0002-9947-05-03810-9.
  10. Jin-Yi Cai, Richard J Lipton, and Yechezkel Zalcstein. The complexity of the ABC problem. SIAM Journal on Computing, 29(6):1878-1888, 2000. Google Scholar
  11. John W. S. Cassels. Local Fields. London Mathematical Society Student Texts. Cambridge University Press, 1986. URL: https://doi.org/10.1017/CBO9781139171885.
  12. Milan Češka, Frits Dannenberg, Marta Kwiatkowska, and Nicola Paoletti. Precise parameter synthesis for stochastic biochemical systems. In Pedro Mendes, Joseph O. Dada, and Kieran Smallbone, editors, Computational Methods in Systems Biology, pages 86-98, Cham, 2014. Springer International Publishing. Google Scholar
  13. Rohit Chadha, Vijay Anand Korthikanti, Mahesh Viswanathan, Gul Agha, and YoungMin Kwon. Model checking MDPs with a unique compact invariant set of distributions. In Eighth International Conference on Quantitative Evaluation of Systems, QEST 2011, Aachen, Germany, 5-8 September, 2011, pages 121-130. IEEE Computer Society, 2011. URL: https://doi.org/10.1109/QEST.2011.22.
  14. Ventsislav Chonev, Joël Ouaknine, and James Worrell. The orbit problem in higher dimensions. In Proceedings of the Forty-Fifth Annual ACM Symposium on Theory of Computing, STOC '13, page 941–950, New York, NY, USA, 2013. URL: https://doi.org/10.1145/2488608.2488728.
  15. Ventsislav Chonev, Joël Ouaknine, and James Worrell. The polyhedron-hitting problem. In Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA '15, page 940–956, USA, 2015. Society for Industrial and Applied Mathematics. Google Scholar
  16. Ventsislav Chonev, Joël Ouaknine, and James Worrell. On the Skolem Problem for Continuous Linear Dynamical Systems. In Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi, editors, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016), volume 55 of LIPIcs, pages 100:1-100:13, Dagstuhl, Germany, 2016. URL: https://doi.org/10.4230/LIPIcs.ICALP.2016.100.
  17. Henri Cohen. A Course in Computational Algebraic Number Theory. Springer Publishing Company, Incorporated, 2010. Google Scholar
  18. David A. Cox, John Little, and Donal O'Shea. Ideals, varieties, and algorithms - an introduction to computational algebraic geometry and commutative algebra. Undergraduate texts in mathematics. Springer, 2 edition, 1997. Google Scholar
  19. Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, and Ufuk Topcu. Synthesis in pMDPs: A tale of 1001 parameters. In Shuvendu K. Lahiri and Chao Wang, editors, Automated Technology for Verification and Analysis, pages 160-176, Cham, 2018. Springer International Publishing. Google Scholar
  20. Harm Derksen, Emmanuel Jeandel, and Pascal Koiran. Quantum automata and algebraic groups. Journal of Symbolic Computation, 39(3):357-371, 2005. Special issue on the occasion of MEGA 2003. URL: https://doi.org/10.1016/j.jsc.2004.11.008.
  21. Otto Foster. Compact Riemann Surfaces, volume 81 of Graduate Textbooks in Mathematics. Springer, 1981. URL: https://doi.org/10.1007/978-1-4612-5961-9.
  22. Robert Givan, Sonia Leach, and Thomas Dean. Bounded-parameter Markov decision processes. Artificial Intelligence, 122(1):71-109, 2000. URL: https://doi.org/10.1016/S0004-3702(00)00047-3.
  23. Michael A. Harrison. Lectures on Linear Sequential Machines. Academic Press, Inc., USA, 1969. Google Scholar
  24. Bengt Jonsson and Kim Guldstrand Larsen. Specification and refinement of probabilistic processes. In Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS '91), Amsterdam, The Netherlands, July 15-18, 1991, pages 266-277. IEEE Computer Society, 1991. URL: https://doi.org/10.1109/LICS.1991.151651.
  25. Sebastian Junges, Erika Abraham, Christian Hensel, Nils Jansen, Joost-Pieter Katoen, Tim Quatmann, and Matthias Volk. Parameter synthesis for Markov models, 2019. Google Scholar
  26. Ravindran Kannan and Richard J. Lipton. Polynomial-time algorithm for the orbit problem. J. ACM, 33(4):808-821, 1986. URL: https://doi.org/10.1145/6490.6496.
  27. Vijay Anand Korthikanti, Mahesh Viswanathan, Gul Agha, and YoungMin Kwon. Reasoning about MDPs as transformers of probability distributions. In QEST 2010, Seventh International Conference on the Quantitative Evaluation of Systems, Williamsburg, Virginia, USA, 15-18 September 2010, pages 199-208. IEEE Computer Society, 2010. URL: https://doi.org/10.1109/QEST.2010.35.
  28. Igor Kozine and Lev Utkin. Interval-valued finite Markov chains. Reliable Computing, 8:97-113, April 2002. URL: https://doi.org/10.1023/A:1014745904458.
  29. YoungMin Kwon and Gul Agha. Linear inequality LTL (iLTL): A model checker for discrete time Markov chains. In Jim Davies, Wolfram Schulte, and Mike Barnett, editors, Formal Methods and Software Engineering, pages 194-208, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. Google Scholar
  30. Ruggero Lanotte, Andrea Maggiolo-Schettini, and Angelo Troina. Parametric probabilistic transition systems for system design and analysis. Formal Asp. Comput., 19:93-109, March 2007. URL: https://doi.org/10.1007/s00165-006-0015-2.
  31. Pierre Liardet. Sur une conjecture de Serge Lang. In Journées arithmétiques de Bordeaux, number 24-25 in Astérisque. Société mathématique de France, 1975. URL: https://www.numdam.org/item/AST_1975__24-25__187_0/.
  32. Rupak Majumdar, Mahmoud Salamati, and Sadegh Soudjani. On Decidability of Time-Bounded Reachability in CTMDPs. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020), volume 168 of LIPIcs, pages 133:1-133:19, Dagstuhl, Germany, 2020. URL: https://doi.org/10.4230/LIPIcs.ICALP.2020.133.
  33. Maurice Mignotte. Some Useful Bounds, pages 259-263. Springer Vienna, Vienna, 1982. URL: https://doi.org/10.1007/978-3-7091-3406-1_16.
  34. Maurice Mignotte, Tarlok N. Shorey, and Robert Tijdeman. The distance between terms of an algebraic recurrence sequence. Journal für die reine und angewandte Mathematik, 1984(349):63-76, 01 May. 1984. URL: https://doi.org/10.1515/crll.1984.349.63.
  35. Alina Ostafe and Igor Shparlinski. On the Skolem problem and some related questions for parametric families of linear recurrence sequences, 2020. Google Scholar
  36. Joël Ouaknine and James Worrell. Decision problems for linear recurrence sequences. In Alain Finkel, Jérôme Leroux, and Igor Potapov, editors, Reachability Problems, pages 21-28, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-33512-9_3.
  37. Shashank Pathak, Erika Ábrahám, Nils Jansen, Armando Tacchella, and Joost-Pieter Katoen. A greedy approach for the efficient repair of stochastic models. In Klaus Havelund, Gerard Holzmann, and Rajeev Joshi, editors, NASA Formal Methods, pages 295-309, Cham, 2015. Springer International Publishing. Google Scholar
  38. Jakob Piribauer and Christel Baier. On Skolem-Hardness and Saturation Points in Markov Decision Processes. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020), volume 168 of LIPIcs, pages 138:1-138:17, Dagstuhl, Germany, 2020. URL: https://doi.org/10.4230/LIPIcs.ICALP.2020.138.
  39. Nikolay K. Vereshchagin. Occurrence of zero in a linear recursive sequence. Mathematical notes of the Academy of Sciences of the USSR, 38:609-615, 1985. Google Scholar
  40. Michel Waldschmidt. Heights of Algebraic Numbers. Springer Berlin Heidelberg, Berlin, Heidelberg, 2000. URL: https://doi.org/10.1007/978-3-662-11569-5_3.
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