Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Analysis of Markov Decision Processes Under Parameter Uncertainty Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

Interactive Markovian Equivalence

verfasst von : Arpit Sharma

Erschienen in: Computer Performance Engineering

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

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.

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 Bounded Aggregation for Continuous Time Markov Decision Processes
Nächstes Kapitel Delay Analysis of Resequencing Buffer in Markov Environment with HOQ-FIFO-LIFO Policy
Fußnoten
1
An IMC is said to be closed if it is not subject to any further synchronization.
 
2
We restrict to models without zenoness.
 
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
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
Note that the definition of strong bisimulation has been slightly modified to take into account the state labels.
 
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
Note that the definition of weak bisimulation has been slightly modified to take into account the state labels.
 
Literatur
1.
2.
Ash, R.B., Doleans-Dade, C.A.: Probability and Measure Theory. Academic Press, San Diego (2000)MATH
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)CrossRefMATH
4.
Baier, C., Katoen, J.-P., Hermanns, H., Wolf, V.: Comparative branching-time semantics for Markov chains. Inf. Comput. 200(2), 149–214 (2005)MathSciNetCrossRefMATH
5.
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 CrossRef
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)CrossRef
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)
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 CrossRef
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)
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.
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 CrossRef
13.
Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: LICS, pp. 342–351 (2010)
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 CrossRef
15.
Hermanns, H.: Interactive Markov Chains: The Quest for Quantified Quality. Lecture Notes in Computer Science, vol. 2428. Springer, Heidelberg (2002)MATH
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 CrossRef
17.
Hermanns, H., Katoen, J., Neuhäußer, M.R., Zhang, L.: GSPN model checking despite confusion. Technical report, RWTH Aachen University (2010)
18.
Johr, S.: Model checking compositional Markov systems, Ph.D. thesis, Saarland University (2008)
19.
Koymans, R.: Specifying real-time properties with metric temporal logic. Real Time Syst. 2(4), 255–299 (1990)CrossRef
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 CrossRef
21.
Neuhäußer, M.R.: Model checking non-deterministic and randomly timed systems, Ph.D. thesis, RWTH Aachen University (2010)
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 CrossRef
23.
24.
Sharma, A.: Reduction techniques for non-deterministic and probabilistic systems, Ph.D. thesis, RWTH Aachen university (2015)
25.
Sharma, A.: A two step perspective for Kripke structure reduction. CoRR, abs/1210.0408 (2012)
26.
27.
Wolf, V., Baier, C., Majster-Cederbaum, M.E.: Trace machines for observing continuous-time Markov chains. ENTCS 153(2), 259–277 (2006)
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)CrossRef
29.
Metadaten
Titel
Interactive Markovian Equivalence
verfasst von
Arpit Sharma
Copyright-Jahr
2017
Buch
Computer Performance Engineering

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

Electronic ISBN: 978-3-319-66583-2

Copyright-Jahr: 2017

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

Neuer Inhalt

    Bildnachweise