Skip to main content
SpringerLink
Log in

Interactive Markovian Equivalence

  • Conference paper
  • First Online:
Computer Performance Engineering (EPEW 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10497))

Included in the following conference series:

Abstract

Behavioral equivalences relate states which are indistinguishable for an external observer of the system. This paper defines two equivalence relations, interactive Markovian equivalence (IME) and weak interactive Markovian equivalence (WIME) for closed IMCs. We define the quotient system under these relations and investigate their relationship with strong bisimulation and weak bisimulation, respectively. Next, we show that both IME and WIME can be used for repeated minimization of closed IMCs. Finally we prove that time-bounded reachability properties are preserved under IME and WIME quotienting.

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.

    An IMC is said to be closed if it is not subject to any further synchronization.

  2. 2.

    We restrict to models without zenoness.

  3. 3.

    We only consider total-time deterministic positional (TTDP) schedulers as they are sufficient for computing the maximum (resp. minimum) probability of time-bounded reachability properties [16].

  4. 4.

    Note that Pbr is not really a probability, it is a Boolean indicator of whether certain states are reached in a certain way or not.

  5. 5.

    Note that the definition of strong bisimulation has been slightly modified to take into account the state labels.

  6. 6.

    Note that WPbr is not really a probability, it is a Boolean indicator of whether certain states are reached in a certain way or not.

  7. 7.

    Note that the definition of weak bisimulation has been slightly modified to take into account the state labels.

