nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Non-bisimulation Based Behavioral Relations for Markov Automata

verfasst von : Arpit Sharma

Erschienen in: Formal Modeling and Analysis of Timed Systems

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Markov automata (MAs) [16] extend probabilistic automata (PAs) [29] with stochastic aspects [22]. This paper defines two equivalence relations, namely, weighted Markovian equivalence (WME) and weak weighted Markovian equivalence (WWME) for the subclass of closed MAs. We define the quotient system under these relations and investigate their relationship with strong bisimulation and weak bisimulation, respectively. Next, we show that both WME and WWME can be used for repeated minimization of closed MAs. Finally, we prove that properties specified using deterministic timed automaton (DTA) specifications and metric temporal logic (MTL) formulas are preserved under WME and WWME quotienting.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel Trace Relations and Logical Preservation for Markov Automata

Nächstes Kapitel Distance on Timed Words and Applications

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.

Since our closed MA models do not allow multiple action transitions, schedulers are not required for resolving non-deterministic choices.

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 [11, 17, 33].

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

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

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

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). https://doi.org/10.1007/978-3-540-87412-6_6CrossRef

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)

Bouyer, P.: From Qualitative to Quantitative Analysis of Timed Systems. Mémoire d’habilitation, Université Paris 7, Paris, France, January 2009

10.

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

11.

Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: Quantitative model checking of continuous-time Markov chains against timed automata specifications. In: LICS, pp. 309–318 (2009)

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

13.

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

14.

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

15.

Eisentraut, C., Godskesen, J.C., Hermanns, H., Song, L., Zhang, L.: Probabilistic bisimulation for realistic schedulers. In: Bjørner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 248–264. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19249-9_16CrossRef

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), 1–29 (2014)MathSciNetMATH

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. In: ECEASST, vol. 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.-P.: The how and why of interactive Markov chains. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol. 6286, pp. 311–337. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17071-3_16CrossRefMATH

24.

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

25.

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

26.

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

27.

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

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 Markov automata. In: Jansen, D.N., Prabhakar, P. (eds.) FORMATS 2018, LNCS 11022, pp. 162–178. Springer, Cham (2018)

33.

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

34.

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

35.

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

36.

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

Titel: Non-bisimulation Based Behavioral Relations for Markov Automata
verfasst von: Arpit Sharma
Verlag: Springer International Publishing
Buch: Formal Modeling and Analysis of Timed Systems
Print ISBN: 978-3-030-00150-6

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

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-030-00151-3_11

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"