Document Open Access Logo

Composition of Stochastic Transition Systems Based on Spans and Couplings

Authors Daniel Gburek, Christel Baier, Sascha Klüppelholz

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2016.102.pdf
  • Filesize: 0.51 MB
  • 15 pages

Document Identifiers

Author Details

Daniel Gburek
Christel Baier
Sascha Klüppelholz

Cite As Get BibTex

Daniel Gburek, Christel Baier, and Sascha Klüppelholz. Composition of Stochastic Transition Systems Based on Spans and Couplings. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 102:1-102:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.ICALP.2016.102

Abstract

Conventional approaches for parallel composition of stochastic systems relate probability measures of the individual components in terms of product measures. Such approaches rely on the assumption that components interact stochastically independent, which might be too rigid for modeling real world systems. In this paper, we introduce a parallel-composition operator for stochastic transition systems that is based on couplings of probability measures and does not impose any stochastic assumptions. When composing systems within our framework, the intended dependencies between components can be determined by providing so-called spans and span couplings. We present a congruence result for our operator with respect to a standard notion of bisimilarity and develop a general theory for spans, exploiting deep results from descriptive set theory. As an application of our general approach, we propose a model for stochastic hybrid systems called stochastic hybrid motion automata.

Subject Classification

Keywords
  • Stochastic Transition System
  • Composition
  • Stochastic Hybrid Motion Automata
  • Stochastically Independent
  • Coupling
  • Span
  • Bisimulation
  • Congruence
  • Po

Metrics

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

