Top

Published in:

2018 | OriginalPaper | Chapter

Trace Relations and Logical Preservation for Markov Automata

Author : Arpit Sharma

Published in: Formal Modeling and Analysis of Timed Systems

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Markov automata (MAs) have been introduced in [16] as a continuous-time version of Segala’s probabilistic automata (PAs) [29]. This paper defines several variants of trace equivalence for closed MA models. These trace equivalences are obtained as a result of button pushing experiments with a black box model of MA. For every class of MA scheduler, a corresponding variant of trace equivalence has been defined. We investigate the relationship among these trace equivalences and also compare them with bisimulation for MAs. Finally, we prove that the properties specified using deterministic timed automaton (DTA) specifications and metric temporal logic (MTL) formulas are preserved under some of these trace equivalences.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Weighted Branching Systems: Behavioural Equivalence, Behavioural Distance, and Their Logical Characterisations

next chapter Non-bisimulation Based Behavioral Relations for Markov Automata

A MA is said to be closed if it is not subject to any further synchronization.

We restrict to models without zenoness. In simple words, this means that \(\tau \) cycles are not allowed.

We only consider schedulers that make a decision as soon as a state is entered. Such schedulers are called early schedulers.

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

For any MA \(\mathcal {M}\) and DTA \(\mathcal {A}\), the set \(Paths^{\mathcal {M}}(\mathcal {A})\) is measurable [17].

Note that paths satisfying an MTL formula \(\varphi \) can be written as a set of cylinder sets [34].

Aldini, A., Bernardo, M.: Expected-delay-summing weak bisimilarity for Markov automata. In: QAPL. EPTCS, vol. 194, pp. 1–15 (2015)

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

Ash, R.B., Doleans-Dade, C.A.: Probability and Measure Theory. Academic Press, New York (2000)MATH

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

Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH

Böde, E., et al.: Compositional dependability evaluation for STATEMATE. IEEE Trans. Softw. Eng. 35(2), 274–292 (2009)CrossRef

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)

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). https://doi.org/10.1007/978-3-540-75596-8_31CrossRefMATH

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)

10.

Bouyer, P.: From qualitative to quantitative analysis of timed systems. Mémoire d’habilitation, Université Paris 7, Paris, France, January 2009

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

12.

Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: Observing continuous-time MDPs by 1-clock timed automata. In: Delzanno, G., Potapov, I. (eds.) RP 2011. LNCS, vol. 6945, pp. 2–25. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24288-5_2CrossRef

13.

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). https://doi.org/10.1007/978-3-642-02658-4_18CrossRef

14.

Deng, Y., Hennessy, M.: On the semantics of Markov automata. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011. LNCS, vol. 6756, pp. 307–318. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22012-8_24CrossRefMATH

15.

Deng, Y., Hennessy, M.: On the semantics of Markov automata. Inf. Comput. 222, 139–168 (2013)MathSciNetCrossRef

16.

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

17.

Fu, H.: Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata. In: HSCC, pp. 323–332. ACM (2013)

18.

Guck, D., Hatefi, H., Hermanns, H., Katoen, J.-P., Timmer, M.: Modelling, reduction and analysis of Markov automata. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 55–71. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40196-1_5CrossRef

19.

Guck, D., Hatefi, H., Hermanns, H., Katoen, J., Timmer, M.: Analysis of timed and long-run objectives for Markov automata. LMCS 10(3) (2014)

20.

Guck, D., Timmer, M., Hatefi, H., Ruijters, E., Stoelinga, M.: Modelling and analysis of Markov reward automata. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 168–184. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11936-6_13CrossRefMATH

21.

Hatefi, H., Hermanns, H.: Model checking algorithms for Markov automata. ECEASST 53 (2012)

22.

Hermanns, H.: Interactive Markov Chains: And the Quest for Quantified Quality. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45804-2CrossRefMATH

23.

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

24.

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). https://doi.org/10.1007/978-3-642-15898-8_12CrossRef

25.

Meyer, J.F., Movaghar, A., Sanders, W.H.: Stochastic activity networks: structure, behavior, and application. In: PNPM, pp. 106–115. IEEE Computer Society (1985)

26.

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

27.

Neuhäußer, M.R., Stoelinga, M., Katoen, J.-P.: Delayed nondeterminism in continuous-time Markov decision processes. In: de Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 364–379. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00596-1_26CrossRef

28.

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). https://doi.org/10.1007/978-3-540-85778-5_1CrossRef

29.

Segala, R.: Modelling and verification of randomized distributed real time systems. Ph.D. thesis, MIT (1995)

30.

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

31.

Sharma, A.: Interactive Markovian equivalence. In: Reinecke, P., Di Marco, A. (eds.) EPEW 2017. LNCS, vol. 10497, pp. 33–49. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66583-2_3CrossRef

32.

Sharma, A.: Trace relations and logical preservation for continuous-time Markov decision processes. In: Hung, D., Kapur, D. (eds.) ICTAC 2017. LNCS, vol. 10580, pp. 192–209. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67729-3_12CrossRef

33.

Sharma, A.: Non-bisimulation based behavioral relations for Markov automata. In: Jansen, D.N., Prabhakar, P. (eds.) FORMATS 2018. LNCS, vol. 11022, pp. 179–196. Springer, Cham (2018)

34.

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). https://doi.org/10.1007/978-3-642-29709-0_28CrossRef

35.

Song, L., Zhang, L., Godskesen, J.C.: Late weak bisimulation for Markov automata. CoRR, abs/1202.4116 (2012)

36.

Timmer, M., Katoen, J.-P., van de Pol, J., Stoelinga, M.I.A.: Efficient modelling and generation of Markov automata. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 364–379. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32940-1_26CrossRef

37.

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

38.

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

Title: Trace Relations and Logical Preservation for Markov Automata
Author: Arpit Sharma
Publisher: Springer International Publishing
Book: Formal Modeling and Analysis of Timed Systems
Print ISBN: 978-3-030-00150-6

Electronic ISBN: 978-3-030-00151-3

Copyright Year: 2018
DOI: https://doi.org/10.1007/978-3-030-00151-3_10

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner