Revisiting Trace Equivalences for Markov Automata

  • Arpit SharmaEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 12018)


Equivalences are important for system synthesis as well as system analysis. This paper defines new variants of trace equivalence for Markov automata (MAs). We perform button pushing experiments with a black box model of MA to obtain these equivalences. For every class of MA scheduler, a corresponding variant of trace equivalence is defined. We investigate the relationship among these equivalences and also prove that each variant defined in this paper is strictly coarser than the corresponding variant of trace equivalence defined originally in [12]. Next, we establish the relationship between our equivalences and bisimulation for MAs. Finally, we investigate the relationship of these equivalences with trace relations defined in the literature for some of the implied models.


Markov Scheduler Equivalence Trace Bisimulation Stochastic 


  1. 1.
    Aldini, A., Bernardo, M.: Expected-delay-summing weak bisimilarity for Markov automata. In: QAPL. EPTCS, vol. 194, pp. 1–15 (2015)Google Scholar
  2. 2.
    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)CrossRefGoogle Scholar
  3. 3.
    Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)zbMATHGoogle Scholar
  4. 4.
    Bernardo, M., De Nicola, R., Loreti, M.: Revisiting trace and testing equivalences for nondeterministic and probabilistic processes. In: Birkedal, L. (ed.) FoSSaCS 2012. LNCS, vol. 7213, pp. 195–209. Springer, Heidelberg (2012). Scholar
  5. 5.
    Bernardo, M., De Nicola, R., Loreti, M.: Revisiting trace and testing equivalences for nondeterministic and probabilistic processes. In: LMCS, vol. 10, no. 1 (2014)Google Scholar
  6. 6.
    Deng, Y., Hennessy, M.: On the semantics of Markov automata. Inf. Comput. 222, 139–168 (2013)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Eisentraut, C., Hermanns, H., Zhang, L.: Concurrency and composition in a stochastic world. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 21–39. Springer, Heidelberg (2010). Scholar
  8. 8.
    Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: LICS, pp. 342–351 (2010)Google Scholar
  9. 9.
    Hermanns, H.: Interactive Markov Chains: And the Quest for Quantified Quality. LNCS, vol. 2428. Springer, Heidelberg (2002). Scholar
  10. 10.
    Segala, R.: A compositional trace-based semantics for probabilistic automata. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 234–248. Springer, Heidelberg (1995). Scholar
  11. 11.
    Segala, R.: Modelling and verification of randomized distributed real time systems. Ph.D. thesis, MIT (1995)Google Scholar
  12. 12.
    Sharma, A.: Trace relations and logical preservation for Markov automata. In: Jansen, D.N., Prabhakar, P. (eds.) FORMATS 2018. LNCS, vol. 11022, pp. 162–178. Springer, Cham (2018). Scholar
  13. 13.
    Sharma, A.: Stuttering for Markov automata. In: TASE. IEEE Computer Society (2019)Google Scholar
  14. 14.
    Song, L., Zhang, L., Godskesen, J.C.: Late weak bisimulation for Markov automata. CoRR abs/1202.4116 (2012)Google Scholar
  15. 15.
    Wolf, V., Baier, C., Majster-Cederbaum, M.E.: Trace machines for observing continuous-time Markov chains. ENTCS 153(2), 259–277 (2006)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.EECS DepartmentIndian Institute of Science Education and Research BhopalBhopalIndia

Personalised recommendations