Skip to main content
SpringerLink
Log in

Lumping-Based Equivalences in Markovian Automata and Applications to Product-Form Analyses

  • Conference paper
  • First Online:
Quantitative Evaluation of Systems (QEST 2015)

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

Included in the following conference series:

Abstract

The analysis of models specified with formalisms like Markovian process algebras or stochastic automata can be based on equivalence relations among the states. In this paper we introduce a relation called exact equivalence that, differently from most aggegation approaches, induces an exact lumping on the underlying Markov chain instead of a strong lumping. We prove that this relation is a congruence for Markovian process algebras and stochastic automata whose synchronisation semantics can be seen as the master/slave synchronisation of the Stochastic Automata Networks (SAN). We show the usefulness of this relation by proving that the class of quasi-reversible models is closed under exact equivalence. Quasi-reversibility is a pivotal property to study product-form models, i.e., models whose equilibrium behaviour can be computed very efficiently without the problem of the state space explosion. Hence, exact equivalence turns out to be a theoretical tool to prove the product-form of models by showing that they are exactly equivalent to models which are known to be quasi-reversible.

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

Notes

  1. 1.

    Notice that \(\tau \) self-loops do not affect the equilibrium distribution of the CTMC underlying the automaton. Moreover, the choice of excluding \(\tau \) self-loops will simplify the definition of automata synchronisation.

References

  1. Baarir, S., Beccuti, M., Dutheillet, C., Franceschinis, G., Haddad, S.: Lumping partially symmetrical stochastic models. Perf. Eval. 68(1), 21–44 (2011)

    Article  Google Scholar 

  2. Baier, C., Katoen, J.-P., Hermanns, H.: Comparative branching-time semantics for markov chains. Inf. Comput. 200(2), 149–214 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  3. Balsamo, S., Marin, A.: Queueing networks. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 34–82. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  4. Balsamo, S., Dei Rossi, G.-L., Marin, A.: Lumping and reversed processes in cooperating automata. In: Al-Begain, K., Fiems, D., Vincent, J.-M. (eds.) ASMTA 2012. LNCS, vol. 7314, pp. 212–226. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  5. Baskett, F., Chandy, K.M., Muntz, R.R., Palacios, F.G.: Open, closed, and mixed networks of queues with different classes of customers. J. ACM 22(2), 248–260 (1975)

    Article  MathSciNet  MATH  Google Scholar 

  6. Bernardo, M.: Weak Markovian bisimulation congruences and exact CTMC-level aggregations for concurrent processes. In: Proceedings of the 10th Workshop on Quantitative Aspects of Programming Languages and Systems (QALP12), pp. 122–136 (2012)

    Google Scholar 

  7. Bernardo, M., Gorrieri, R.: A tutorial on empa: a theory of concurrent processes with nondeterminism, priorities, probabilities and time. Theo. Comput. Sci. 202, 1–54 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  8. Bravetti, M.: Revisiting interactive markov chains. Electr. Notes Theor. Comput. Sci. 68(5), 65–84 (2003)

    Article  Google Scholar 

  9. Buchholz, P.: Exact and ordinary lumpability in finite markov chains. J. Appl. Probab. 31, 59–75 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  10. Buchholz, P.: Exact performance equivalence: an equivalence relation for stochastic automata. Theor. Comput. Sci. 215(1–2), 263–287 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  11. Harrison, P.G.: Turning back time in markovian process algebra. Theo. Comput. Sci. 290(3), 1947–1986 (2003)

    Article  MATH  Google Scholar 

  12. Hermanns, H.: Interactive Markov Chains. Springer, Heidelberg (2002)

    Book  MATH  Google Scholar 

  13. Hermanns, H., Herzog, U., Katoen, J.P.: Process algebra for performance evaluation. Theor. Comput. Sci. 274(1–2), 43–87 (2002)

    Article  MathSciNet  MATH  Google Scholar 

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

    Book  Google Scholar 

  15. Hillston, J., Marin, A., Piazza, C., Rossi, S.: Contextual lumpability. In: Proceedings of Valuetools 2013 Conference. ACM Press (2013)

    Google Scholar 

  16. Skou, A., Larsen, K.G.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1–28 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  17. Kelly, F.: Reversibility and Stochastic Networks. Wiley, New York (1979)

    MATH  Google Scholar 

  18. Kemeny, J.G., Snell, J.L.: Finite Markov Chains. Springer, Heidelberg (1976)

    MATH  Google Scholar 

  19. Le Boudec, J.Y.: A BCMP extension to multiserver stations with concurrent classes of customers. In: SIGMETRICS 1986/PERFORMANCE 1986: Proceedings of the 1986 ACM SIGMETRICS International Conference on Computer Performance Modelling, Measurement and Evaluation, pp. 78–91. ACM Press, New York, NY (1986)

    Google Scholar 

  20. Marin, A., Rossi, S.: Autoreversibility: exploiting symmetries in Markov chains. In: Proceedings of MASCOTS 2013, pp. 151–160. IEEE Computer Society (2013)

    Google Scholar 

  21. Marin, A., Vigliotti, M.G.: A general result for deriving product-form solutions of Markovian models. In: Proceedings of First Joint WOSP/SIPEW International Conference on Performance Engineering, pp. 165–176. ACM, San Josè, CA, USA (2010)

    Google Scholar 

  22. Molloy, M.K.: Performance analysis using stochastic petri nets. IEEE Trans. on Comput. 31(9), 913–917 (1982)

    Article  Google Scholar 

  23. Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973–989 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  24. Plateau, B.: On the stochastic structure of parallelism and synchronization models for distributed algorithms. SIGMETRICS Perf. Eval. Rev. 13(2), 147–154 (1985)

    Article  Google Scholar 

  25. Schweitzer, P.: Aggregation methods for large Markov chains. In: Mathematical Computer Performance and Reliability (1984)

    Google Scholar 

  26. Sproston, J., Donatelli, S.: Backward bisimulation in markov chain model checking. IEEE TSE 32(8), 531–546 (2006)

    Google Scholar 

  27. Sumita, U., Reiders, M.: Lumpability and time-reversibility in the aggregation-disaggregation method for large markov chains. Commun. Stat. Stoch. Models 5, 63–81 (1989)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DAIS - Università Ca’ Foscari, Venice, Italy

    Andrea Marin & Sabina Rossi

Authors
  1. Andrea Marin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sabina Rossi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sabina Rossi .

Editor information

Editors and Affiliations

  1. Universidad de Zaragoza, Zaragoza, Spain

    Javier Campos

  2. University of Twente, Enschede, The Netherlands

    Boudewijn R. Haverkort

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Marin, A., Rossi, S. (2015). Lumping-Based Equivalences in Markovian Automata and Applications to Product-Form Analyses. In: Campos, J., Haverkort, B. (eds) Quantitative Evaluation of Systems. QEST 2015. Lecture Notes in Computer Science(), vol 9259. Springer, Cham. https://doi.org/10.1007/978-3-319-22264-6_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-22264-6_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-22263-9

  • Online ISBN: 978-3-319-22264-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation