Skip to main content
SpringerLink
Log in

Weak Markovian Bisimulation Congruences and Exact CTMC-Level Aggregations for Sequential Processes

  • Conference paper
Trustworthy Global Computing (TGC 2011)

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

Included in the following conference series:

Abstract

The Markovian behavioral equivalences defined so far treat exponentially timed internal actions like any other action. Since an exponentially timed internal action has a nonzero duration, it can be observed whenever it is executed between a pair of exponentially timed noninternal actions. However, no difference may be noted at steady state between a sequence of exponentially timed internal actions and a single exponentially timed internal action as long as their average durations coincide. We show that Milner’s construction to derive a weak bisimulation congruence for nondeterministic processes can be extended to sequential Markovian processes in a way that captures the above situation. The resulting weak Markovian bisimulation congruence admits a sound and complete axiomatization, induces an exact CTMC-level aggregation at steady state, and is decidable in polynomial time for finite-state processes having no cycles of exponentially timed internal actions.

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 54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.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. 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)

    Chapter  Google Scholar 

  3. Baier, C., Katoen, J.-P., Hermanns, H., Wolf, V.: Comparative Branching-Time Semantics for Markov Chains. Information and Computation 200, 149–214 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  4. Bernardo, M.: Non-Bisimulation-Based Markovian Behavioral Equivalences. Journal of Logic and Algebraic Programming 72, 3–49 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  5. Bernardo, M.: Weak Markovian Bisimulation Congruences and Exact CTMC-Level Aggregations for Concurrent Processes (in preparation)

    Google Scholar 

  6. Bernardo, M., Aldini, A.: Weak Markovian Bisimilarity: Abstracting from Prioritized/Weighted Internal Immediate Actions. In: Proc. of the 10th Italian Conf. on Theoretical Computer Science (ICTCS 2007), Rome, Italy, pp. 39–56. World Scientific (2007)

    Google Scholar 

  7. Bernardo, M., Bravetti, M.: Performance Measure Sensitive Congruences for Markovian Process Algebras. In: Theoretical Computer Science 290, 117–160 (2003)

    Google Scholar 

  8. Bravetti, M.: Revisiting Interactive Markov Chains. In: Proc. of the 3rd Int. Workshop on Models for Time-Critical Systems (MTCS 2002), Brno, Czech Republic. ENTCS, vol. 68(5), pp. 1–20. Elsevier (2002)

    Google Scholar 

  9. Bravetti, M., Bernardo, M., Gorrieri, R.: A Note on the Congruence Proof for Recursion in Markovian Bisimulation Equivalence. In: Proc. of the 6th Int. Workshop on Process Algebra and Performance Modelling (PAPM 1998), Nice, France, pp. 153–164 (1998)

    Google Scholar 

  10. Buchholz, P.: Exact and Ordinary Lumpability in Finite Markov Chains. Journal of Applied Probability 31, 59–75 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  11. van Glabbeek, R.J., Weijland, W.P.: Branching Time and Abstraction in Bisimulation Semantics. Journal of the ACM 43, 555–600 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  12. Hermanns, H. (ed.): Interactive Markov Chains. LNCS, vol. 2428. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  13. Hermanns, H., Rettelbach, M.: Syntax, Semantics, Equivalences, and Axioms for MTIPP. In: Proc. of the 2nd Int. Workshop on Process Algebra and Performance Modelling (PAPM 1994), Technical Report 27-4, Erlangen, Germany, pp. 71–87 (1994)

    Google Scholar 

  14. Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press (1996)

    Google Scholar 

  15. Howard, R.A.: Dynamic Probabilistic Systems. John Wiley & Sons (1971)

    Google Scholar 

  16. Kanellakis, P.C., Smolka, S.A.: CCS Expressions, Finite State Processes, and Three Problems of Equivalence. Information and Computation 86, 43–68 (1990)

    Article  MathSciNet  MATH  Google Scholar 

  17. Markovski, J., Trcka, N.: Lumping Markov Chains with Silent Steps. In: Proc. of the 3rd Int. Conf. on Quantitative Evaluation of Systems (QEST 2006), Riverside, CA, pp. 221–230. IEEE-CS Press (2006)

    Google Scholar 

  18. Milner, R.: Communication and Concurrency. Prentice Hall (1989)

    Google Scholar 

  19. Montanari, U., Sassone, V.: Dynamic Congruence vs. Progressing Bisimulation for CCS. Fundamenta Informaticae 16, 171–199 (1992)

    MathSciNet  MATH  Google Scholar 

  20. Paige, R., Tarjan, R.E.: Three Partition Refinement Algorithms. SIAM Journal on Computing 16, 973–989 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  21. Rettelbach, M.: Probabilistic Branching in Markovian Process Algebras. Computer Journal 38, 590–599 (1995)

    Article  Google Scholar 

  22. Rubino, G., Sericola, B.: Sojourn Times in Finite Markov Processes. Journal of Applied Probability 27, 744–756 (1989)

    Article  MathSciNet  Google Scholar 

  23. Stewart, W.J.: Introduction to the Numerical Solution of Markov Chains. Princeton University Press (1994)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Scienze di Base e Fondamenti, Università di Urbino, Italy

    Marco Bernardo

Authors
  1. Marco Bernardo
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computer Science Department, University of Pisa, Largo Bruno Pontecorvo 3, 56127, Pisa, Italy

    Roberto Bruni

  2. ECS, University of Southampton, University Road, SO17 1BJ, Southampton, UK

    Vladimiro Sassone

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bernardo, M. (2012). Weak Markovian Bisimulation Congruences and Exact CTMC-Level Aggregations for Sequential Processes. In: Bruni, R., Sassone, V. (eds) Trustworthy Global Computing. TGC 2011. Lecture Notes in Computer Science, vol 7173. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30065-3_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-30065-3_6

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-30064-6

  • Online ISBN: 978-3-642-30065-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation