nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

Trace Relations and Logical Preservation for Continuous-Time Markov Decision Processes

verfasst von : Arpit Sharma

Erschienen in: Theoretical Aspects of Computing – ICTAC 2017

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

Equivalence relations are widely used for comparing the behavior of stochastic systems. This paper introduces several variants of trace equivalence for continuous-time Markov decision processes (CTMDPs). These trace equivalences are obtained as a result of button pushing experiments with a black box model of CTMDP. For every class of CTMDP scheduler, a corresponding variant of trace equivalence has been introduced. We investigate the relationship among these trace equivalences and also compare them with bisimulation for CTMDPs. 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!

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 Polynomial Time Learner for Inferring Subclasses of Internal Contextual Grammars with Local Maximum Selectors

Nächstes Kapitel Constructing Cycles in the Simplex Method for DPLL(T)

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

A CTMDP in which the delay time distribution per state visit is the same for all states.

Note that the exit rate of \(s_{3}\) for both \(\alpha \) and \(\beta \) is the same. This is in accordance with the assumption that the exit rates need to be the same for any state s with \(|Act(s)|>1\).

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

Ash, R.B., Doleans-Dade, C.A.: Probability and Measure Theory. Academic Press, Cambridge (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)CrossRefMATH

Baier, C., Hermanns, H.: Weak bisimulation for fully probabilistic processes. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 119–130. Springer, Heidelberg (1997). doi:10.1007/3-540-63166-6_14 CrossRef

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

Baier, C., Katoen, J.-P., Hermanns, H., Wolf, V.: Comparative branching-time semantics for Markov chains. Inf. Comput. 200(2), 149–214 (2005)MathSciNetCrossRefMATH

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

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

Bernardo, M., De Nicola, R., Loreti, M.: Revisiting trace and testing equivalences for nondeterministic and probabilistic processes. LMCS, 10(1) (2014)

10.

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

11.

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). doi:10.1007/978-3-642-24288-5_2 CrossRef

12.

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. IEEE Computer Society (2009)

13.

Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Weak bisimulation is sound and complete for pCTL\({}^{\text{* }}\). Inf. Comput. 208(2), 203–219 (2010)MathSciNetCrossRefMATH

14.

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

15.

Hermanns, H. (ed.): Interactive Markov Chains: And the Quest for Quantified Quality. LNCS, vol. 2428. Springer, Heidelberg (2002). doi:10.1007/3-540-45804-2 MATH

16.

Huynh, D.T., Tian, L.: On some equivalence relations for probabilistic processes. Fundam. Inf. 17(3), 211–234 (1992)MathSciNetMATH

17.

Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS, pp. 266–277. IEEE Computer Society (1991)

18.

Jou, C.-C., Smolka, S.A.: Equivalences, congruences, and complete axiomatizations for probabilistic processes. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 367–383. Springer, Heidelberg (1990). doi:10.1007/BFb0039071 CrossRef

19.

Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. In: POPL, pp. 344–352 (1989)

20.

Marsan, M.A., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with Generalized Stochastic Petri Nets, 1st edn. Wiley, Hoboken (1994)MATH

21.

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

22.

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

23.

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). doi:10.1007/978-3-540-85778-5_1 CrossRef

24.

Parma, A., Segala, R.: Axiomatization of trace semantics for stochastic nondeterministic processes. In: QEST, pp. 294–303 (2004)

25.

Philippou, A., Lee, I., Sokolsky, O.: Weak bisimulation for probabilistic systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 334–349. Springer, Heidelberg (2000). doi:10.1007/3-540-44618-4_25 CrossRef

26.

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

27.

Segala, R.: Testing probabilistic automata. In: Montanari, U., Sassone, V. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 299–314. Springer, Heidelberg (1996). doi:10.1007/3-540-61604-7_62

28.

Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. Nord. J. Comput. 2(2), 250–273 (1995)MathSciNetMATH

29.

Sharma, A.: Weighted probabilistic equivalence preserves \(\upomega \)-regular properties. In: Schmitt, J.B. (ed.) MMB&DFT. LNCS. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28540-0_9

30.

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). doi:10.1007/978-3-642-29709-0_28 CrossRef

31.

Stoelinga, M., Vaandrager, F.: A testing scenario for probabilistic automata. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 464–477. Springer, Heidelberg (2003). doi:10.1007/3-540-45061-0_38 CrossRef

32.

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

33.

Wolf, V., Baier, C., Majster-Cederbaum, M.E.: Trace semantics for stochastic systems with nondeterminism. Electr. Notes Theo. Comput. Sci. 164(3), 187–204 (2006)CrossRef

Titel: Trace Relations and Logical Preservation for Continuous-Time Markov Decision Processes
verfasst von: Arpit Sharma
Verlag: Springer International Publishing
Buch: Theoretical Aspects of Computing – ICTAC 2017
Print ISBN: 978-3-319-67728-6

Electronic ISBN: 978-3-319-67729-3

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-67729-3_12

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"