References

  1. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  2. Ash, R.B., Doleans-Dade, C.A.: Probability and Measure Theory. Academic Press, San Diego (2000)

    MATH  Google Scholar 

  3. Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Software Eng. 29(6), 524–541 (2003)

    Article  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  5. Bernardo, M.: Non-bisimulation-based Markovian behavioral equivalences. J. Log. Algebr. Program. 72(1), 3–49 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  6. Bernardo, M.: Towards state space reduction based on T-lumpability-consistent relations. In: Thomas, N., Juiz, C. (eds.) EPEW 2008. LNCS, vol. 5261, pp. 64–78. Springer, Heidelberg (2008). doi:10.1007/978-3-540-87412-6_6

    Chapter  Google Scholar 

  7. Böde, E., Herbstritt, M., Hermanns, H., Johr, S., Peikenkamp, T., Pulungan, R., Rakow, J., Wimmer, R., Becker, B.: Compositional dependability evaluation for STATEMATE. IEEE Trans. Software Eng. 35(2), 274–292 (2009)

    Article  Google Scholar 

  8. Boudali, H., Crouzen, P., Haverkort, B.R., Kuntz, M., Stoelinga, M.: Architectural dependability evaluation with arcade. In: DSN, pp. 512–521. IEEE Computer Society (2008)

    Google Scholar 

  9. Boudali, H., Crouzen, P., Stoelinga, M.: A compositional semantics for dynamic fault trees in terms of interactive Markov chains. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 441–456. Springer, Heidelberg (2007). doi:10.1007/978-3-540-75596-8_31

    Chapter  Google Scholar 

  10. Boudali, H., Crouzen, P., Stoelinga, M.: Dynamic fault tree analysis using input/output interactive Markov chains. In: DSN, pp. 708–717. IEEE Computer Society (2007)

    Google Scholar 

  11. Bozzano, M., Cimatti, A., Katoen, J., Nguyen, V.Y., Noll, T., Roveri, M.: Safety, dependability and performance analysis of extended AADL models. Comput. J. 54(5), 754–775 (2011)

    Article  Google Scholar 

  12. Coste, N., Hermanns, H., Lantreibecq, E., Serwe, W.: Towards performance prediction of compositional models in industrial GALS designs. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 204–218. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02658-4_18

    Chapter  Google Scholar 

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

    Google Scholar 

  14. Guck, D., Han, T., Katoen, J.-P., Neuhäußer, M.R.: Quantitative timed analysis of interactive Markov chains. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 8–23. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28891-3_4

    Chapter  Google Scholar 

  15. Hermanns, H.: Interactive Markov Chains: The Quest for Quantified Quality. Lecture Notes in Computer Science, vol. 2428. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  16. Hermanns, H., Katoen, J.-P.: The how and why of interactive Markov chains. In: Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol. 6286, pp. 311–337. Springer, Heidelberg (2010). doi:10.1007/978-3-642-17071-3_16

    Chapter  Google Scholar 

  17. Hermanns, H., Katoen, J., Neuhäußer, M.R., Zhang, L.: GSPN model checking despite confusion. Technical report, RWTH Aachen University (2010)

    Google Scholar 

  18. Johr, S.: Model checking compositional Markov systems, Ph.D. thesis, Saarland University (2008)

    Google Scholar 

  19. Koymans, R.: Specifying real-time properties with metric temporal logic. Real Time Syst. 2(4), 255–299 (1990)

    Article  Google Scholar 

  20. Mateescu, R., Serwe, W.: A study of shared-memory mutual exclusion protocols using CADP. In: Kowalewski, S., Roveri, M. (eds.) FMICS 2010. LNCS, vol. 6371, pp. 180–197. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15898-8_12

    Chapter  Google Scholar 

  21. Neuhäußer, M.R.: Model checking non-deterministic and randomly timed systems, Ph.D. thesis, RWTH Aachen University (2010)

    Google Scholar 

  22. Neuhäußer, M.R., Katoen, J.-P.: Bisimulation and logical preservation for continuous-time Markov decision processes. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 412–427. Springer, Heidelberg (2007). doi:10.1007/978-3-540-74407-8_28

    Chapter  Google Scholar 

  23. Ouaknine, J., Worrell, J.: Some recent results in metric temporal logic. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 1–13. Springer, Heidelberg (2008). doi:10.1007/978-3-540-85778-5_1

    Chapter  Google Scholar 

  24. Sharma, A.: Reduction techniques for non-deterministic and probabilistic systems, Ph.D. thesis, RWTH Aachen university (2015)

    Google Scholar 

  25. Sharma, A.: A two step perspective for Kripke structure reduction. CoRR, abs/1210.0408 (2012)

    Google Scholar 

  26. Sharma, A., Katoen, J.-P.: Weighted lumpability on Markov chains. In: Clarke, E., Virbitskaite, I., Voronkov, A. (eds.) PSI 2011. LNCS, vol. 7162, pp. 322–339. Springer, Heidelberg (2012). doi:10.1007/978-3-642-29709-0_28

    Chapter  Google Scholar 

  27. Wolf, V., Baier, C., Majster-Cederbaum, M.E.: Trace machines for observing continuous-time Markov chains. ENTCS 153(2), 259–277 (2006)

    Google Scholar 

  28. Wolf, V., Baier, C., Majster-Cederbaum, M.E.: Trace semantics for stochastic systems with nondeterminism. Electr. Notes Theor. Comput. Sci. 164(3), 187–204 (2006)

    Article  Google Scholar 

  29. Zhang, L., Neuhäußer, M.R.: Model checking interactive Markov chains. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 53–68. Springer, Heidelberg (2010). doi:10.1007/978-3-642-12002-2_5

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Electrical Engineering and Computer Science, Indian Institute of Science Education and Research Bhopal, Bhopal, India

    Arpit Sharma

Authors
  1. Arpit Sharma
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Arpit Sharma .

Editor information

Editors and Affiliations

  1. Bristol, Germany

    Philipp Reinecke

  2. University of L’Aquila, L’Aquila, Italy

    Antinisca Di Marco

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Sharma, A. (2017). Interactive Markovian Equivalence. In: Reinecke, P., Di Marco, A. (eds) Computer Performance Engineering. EPEW 2017. Lecture Notes in Computer Science(), vol 10497. Springer, Cham. https://doi.org/10.1007/978-3-319-66583-2_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-66583-2_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-66582-5

  • Online ISBN: 978-3-319-66583-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation