Document Open Access Logo

About Decisiveness of Dynamic Probabilistic Models

Authors Alain Finkel , Serge Haddad , Lina Ye

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2023.14.pdf
  • Filesize: 0.84 MB
  • 17 pages

Document Identifiers

Author Details

Alain Finkel
  • Université Paris-Saclay, CNRS, ENS Paris-Saclay, IUF, Laboratoire Méthodes Formelles, 91190, Gif-sur-Yvette, France
Serge Haddad
  • Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, INRIA 91190, Gif-sur-Yvette, France
Lina Ye
  • Université Paris-Saclay, CNRS, ENS Paris-Saclay, CentraleSupélec, Laboratoire Méthodes Formelles, 91190, Gif-sur-Yvette, France

Funding

  • Finkel, Alain: His work has been supported by ANR project BRAVAS (ANR-17-CE40-0028).
  • Haddad, Serge: His work has been supported by ANR project MAVeriQ (ANR-20-CE25-0012).

Cite AsGet BibTex

Alain Finkel, Serge Haddad, and Lina Ye. About Decisiveness of Dynamic Probabilistic Models. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CONCUR.2023.14

Abstract

Decisiveness of infinite Markov chains with respect to some (finite or infinite) target set of states is a key property that allows to compute the reachability probability of this set up to an arbitrary precision. Most of the existing works assume constant weights for defining the probability of a transition in the considered models. However numerous probabilistic modelings require the (dynamic) weight to also depend on the current state. So we introduce a dynamic probabilistic version of counter machine (pCM). After establishing that decisiveness is undecidable for pCMs even with constant weights, we study the decidability of decisiveness for subclasses of pCM. We show that, without restrictions on dynamic weights, decisiveness is undecidable with a single state and single counter pCM. On the contrary with polynomial weights, decisiveness becomes decidable for single counter pCMs under mild conditions. Then we show that decisiveness of probabilistic Petri nets (pPNs) with polynomial weights is undecidable even when the target set is upward-closed unlike the case of constant weights. Finally we prove that the standard subclass of pPNs with a regular language is decisive with respect to a finite set whatever the kind of weights.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Markov processes
  • Theory of computation → Concurrency
Keywords
  • infinite Markov chain
  • reachability probability
  • decisiveness

Metrics

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

Related Versions

References

  1. Parosh Aziz Abdulla, Christel Baier, S. Purushothaman Iyer, and Bengt Jonsson. Reasoning about probabilistic lossy channel systems. In Catuscia Palamidessi, editor, CONCUR 2000 - 11th International Conference on Concurrency Theory, University Park, PA, USA, August 22-25, volume 1877 of LNCS, pages 320-333. Springer, 2000. URL: https://doi.org/10.1007/3-540-44618-4_24.
  2. Parosh Aziz Abdulla, Nathalie Bertrand, Alexander Moshe Rabinovich, and Philippe Schnoebelen. Verification of probabilistic systems with faulty communication. Inf. Comput., 202(2):141-165, 2005. URL: https://doi.org/10.1016/j.ic.2005.05.008.
  3. Parosh Aziz Abdulla, Noomene Ben Henda, and Richard Mayr. Decisive Markov chains. Log. Methods Comput. Sci., 3(4), 2007. URL: https://doi.org/10.48550/arXiv.0706.2585.
  4. Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. Inf. Comput., 127(2):91-101, 1996. URL: https://doi.org/10.1109/LICS.1993.287591.
  5. Parosh Aziz Abdulla and Alexander Moshe Rabinovich. Verification of probabilistic systems with faulty communication. In Proceedings of the 6th international conference on Foundations of Software Science and Computational Structures FOSSACS, volume 2620 of LNCS, pages 39-53. Springer, 2003. URL: https://doi.org/10.1007/3-540-36576-1_3.
  6. Christel Baier and Bettina Engelen. Establishing qualitative properties for probabilistic lossy channel systems: An algorithmic approach. In Formal Methods for Real-Time and Probabilistic Systems, Proceedings of the 5th International AMAST Workshop, ARTS'99, Bamberg, Germany, May 26-28, 1999, volume 1601 of LNCS, pages 34-52. Springer, 1999. URL: https://doi.org/10.1007/3-540-48778-6_3.
  7. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  8. N. G. Bean, L. Bright, G. Latouche, C. E. M. Pearce, P. K. Pollett, and P. G. Taylor. The quasi-stationary behavior of quasi-birth-and-death processes. The Annals of Applied Probability, 7(1):134-155, 1997. URL: https://doi.org/10.1214/aoap/1034625256.
  9. Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, and Pierre Carlier. When are stochastic transition systems tameable? J. Log. Algebraic Methods Program., 99:41-96, 2018. URL: https://doi.org/10.48550/arXiv.1703.04806.
  10. Nathalie Bertrand and Philippe Schnoebelen. Model checking lossy channels systems is probably decidable. In Proceedings of the 6th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2003 Held as Part of ETAPS 2003, Warsaw, Poland, April 7-11, volume 2620 of LNCS, pages 120-135. Springer, 2003. URL: https://doi.org/10.1007/3-540-36576-1_8.
  11. Tomás Brázdil, Krishnendu Chatterjee, Antonín Kucera, Petr Novotný, Dominik Velan, and Florian Zuleger. Efficient algorithms for asymptotic bounds on termination time in VASS. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, pages 185-194. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209191.
  12. Tomás Brázdil, Javier Esparza, Stefan Kiefer, and Antonín Kucera. Analyzing probabilistic pushdown automata. Formal Methods Syst. Des., 43(2):124-163, 2013. URL: https://doi.org/10.1007/s10703-012-0166-0.
  13. Tomás Brázdil, Stefan Kiefer, and Antonín Kucera. Efficient analysis of probabilistic programs with an unbounded counter. J. ACM, 61(6):41:1-41:35, 2014. URL: https://doi.org/10.1145/2629599.
  14. Stéphane Demri. On selective unboundedness of VASS. J. Comput. Syst. Sci., 79(5):689-713, 2013. URL: https://doi.org/10.1016/j.jcss.2013.01.014.
  15. Catherine Dufourd, Alain Finkel, and Philippe Schnoebelen. Reset nets between decidability and undecidability. In Proceedings of the 25th International Colloquium on Automata, Languages and Programming, ICALP'98, volume 1443 of LNCS, pages 103-115. Springer, 1998. URL: https://doi.org/10.5555/646252.686157.
  16. Javier Esparza, Antonín Kucera, and Richard Mayr. Model Checking Probabilistic Pushdown Automata. Logical Methods in Computer Science, Volume 2, Issue 1, 2006. URL: https://doi.org/10.2168/LMCS-2(1:2)2006.
  17. Alain Finkel, Serge Haddad, and Lina Ye. About decisiveness of dynamic probabilistic models. CoRR, abs/2305.19564, 2023. URL: https://doi.org/10.48550/arXiv.2305.19564.
  18. Abraham Ginzburg and Michael Yoeli. Vector addition systems and regular languages. J. Comput. Syst. Sci., 20(3):277-284, 1980. URL: https://doi.org/10.1016/0022-0000(80)90009-4.
  19. S. Purushothaman Iyer and Murali Narasimha. Probabilistic lossy channel systems. In Theory and Practice of Software Development (TAPSOFT), 7th International Joint Conference CAAP/FASE, volume 1214 of LNCS, pages 667-681. Springer, 1997. URL: https://doi.org/10.1007/BFb0030633.
  20. J. Kemeny, J. Snell, and A. Knapp. Denumerable Markov Chains. Springer-Verlag, 2nd edition, 1976. URL: https://doi.org/10.1007/978-1-4684-9455-6.
  21. Tianrong Lin. Model-checking PCTL properties of stateless probabilistic pushdown systems with various extensions, 2023. URL: https://doi.org/10.48550/arXiv.2209.10517.
  22. Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, Inc., USA, 1967. URL: https://doi.org/10.5555/1095587.
  23. Alexander Moshe Rabinovich. Quantitative analysis of probabilistic lossy channel systems. In Proceedings of 30th International Colloquium Automata, Languages and Programming ICALP, volume 2719 of LNCS, pages 1008-1021. Springer, 2003. URL: https://doi.org/10.1007/3-540-45061-0_78.
  24. Eugene S. Santos. Probabilistic grammars and automata. Inf. Control., 21(1):27-47, 1972. URL: https://doi.org/10.1016/S0019-9958(72)90026-5.
  25. Rüdiger Valk. Self-modifying nets, a natural extension of Petri nets. In Proceedings of the 5th International Colloquium on Automata, Languages and Programming, volume 62 of LNCS, pages 464-476. Springer, 1978. URL: https://doi.org/10.1007/3-540-08860-1_35.
  26. Rüdiger Valk and Guy Vidal-Naquet. Petri nets and regular languages. J. Comput. Syst. Sci., 23(3):299-325, 1981. URL: https://doi.org/10.1016/0022-0000(81)90067-2.
  27. Moshe Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In Proceedings of the 26th Annual Symposium on Foundations of Computer Science, pages 327-338. IEEE Computer Society, 1985. URL: https://doi.org/10.1109/SFCS.1985.12.
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