{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:16:44Z","timestamp":1759637804755},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319677286"},{"type":"electronic","value":"9783319677293"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-67729-3_12","type":"book-chapter","created":{"date-parts":[[2017,9,16]],"date-time":"2017-09-16T01:04:04Z","timestamp":1505523844000},"page":"192-209","source":"Crossref","is-referenced-by-count":3,"title":["Trace Relations and Logical Preservation for Continuous-Time Markov Decision Processes"],"prefix":"10.1007","author":[{"given":"Arpit","family":"Sharma","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,9,17]]},"reference":[{"issue":"2","key":"12_CR1","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"12_CR2","volume-title":"Probability and Measure Theory","author":"RB Ash","year":"2000","unstructured":"Ash, R.B., Doleans-Dade, C.A.: Probability and Measure Theory. Academic Press, Cambridge (2000)"},{"issue":"6","key":"12_CR3","doi-asserted-by":"crossref","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C Baier","year":"2003","unstructured":"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\u2013541 (2003)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/3-540-63166-6_14","volume-title":"Computer Aided Verification","author":"C Baier","year":"1997","unstructured":"Baier, C., Hermanns, H.: Weak bisimulation for fully probabilistic processes. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 119\u2013130. Springer, Heidelberg (1997). doi: 10.1007\/3-540-63166-6_14"},{"key":"12_CR5","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"issue":"2","key":"12_CR6","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/j.ic.2005.03.001","volume":"200","author":"C Baier","year":"2005","unstructured":"Baier, C., Katoen, J.-P., Hermanns, H., Wolf, V.: Comparative branching-time semantics for Markov chains. Inf. Comput. 200(2), 149\u2013214 (2005)","journal-title":"Inf. Comput."},{"issue":"1","key":"12_CR7","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.jlap.2007.02.002","volume":"72","author":"M Bernardo","year":"2007","unstructured":"Bernardo, M.: Non-bisimulation-based Markovian behavioral equivalences. J. Log. Algebr. Program. 72(1), 3\u201349 (2007)","journal-title":"J. Log. Algebr. Program."},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-540-87412-6_6","volume-title":"Computer Performance Engineering","author":"M Bernardo","year":"2008","unstructured":"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\u201378. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-87412-6_6"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Bernardo, M., De Nicola, R., Loreti, M.: Revisiting trace and testing equivalences for nondeterministic and probabilistic processes. LMCS, 10(1) (2014)","DOI":"10.2168\/LMCS-10(1:16)2014"},{"key":"12_CR10","unstructured":"Bouyer, P.: From Qualitative to Quantitative Analysis of Timed Systems. M\u00e9moire d\u2019habilitation. Universit\u00e9 Paris 7, Paris, France, January 2009"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-24288-5_2","volume-title":"Reachability Problems","author":"T Chen","year":"2011","unstructured":"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\u201325. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-24288-5_2"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"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\u2013318. IEEE Computer Society (2009)","DOI":"10.1109\/LICS.2009.21"},{"issue":"2","key":"12_CR13","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/j.ic.2009.11.002","volume":"208","author":"J Desharnais","year":"2010","unstructured":"Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Weak bisimulation is sound and complete for pCTL $${}^{\\text{* }}$$ . Inf. Comput. 208(2), 203\u2013219 (2010)","journal-title":"Inf. Comput."},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Fu, H.: Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata. In: HSCC, pp. 323\u2013332. ACM (2013)","DOI":"10.1145\/2461328.2461376"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45804-2","volume-title":"Interactive Markov Chains: And the Quest for Quantified Quality","year":"2002","unstructured":"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"},{"issue":"3","key":"12_CR16","first-page":"211","volume":"17","author":"DT Huynh","year":"1992","unstructured":"Huynh, D.T., Tian, L.: On some equivalence relations for probabilistic processes. Fundam. Inf. 17(3), 211\u2013234 (1992)","journal-title":"Fundam. Inf."},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS, pp. 266\u2013277. IEEE Computer Society (1991)","DOI":"10.1109\/LICS.1991.151651"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/BFb0039071","volume-title":"CONCUR 1990 Theories of Concurrency: Unification and Extension","author":"C-C Jou","year":"1990","unstructured":"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\u2013383. Springer, Heidelberg (1990). doi: 10.1007\/BFb0039071"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. In: POPL, pp. 344\u2013352 (1989)","DOI":"10.1145\/75277.75307"},{"key":"12_CR20","volume-title":"Modelling with Generalized Stochastic Petri Nets","author":"MA Marsan","year":"1994","unstructured":"Marsan, M.A., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with Generalized Stochastic Petri Nets, 1st edn. Wiley, Hoboken (1994)","edition":"1"},{"key":"12_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/978-3-540-74407-8_28","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"MR Neuh\u00e4u\u00dfer","year":"2007","unstructured":"Neuh\u00e4u\u00dfer, 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\u2013427. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-74407-8_28"},{"key":"12_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-642-00596-1_26","volume-title":"Foundations of Software Science and Computational Structures","author":"MR Neuh\u00e4u\u00dfer","year":"2009","unstructured":"Neuh\u00e4u\u00dfer, 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\u2013379. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-00596-1_26"},{"key":"12_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-85778-5_1","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"J Ouaknine","year":"2008","unstructured":"Ouaknine, J., Worrell, J.: Some recent results in metric temporal logic. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 1\u201313. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-85778-5_1"},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"Parma, A., Segala, R.: Axiomatization of trace semantics for stochastic nondeterministic processes. In: QEST, pp. 294\u2013303 (2004)","DOI":"10.1109\/QEST.2004.1348043"},{"key":"12_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/3-540-44618-4_25","volume-title":"CONCUR 2000 \u2014 Concurrency Theory","author":"A Philippou","year":"2000","unstructured":"Philippou, A., Lee, I., Sokolsky, O.: Weak bisimulation for probabilistic systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 334\u2013349. Springer, Heidelberg (2000). doi: 10.1007\/3-540-44618-4_25"},{"key":"12_CR26","unstructured":"Segala, R.: Modelling and verification of randomized distributed real time systems. Ph.D. thesis. MIT (1995)"},{"key":"12_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-61604-7_62","volume-title":"CONCUR 1996: Concurrency Theory","author":"R Segala","year":"1996","unstructured":"Segala, R.: Testing probabilistic automata. In: Montanari, U., Sassone, V. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 299\u2013314. Springer, Heidelberg (1996). doi: 10.1007\/3-540-61604-7_62"},{"issue":"2","key":"12_CR28","first-page":"250","volume":"2","author":"R Segala","year":"1995","unstructured":"Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. Nord. J. Comput. 2(2), 250\u2013273 (1995)","journal-title":"Nord. J. Comput."},{"key":"12_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28540-0_9","volume-title":"Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance","author":"A Sharma","year":"2012","unstructured":"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"},{"key":"12_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/978-3-642-29709-0_28","volume-title":"Perspectives of Systems Informatics","author":"A Sharma","year":"2012","unstructured":"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\u2013339. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-29709-0_28"},{"key":"12_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"464","DOI":"10.1007\/3-540-45061-0_38","volume-title":"Automata, Languages and Programming","author":"M Stoelinga","year":"2003","unstructured":"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\u2013477. Springer, Heidelberg (2003). doi: 10.1007\/3-540-45061-0_38"},{"issue":"2","key":"12_CR32","first-page":"259","volume":"153","author":"V Wolf","year":"2006","unstructured":"Wolf, V., Baier, C., Majster-Cederbaum, M.E.: Trace machines for observing continuous-time Markov chains. ENTCS 153(2), 259\u2013277 (2006)","journal-title":"ENTCS"},{"issue":"3","key":"12_CR33","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1016\/j.entcs.2006.07.019","volume":"164","author":"V Wolf","year":"2006","unstructured":"Wolf, V., Baier, C., Majster-Cederbaum, M.E.: Trace semantics for stochastic systems with nondeterminism. Electr. Notes Theo. Comput. Sci. 164(3), 187\u2013204 (2006)","journal-title":"Electr. Notes Theo. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2017"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-67729-3_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,3]],"date-time":"2019-10-03T11:18:29Z","timestamp":1570101509000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-67729-3_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319677286","9783319677293"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-67729-3_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}