References

  1. L. de Alfaro. Formal Verification of Probabilistic Systems. PhD thesis, University of Stanford, 1997. Google Scholar
  2. L. de Alfaro. Stochastic transition systems. In 9th International Conference on Concurrency Theory (CONCUR), LNCS 1446, pages 423-438. Springer, 1998. Google Scholar
  3. R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138(1):3-34, 1995. Google Scholar
  4. R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183-235, 1994. Google Scholar
  5. R. Alur and T. A. Henzinger. Modularity for timed and hybrid systems. In 8th International Conference on Concurrency Theory (CONCUR), LNCS 1243, pages 74-88. Springer, 1997. Google Scholar
  6. G. Bacci, G. Bacci, K. G. Larsen, and R. Mardare. Bisimulation on Markov processes over arbitrary measurable spaces. In Horizons of the Mind. A Tribute to P. Panangaden, LNCS 8464, pages 76-95. Springer, 2014. Google Scholar
  7. P. Billingsley. Convergence of Probability Measures. Wiley-Interscience, 2 edition, 1999. Google Scholar
  8. V. I. Bogachev. Measure Theory Volume, volume 1 and 2. Springer, 2007. Google Scholar
  9. H. Bohnenkamp, P. R. D'Argenio, H. Hermanns, and J.-P. Katoen. MoDeST: A compositional modeling formalism for real-time and stochastic systems. IEEE Transactions on Software Engineering, 32(10):812-830, 2006. Google Scholar
  10. S. Bornot and J. Sifakis. On the composition of hybrid systems. In 1st International Workshop on Hybrid Systems: Computation and Control (HSCC), volume 1386 of Lecture Notes in Computer Science, pages 49-63. Springer, 1998. Google Scholar
  11. P. Bouyer, T. Brihaye, P. Carlier, and Q. Menet. Compositional design of stochastic timed automata. In 11th International Computer Science Symposium in Russia (CSR), LNCS, 2016 (to appear). Google Scholar
  12. M. Bravetti. Real time and stochastic time. In Formal Methods for the Design of Real-Time Systems, International School on Formal Methods for the Design of Computer, Communication and Software Systems (SFM-RT), LNCS 3185, pages 132-180. Springer, 2004. Google Scholar
  13. M. Bravetti and P. R. D'Argenio. Tutte le algebre insieme: Concepts, discussions and relations of stochastic process algebras with general distributions. In Validation of Stochastic Systems - A Guide to Current Research, LNCS 2925, pages 44-88. Springer, 2004. Google Scholar
  14. M. Bravetti and R. Gorrieri. The theory of interactive generalized semi-Markov processes. Theoretical Computer Science, 282(1):5-32, 2002. Google Scholar
  15. M. L. Bujorianu and John Lygeros. Towards a general theory of stochastic hybrid systems. In Stochastic Hybrid Systems, volume 337 of Lecture Notes in Control and Information Science, pages 3-30. Springer, 2006. Google Scholar
  16. S. Cattani, R. Segala, M. Z. Kwiatkowska, and G. Norman. Stochastic transition systems for continuous state spaces and non-determinism. In 8th International Conference on Foundations of Software Science and Computational Structures (FOSSACS), LNCS 3441, pages 125-139. Springer, 2005. Google Scholar
  17. V. Danos, J. Desharnais, F. Laviolette, and P. Panangaden. Bisimulation and cocongruence for probabilistic systems. Information and Computation, 204(4):503-523, 2006. Google Scholar
  18. P. R. D'Argenio. Algebras and Automata for Timed and Stochastic Systems. PhD thesis, University of Twente, 1999. Google Scholar
  19. P. R. D'Argenio and J.-P. Katoen. A theory of stochastic systems part I: Stochastic automata and part II: Process algebra. Information and Computation, 203(1):1-74, 2005. Google Scholar
  20. P. R. D'Argenio, P. Sánchez Terraf, and N. Wolovick. Bisimulations for non-deterministic labelled Markov processes. Mathematical Structures in Computer Science, 22:43-68, 2012. Google Scholar
  21. E. P. de Vink and J.J.M.M. Rutten. Bisimulation for probabilistic transition systems: a coalgebraic approach. Theoretical Computer Science, 221:271-293, 1999. Google Scholar
  22. J. Desharnais, A. Edalat, and P. Panangaden. Bisimulation for labelled Markov processes. Information and Computation, 179(2):163-193, 2002. Google Scholar
  23. C. Eisentraut, H. Hermanns, and L. Zhang. On probabilistic automata in continuous time. In 25th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 342-351. IEEE Computer Society, 2010. Google Scholar
  24. M. Fränzle, E. M. Hahn, H. Hermanns, N. Wolovick, and L. Zhang. Measurability and safety verification for stochastic hybrid systems. In 14th International Conference on Hybrid Systems: Computation and Control (HSCC), pages 43-52. ACM, 2011. Google Scholar
  25. D. Gburek, C. Baier, and S. Klüppelholz. Composition of stochastic transition systems based on spans and couplings. Technical report, Technische Universität Dresden, 2016. URL: http://wwwtcs.inf.tu-dresden.de/ALGI/PUB/ICALP16/.
  26. E. M. Hahn. Model checking stochastic hybrid systems. PhD thesis, Universität des Saarlandes, 2013. Google Scholar
  27. E. M. Hahn, A. Hartmanns, H. Hermanns, and J.-P. Katoen. A compositional modelling and analysis framework for stochastic hybrid systems. Formal Methods in System Design, 2012. Google Scholar
  28. A. Hartmanns and H. Hermanns. In the quantitative automata zoo. Science of Computer Programming, 112:3-23, 2015. Google Scholar
  29. T. A. Henzinger. The theory of hybrid automata. In 11th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 278-292. IEEE Computer Society, 1996. Google Scholar
  30. H. Hermanns. Interactive Markov Chains: And the Quest for Quantified Quality. Springer, 2002. Google Scholar
  31. H. Hermanns, J. Krcál, and J. Kretínský. Probabilistic bisimulation: Naturally on distributions. In 25th International Conference on Concurrency Theory (CONCUR), LNCS 8704, pages 249-265. Springer, 2014. Google Scholar
  32. C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1985. Google Scholar
  33. J. Hu, J. Lygeros, and S. Sastry. Towards a theory of stochastic hybrid systems. In 12th International Conference on Hybrid Systems: Computation and Control (HSCC), LNCS 1790, pages 160-173. Springer, 2000. Google Scholar
  34. A. S. Kechris. Classical Descriptive Set Theory, volume 156 of Graduate Texts in Mathematics. Springer, 1995. Google Scholar
  35. H. Kerstan and B. König. Coalgebraic trace semantics for probabilistic transition systems based on measure theory. In 23th International Conference on Concurrency Theory (CONCUR), LNCS 7454, pages 410-424. Springer, 2012. Google Scholar
  36. N. Lynch, R. Segala, and F. Vaandrager. Hybrid I/O automata. Information and Computation, 185(1):105-157, 2003. Google Scholar
  37. R. Milner. A Calculus of Communicating Systems. Springer, 1982. Google Scholar
  38. S. Mitra and N. Lynch. Trace-based semantics for probabilistic timed I/O automata. In 12th International Conference on Hybrid Systems: Computation and Control (HSCC), LNCS 4416, pages 718-722. Springer, 2007. Google Scholar
  39. R. Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Massachusetts Institute of Technology, 1995. Google Scholar
  40. J. Sproston. Model Checking for Probabilistic Timed and Hybrid Systems. PhD thesis, University of Birmingham, 2001. Google Scholar
  41. V. Strassen. The existence of probability measures with given marginals. The Annals of Mathematical Statistics, 36(2):423-439, 1965. 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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact