Skip to main content

2018 | OriginalPaper | Buchkapitel

Trace Relations and Logical Preservation for Markov Automata

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

search-config
loading …

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.

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!

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!

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!

Fußnoten
1
A MA is said to be closed if it is not subject to any further synchronization.
 
2
We restrict to models without zenoness. In simple words, this means that \(\tau \) cycles are not allowed.
 
3
We only consider schedulers that make a decision as soon as a state is entered. Such schedulers are called early schedulers.
 
4
Note that the definition of strong bisimulation has been slightly modified to take into account the state labels.
 
5
For any MA \(\mathcal {M}\) and DTA \(\mathcal {A}\), the set \(Paths^{\mathcal {M}}(\mathcal {A})\) is measurable [17].
 
6
Note that paths satisfying an MTL formula \(\varphi \) can be written as a set of cylinder sets [34].
 
Literatur
1.
Zurück zum Zitat Aldini, A., Bernardo, M.: Expected-delay-summing weak bisimilarity for Markov automata. In: QAPL. EPTCS, vol. 194, pp. 1–15 (2015) Aldini, A., Bernardo, M.: Expected-delay-summing weak bisimilarity for Markov automata. In: QAPL. EPTCS, vol. 194, pp. 1–15 (2015)
3.
Zurück zum Zitat Ash, R.B., Doleans-Dade, C.A.: Probability and Measure Theory. Academic Press, New York (2000)MATH Ash, R.B., Doleans-Dade, C.A.: Probability and Measure Theory. Academic Press, New York (2000)MATH
4.
Zurück zum Zitat 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., 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
5.
Zurück zum Zitat Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH
6.
Zurück zum Zitat Böde, E., et al.: Compositional dependability evaluation for STATEMATE. IEEE Trans. Softw. Eng. 35(2), 274–292 (2009)CrossRef Böde, E., et al.: Compositional dependability evaluation for STATEMATE. IEEE Trans. Softw. Eng. 35(2), 274–292 (2009)CrossRef
7.
Zurück zum Zitat 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., Haverkort, B.R., Kuntz, M., Stoelinga, M.: Architectural dependability evaluation with arcade. In: DSN, pp. 512–521. IEEE Computer Society (2008)
9.
Zurück zum Zitat 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) 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.
Zurück zum Zitat Bouyer, P.: From qualitative to quantitative analysis of timed systems. Mémoire d’habilitation, Université Paris 7, Paris, France, January 2009 Bouyer, P.: From qualitative to quantitative analysis of timed systems. Mémoire d’habilitation, Université Paris 7, Paris, France, January 2009
11.
Zurück zum Zitat 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 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
16.
Zurück zum Zitat Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: LICS, pp. 342–351 (2010) Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: LICS, pp. 342–351 (2010)
17.
Zurück zum Zitat Fu, H.: Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata. In: HSCC, pp. 323–332. ACM (2013) Fu, H.: Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata. In: HSCC, pp. 323–332. ACM (2013)
19.
Zurück zum Zitat Guck, D., Hatefi, H., Hermanns, H., Katoen, J., Timmer, M.: Analysis of timed and long-run objectives for Markov automata. LMCS 10(3) (2014) Guck, D., Hatefi, H., Hermanns, H., Katoen, J., Timmer, M.: Analysis of timed and long-run objectives for Markov automata. LMCS 10(3) (2014)
21.
Zurück zum Zitat Hatefi, H., Hermanns, H.: Model checking algorithms for Markov automata. ECEASST 53 (2012) Hatefi, H., Hermanns, H.: Model checking algorithms for Markov automata. ECEASST 53 (2012)
23.
Zurück zum Zitat Hermanns, H., Katoen, J., Neuhäußer, M.R., Zhang, L.: GSPN model checking despite confusion. Technical report, RWTH Aachen University (2010) Hermanns, H., Katoen, J., Neuhäußer, M.R., Zhang, L.: GSPN model checking despite confusion. Technical report, RWTH Aachen University (2010)
25.
Zurück zum Zitat Meyer, J.F., Movaghar, A., Sanders, W.H.: Stochastic activity networks: structure, behavior, and application. In: PNPM, pp. 106–115. IEEE Computer Society (1985) 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.
Zurück zum Zitat 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) 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)
29.
Zurück zum Zitat Segala, R.: Modelling and verification of randomized distributed real time systems. Ph.D. thesis, MIT (1995) Segala, R.: Modelling and verification of randomized distributed real time systems. Ph.D. thesis, MIT (1995)
30.
Zurück zum Zitat Sharma, A.: Reduction techniques for non-deterministic and probabilistic systems. Ph.D. dissertation, RWTH Aachen (2015) Sharma, A.: Reduction techniques for non-deterministic and probabilistic systems. Ph.D. dissertation, RWTH Aachen (2015)
33.
Zurück zum Zitat 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) 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)
35.
Zurück zum Zitat Song, L., Zhang, L., Godskesen, J.C.: Late weak bisimulation for Markov automata. CoRR, abs/1202.4116 (2012) Song, L., Zhang, L., Godskesen, J.C.: Late weak bisimulation for Markov automata. CoRR, abs/1202.4116 (2012)
37.
Zurück zum Zitat Wolf, V., Baier, C., Majster-Cederbaum, M.E.: Trace machines for observing continuous-time Markov chains. ENTCS 153(2), 259–277 (2006) Wolf, V., Baier, C., Majster-Cederbaum, M.E.: Trace machines for observing continuous-time Markov chains. ENTCS 153(2), 259–277 (2006)
38.
Zurück zum Zitat 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 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
Metadaten
Titel
Trace Relations and Logical Preservation for Markov Automata
verfasst von
Arpit Sharma
Copyright-Jahr
2018
DOI
https://doi.org/10.1007/978-3-030-00151-3_10