Abstract
We study the interaction between non-deterministic and probabilistic behaviour in systems with continuous state spaces, arbitrary probability distributions and uncountable branching. Models of such systems have been proposed previously. Here, we introduce a model that extends probabilistic automata to the continuous setting. We identify the class of schedulers that ensures measurability properties on executions, and show that such measurability properties are preserved by parallel composition. Finally, we demonstrate how these results allow us to define an alternative notion of weak bisimulation in our model.
Supported in part by EPSRC grants GR/N22960, GR/S46727 and GR/S11107, MURST project CoVer and FIRB project SPY-Mod.
Chapter PDF
Similar content being viewed by others
References
Alfaro, L.d.: Formal Verification of Probabilistic Systems. PhD thesis, Stanford University, Available as Technical report STAN-CS-TR-98-1601 (1997)
Ash, R.B.: Real Analysis and Probability. Academic Press, London (1972)
Baier, C., Hermanns, H.: Weak bisimulation for fully probabilistic processes. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 119–130. Springer, Heidelberg (1997)
Bravetti, M.: Specification and Analysis of Stochastic Real-Time Systems. PhD thesis, Università di Bologna, Padova, Venezia (2002)
Bravetti, M., D’Argenio, P.: Tutte le algebre insieme: Concepts, discussions and relations of stochastic process algebras with general distributions. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 44–88. Springer, Heidelberg (2004)
Cattani, S.: Trace-based Process Algebras for Real-time Probabilistic Systems. PhD thesis, School of Computer Science, The University of Birmingham (forthcoming 2005)
D’Argenio, P.R.: Algebras and Automata for Timed and Stochastic Systems. PhD thesis, Department of Computer Science, University of Twente (November 1999)
Desharnais, J., Edalat, A., Panangaden, P.: Bisimulation for labelled markov processes. Information and Computation 179(2), 163–193 (2002)
Giry, M.: A categorical approach to probability theory. In: Banaschewski, B. (ed.) Categorical Aspects of Topology and Analysis. Lecture Notes in Mathematics, vol. 915, pp. 68–85. Springer, Heidelberg (1981)
Glabbeek, R.v., Smolka, S., Steffen, B.: Reactive, generative, and stratified models of probabilistic processes. Information and Computation 121(1), 59–80 (1995)
Hansson, H.: Time and Probability in Formal Design of Distributed Systems. Real-Time Safety Critical Systems, vol. 1. Elsevier, Amsterdam (1994)
Hermanns, H.: Interactive Markov Chains: The Quest for Quantified Quality. LNCS, vol. 2428, p. 57. Springer, Heidelberg (2002)
Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press, Cambridge (1996)
Hoare, C.: Communicating Sequential Processes. Prentice-Hall International, Englewood Cliffs (1985)
Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Verifying quantitative properties of continuous probabilistic real-time graphs. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 132–137. Springer, Heidelberg (2000)
Larsen, K., Skou, A.: Bisimulation through probabilistic testing. Information and Computation 94(1), 1–28 (1991)
Milner, R.: Communication and Concurrency. Prentice-Hall International, Englewood Cliffs (1989)
Panangaden, P.: Measure and probability for concurrency theorists. Theoretical Comput. Sci. 253(2), 287–309 (2001)
Philippou, A., Lee, I., Sokolsky, O.: Weak bisimulation for probabilistic systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 334–349. Springer, Heidelberg (2000)
Segala, R.: A compositional trace-based semantics for probabilistic automata. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 234–248. Springer, Heidelberg (1995)
Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, MIT, Dept. of Electrical Engineering and Computer Science (1995); Also appears as technical report MIT/LCS/TR-676
Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. Nordic Journal of Computing 2(2), 250–273 (1995)
Stoelinga, M.: Alea jacta est: verification of probabilistic, real-time and parametric systems. PhD thesis, University of Nijmegen, The Netherlands (April 2002)
Wu, S., Smolka, S., Stark, E.: Composition and behaviors of probabilistic I/O automata. Theoretical Comput. Sci. 176(1-2), 1–38 (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cattani, S., Segala, R., Kwiatkowska, M., Norman, G. (2005). Stochastic Transition Systems for Continuous State Spaces and Non-determinism. In: Sassone, V. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2005. Lecture Notes in Computer Science, vol 3441. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31982-5_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-31982-5_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25388-4
Online ISBN: 978-3-540-31982-5
eBook Packages: Computer ScienceComputer Science (R0)