Document Open Access Logo

Analysing Decisive Stochastic Processes

Authors Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, Pierre Carlier

PDF

File

Thumbnail PDF
PDF
LIPIcs.ICALP.2016.101.pdf
  • Filesize: 462 kB
  • 14 pages

Document Identifiers

Subject Classification

Keywords
  • Real-time stochastic processes
  • Decisiveness
  • Approximation Scheme

Metrics

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

Abstract

In 2007, Abdulla et al. introduced the elegant concept of decisive Markov chain. Intuitively, decisiveness allows one to lift the good properties of finite Markov chains to infinite Markov chains. For instance, the approximate quantitative reachability problem can be solved for decisive Markov chains (enjoying reasonable effectiveness assumptions) including probabilistic lossy channel systems and probabilistic vector addition systems with states. In this paper, we extend the concept of decisiveness to more general stochastic processes. This extension is non trivial as we consider stochastic processes with a potentially continuous set of states and uncountable branching (common features of real-time stochastic processes). This allows us to obtain decidability results for both qualitative and quantitative verification problems on some classes of real-time stochastic processes, including generalized semi-Markov processes and stochastic timed
automata

Cite As Get BibTex

Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, and Pierre Carlier. Analysing Decisive Stochastic Processes. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 101:1-101:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.ICALP.2016.101

Author Details

Nathalie Bertrand
Patricia Bouyer
Thomas Brihaye
Pierre Carlier

References

  1. Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Jonathan Cederberg. Timed lossy channel systems. In Proc. 31sth Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'12), volume 18 of LIPIcs, pages 374-386. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2012.374.
  2. Parosh Aziz Abdulla, Noomene Ben Henda, and Richard Mayr. Decisive Markov chains. Logical Methods in Computer Science, 3(4), 2007. Google Scholar
  3. Rajeev Alur and Mikhail Bernadsky. Bounded model checking for GSMP models of stochastic real-time systems. In Proc. 9th International Workshop on Hybrid Systems: Computation and Control (HSCC'06), volume 3927 of Lecture Notes in Computer Science, pages 19-33. Springer, 2006. Google Scholar
  4. Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994. Google Scholar
  5. Christel Baier. Reasoning about cost-utility constraints in probabilistic models. In Proc. 9th Workshop on Reachability Problems in Computational Models (RP'15), volume 9328 of Lecture Notes in Computer Science, pages 1-6. Springer, 2015. Google Scholar
  6. Christel Baier, Boudewijn Haverkort, Holger Hermanns, and Joost-Pieter Katoen. Model-checking algorithms for continuous-time Markov chains. IEEE Transactions on Software Engineering, 29(7):524-541, 2003. Google Scholar
  7. Mikhail Bernadsky and Rajeev Alur. Symbolic analysis for GSMP models with one stateful clock. In Proc. 10th International Workshop on Hybrid Systems: Computation and Control (HSCC'07), volume 4416 of Lecture Notes in Computer Science, pages 90-103. Springer, 2007. Google Scholar
  8. Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, and Nicolas Markey. Quantitative model-checking of one-clock timed automata under probabilistic semantics. In Proc. 5th International Conference on Quantitative Evaluation of Systems (QEST'08). IEEE Computer Society Press, 2008. Google Scholar
  9. Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, Quentin Menet, Christel Baier, Marcus Größer, and Marcin Jurdziński. Stochastic timed automata. Logical Methods in Computer Science, 10(4):1-73, 2014. Google Scholar
  10. Tomáš Brázdil, Jan Krčál, Jan Křetínský, and Vojtěch Řehák. Fixed-delay events in generalized semi-Markov processes revisited. In Proc. 22nd International Conference on Concurrency Theory (CONCUR'11), volume 6901 of Lecture Notes in Computer Science, pages 140-155. Springer, 2011. Google Scholar
  11. Lorenzo Clemente, Frédéric Herbreteau, Amélie Stainer, and Grégoire Sutre. Reachability of communicating timed processes. In Proc. 16th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'13), volume 7794 of Lecture Notes in Computer Science, pages 81-96. Springer, 2013. Google Scholar
  12. Josée Desharnais and Prakash Panangaden. Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes. Journal of Logic and Algebraic Programming, 56:99-115, 2003. Google Scholar
  13. Peter W. Glynn. A GSMP formalism for discrete event systems. Proceedings of the IEEE, 77(1):14-23, 1989. Google Scholar
  14. Geoffrey R. Grimmett and David R. Stirzaker. Probability and Random Processes. Oxford University Press, 1992. Google Scholar
  15. Ernst Moritz Hahn, Holger Hermanns, Björn Wachter, and Lijun Zhang. Time-bounded model checking of infinite-state continuous-time Markov chains. Fundamenta Informaticae, 95(1):129-155, 2009. Google Scholar
  16. Ronald A. Howard. Dynamic Probabilistic Systems, Volume II: Semi-Markov and Decision Processes. John Wiley &Sons, 1971. Google Scholar
  17. S. Purushothaman Iyer and Murali Narasimha. Probabilistic lossy channel systems. In Proc. 7th International Joint Conference on Theory and Practice of Software Development (TAPSOFT'97), volume 1214 of Lecture Notes in Computer Science, pages 667-681. Springer, 1997. Google Scholar
  18. Sadegh Soudjani, Rupak Majumdar, and Alessandro Abate. Safety verification of continuous-space pure jump Markov processes. In Proc. 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16), volume 9636 of Lecture Notes in Computer Science, pages 147-163. Springer, 2016. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact