Skip to main content
SpringerLink
Log in

On the Semantics of Markov Automata

  • Conference paper
Automata, Languages and Programming (ICALP 2011)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6756))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aldini, A., Bernardo, M., Corradini, F.: A Process Algebraic Approach to Software Architecture Design. Springer, Heidelberg (2010)

    Book  MATH  Google Scholar 

  2. 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)

    Article  MATH  MathSciNet  Google Scholar 

  3. Bravetti, M., Bernardo, M.: Compositional asymmetric cooperations for process algebras with probabilities, priorities, and time. ENTCS 39(3) (2000)

    Google Scholar 

  4. Deng, Y., Du, W.: Probabilistic barbed congruence. ENTCS 190(3), 185–203 (2007)

    MATH  Google Scholar 

  5. 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)

    Chapter  Google Scholar 

  6. 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)

    Article  MATH  MathSciNet  Google Scholar 

  7. Eisentraut, C.: Personal communication (2011)

    Google Scholar 

  8. Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: Proc. LICS 2010, pp. 342–351 (2010)

    Google Scholar 

  9. Fournet, C., Gonthier, G.: A hierarchy of equivalences for asynchronous calculi. J. Log. Algebr. Program. 63(1), 131–173 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  10. Hermanns, H.: Interactive Markov Chains: The Quest for Quantified Quality. LNCS, vol. 2428, p. 129. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  11. Hermanns, H., Parma, A., Segala, R., Wachter, B., Zhang, L.: Probabilistic logical characterization. Inf. Comput. 209, 154–172 (2011)

    Article  MATH  MathSciNet  Google Scholar 

  12. Hillston, J.: A Compositional Approach to Performance Modelling. Distinguished Dissertations in Computer Science. Cambridge University Press, New York (2005)

    MATH  Google Scholar 

  13. 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)

    Chapter  Google Scholar 

  14. Jeffrey, A., Rathke, J.: Contextual equivalence for higher-order pi-calculus revisited. LMCS 1(1:4) (2005)

    Google Scholar 

  15. Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing (preliminary report). In: Proc. POPL 1989, pp. 344–352. ACM, New York (1989)

    Google Scholar 

  16. Milner, R.: Calculi for synchrony and asynchrony. Theor. Comput. Sci. 25, 267–310 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  17. Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)

    MATH  Google Scholar 

  18. 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)

    Chapter  Google Scholar 

  19. 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)

    Chapter  Google Scholar 

  20. 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)

    Google Scholar 

  21. Sangiorgi, D., Walker, D.: The π-calculus: a Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)

    MATH  Google Scholar 

  22. Segala, R.: Modeling and verification of randomized distributed real-time systems. Technical Report MIT/LCS/TR-676, PhD thesis, MIT, Dept. of EECS (1995)

    Google Scholar 

  23. Segala, R.: Testing probabilistic automata. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 299–314. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  24. Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. Nord. J. Comput. 2(2), 250–273 (1995)

    MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Shanghai Jiao Tong University, China

    Yuxin Deng

  2. Trinity College Dublin, Ireland

    Matthew Hennessy

  3. Carnegie Mellon University, USA

    Yuxin Deng

  4. Chinese Academy of Sciences, China

    Yuxin Deng

Authors
  1. Yuxin Deng
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Matthew Hennessy
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. ICE-TCS, School of Computer Science, Reykjavik University, Menntavegur 1, IS 101, Reykjavik, Iceland

    Luca Aceto

  2. Fakultät für Informatik, Universität Wien, Universitätsstraße10/9, 1090, Wien, Österreich, Austria

    Monika Henzinger

  3. Department of Applied Mathematics, Charles University, Malostranské nám. 25, 118 00, Praha 1, Czech Republic

    Jiří Sgall

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation