Document Open Access Logo

Parameter Synthesis for Parametric Probabilistic Dynamical Systems and Prefix-Independent Specifications

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

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2022.10.pdf
  • Filesize: 1.17 MB
  • 16 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
  • University of Lorraine, CNRS, Inria, LORIA, Nancy, France
Joël Ouaknine
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany
David Purser
  • University of Warsaw, Poland
Markus A. Whiteland
  • University of Liège, Belgium
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).

Cite AsGet BibTex

Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser, Markus A. Whiteland, and James Worrell. Parameter Synthesis for Parametric Probabilistic Dynamical Systems and Prefix-Independent Specifications. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.CONCUR.2022.10

Abstract

We consider the model-checking problem for parametric probabilistic dynamical systems, formalised as Markov chains with parametric transition functions, analysed under the distribution-transformer semantics (in which a Markov chain induces a sequence of distributions over states). We examine the problem of synthesising the set of parameter valuations of a parametric Markov chain such that the orbits of induced state distributions satisfy a prefix-independent ω-regular property. Our main result establishes that in all non-degenerate instances, the feasible set of parameters is (up to a null set) semialgebraic, and can moreover be computed (in polynomial time assuming that the ambient dimension, corresponding to the number of states of the Markov chain, is fixed).

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Model checking
  • parametric Markov chains
  • distribution transformer semantics

Metrics

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

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. URL: https://doi.org/10.1145/2629417.
  2. 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.
  3. Shaull Almagor, Toghrul Karimov, Edon Kelmendi, Joël Ouaknine, and James Worrell. Deciding ω-regular properties on linear recurrence sequences. Proc. ACM Program. Lang., 5(POPL):1-24, 2021. URL: https://doi.org/10.1145/3434329.
  4. Tomáš Babiak, Mojmír Křetínský, Vojtěch Řehák, and Jan Strejček. LTL to Büchi Automata Translation: Fast and More Deterministic. In Cormac Flanagan and Barbara König, editors, Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, pages 95-109, Berlin, Heidelberg, 2012. Springer. URL: https://doi.org/10.1007/978-3-642-28756-5_8.
  5. 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 Serge Haddad and Daniele Varacca, editors, 32nd International Conference on Concurrency Theory, CONCUR 2021, volume 203 of LIPIcs, pages 28:1-28:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2021.28.
  6. Christel Baier, Christian Hensel, Lisa Hutschenreiter, Sebastian Junges, Joost-Pieter Katoen, and Joachim Klein. Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination. Information and Computation, 272:104504, June 2020. URL: https://doi.org/10.1016/j.ic.2019.104504.
  7. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  8. Saugata Basu, Richard Pollack, and Marie-Françoise Roy. Semi-algebraic sets. In Algorithms in Real Algebraic Geometry, pages 83-99. Springer Berlin Heidelberg, Berlin, Heidelberg, 2006. URL: https://doi.org/10.1007/3-540-33099-2_4.
  9. Richard Caron and Tim Traynor. The zero set of a polynomial. Technical report, WSMR report 05-02, 2005. Google Scholar
  10. 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.
  11. 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, pages 940-956. SIAM, 2014. Google Scholar
  12. Conrado Daws. Symbolic and Parametric Model Checking of Discrete-Time Markov Chains. In Zhiming Liu and Keijiro Araki, editors, Theoretical Aspects of Computing - ICTAC 2004, Lecture Notes in Computer Science, pages 280-294, Berlin, Heidelberg, 2005. Springer. URL: https://doi.org/10.1007/978-3-540-31862-0_21.
  13. Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Bruintjes, Joost-Pieter Katoen, and Erika Ábrahám. PROPhESY: A PRObabilistic ParamEter SYnthesis Tool. In Daniel Kroening and Corina S. Păsăreanu, editors, Computer Aided Verification, Lecture Notes in Computer Science, pages 214-231, Cham, 2015. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-21690-4_13.
  14. Ernst Moritz Hahn, Holger Hermanns, and Lijun Zhang. Probabilistic reachability for parametric Markov models. International Journal on Software Tools for Technology Transfer, 13(1):3-19, January 2011. URL: https://doi.org/10.1007/s10009-010-0146-x.
  15. Hans Hansson and Bengt Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6(5):512-535, September 1994. URL: https://doi.org/10.1007/BF01211866.
  16. 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.
  17. Vijay Anand Korthikanti, Mahesh Viswanathan, Gul Agha, and YoungMin Kwon. Reasoning about MDPs as Transformers of Probability Distributions. In 2010 Seventh International Conference on the Quantitative Evaluation of Systems, pages 199-208, September 2010. URL: https://doi.org/10.1109/QEST.2010.35.
  18. 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, Lecture Notes in Computer Science, pages 194-208, Berlin, Heidelberg, 2004. Springer. URL: https://doi.org/10.1007/978-3-540-30482-1_21.
  19. YoungMin Kwon and Gul Agha. Verifying the Evolution of Probability Distributions Governed by a DTMC. IEEE Transactions on Software Engineering, 37(1):126-141, January 2011. URL: https://doi.org/10.1109/TSE.2010.80.
  20. Ruggero Lanotte, Andrea Maggiolo-Schettini, and Angelo Troina. Parametric probabilistic transition systems for system design and analysis. Formal Aspects of Computing, 19(1):93-109, March 2007. URL: https://doi.org/10.1007/s00165-006-0015-2.
  21. Joël Ouaknine and James Worrell. Positivity problems for low-order linear recurrence sequences. In Chandra Chekuri, editor, Proceedings of the Twenty-Fifth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2014, pages 366-379. SIAM, 2014. URL: https://doi.org/10.1137/1.9781611973402.27.
  22. Joël Ouaknine and James Worrell. Ultimate positivity is decidable for simple linear recurrence sequences. In Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, and Elias Koutsoupias, editors, Automata, Languages, and Programming - 41st International Colloquium, ICALP 2014, volume 8573 of Lecture Notes in Computer Science, pages 330-341. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-43951-7_28.
  23. James Renegar. On the computational complexity and geometry of the first-order theory of the reals, part I: introduction. preliminaries. the geometry of semi-algebraic sets. the decision problem for the existential theory of the reals. J. Symb. Comput., 13(3):255-300, 1992. URL: https://doi.org/10.1016/S0747-7171(10)80003-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