Abstract
Markov automata describe systems in terms of events which may be nondeterministic, may occur probabilistically, or may be subject to time delays. We define a novel notion of weak bisimulation for such systems and prove that this provides both a sound and complete proof methodology for a natural extensional behavioural equivalence between such systems, a generalisation of reduction barbed congruence, the well-known touchstone equivalence for a large variety of process description languages.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
- Operational Semantic
- Label Transition System
- Full Distribution
- Behavioural Equivalence
- Probabilistic Automaton
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Aldini, A., Bernardo, M., Corradini, F.: A Process Algebraic Approach to Software Architecture Design. Springer, Heidelberg (2010)
Bernardo, M., Gorrieri, R.: A tutorial on empa: A theory of concurrent processes with nondeterminism, priorities, probabilities and time. Theor. Comput. Sci. 202(1-2), 1–54 (1998)
Bravetti, M., Bernardo, M.: Compositional asymmetric cooperations for process algebras with probabilities, priorities, and time. ENTCS 39(3) (2000)
Deng, Y., Du, W.: Probabilistic barbed congruence. ENTCS 190(3), 185–203 (2007)
Deng, Y., van Glabbeek, R., Hennessy, M., Morgan, C.: Testing finitary probabilistic processes (extended abstract). In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 274–288. Springer, Heidelberg (2009)
Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Weak bisimulation is sound and complete for pCTL\(^{\mbox{*}}\). Information and Computation 208(2), 203–219 (2010)
Eisentraut, C.: Personal communication (2011)
Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: Proc. LICS 2010, pp. 342–351 (2010)
Fournet, C., Gonthier, G.: A hierarchy of equivalences for asynchronous calculi. J. Log. Algebr. Program. 63(1), 131–173 (2005)
Hermanns, H.: Interactive Markov Chains: The Quest for Quantified Quality. LNCS, vol. 2428, p. 129. Springer, Heidelberg (2002)
Hermanns, H., Parma, A., Segala, R., Wachter, B., Zhang, L.: Probabilistic logical characterization. Inf. Comput. 209, 154–172 (2011)
Hillston, J.: A Compositional Approach to Performance Modelling. Distinguished Dissertations in Computer Science. Cambridge University Press, New York (2005)
Honda, K., Tokoro, M.: On asynchronous communication semantics. In: Zatarain-Cabada, R., Wang, J. (eds.) ECOOP-WS 1991. LNCS, vol. 612, pp. 21–51. Springer, Heidelberg (1992)
Jeffrey, A., Rathke, J.: Contextual equivalence for higher-order pi-calculus revisited. LMCS 1(1:4) (2005)
Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing (preliminary report). In: Proc. POPL 1989, pp. 344–352. ACM, New York (1989)
Milner, R.: Calculi for synchrony and asynchrony. Theor. Comput. Sci. 25, 267–310 (1983)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
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)
Rathke, J., Sobocinski, P.: Deriving structural labelled transitions for mobile ambients. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 462–476. Springer, Heidelberg (2008)
Sangiorgi, D., Kobayashi, N., Sumii, E.: Environmental bisimulations for higher-order languages. In: Proc. LICS 2007, pp. 293–302. IEEE Computer Society, Los Alamitos (2007)
Sangiorgi, D., Walker, D.: The π-calculus: a Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)
Segala, R.: Modeling and verification of randomized distributed real-time systems. Technical Report MIT/LCS/TR-676, PhD thesis, MIT, Dept. of EECS (1995)
Segala, R.: Testing probabilistic automata. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 299–314. Springer, Heidelberg (1996)
Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. Nord. J. Comput. 2(2), 250–273 (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Deng, Y., Hennessy, M. (2011). On the Semantics of Markov Automata. In: Aceto, L., Henzinger, M., Sgall, J. (eds) Automata, Languages and Programming. ICALP 2011. Lecture Notes in Computer Science, vol 6756. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22012-8_24
Download citation
DOI: https://doi.org/10.1007/978-3-642-22012-8_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22011-1
Online ISBN: 978-3-642-22012-8
eBook Packages: Computer ScienceComputer Science (R0)