{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T14:37:12Z","timestamp":1742395032922},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540733676"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73368-3_37","type":"book-chapter","created":{"date-parts":[[2007,8,29]],"date-time":"2007-08-29T22:29:34Z","timestamp":1188426574000},"page":"311-324","source":"Crossref","is-referenced-by-count":46,"title":["Three-Valued Abstraction for Continuous-Time Markov Chains"],"prefix":"10.1007","author":[{"given":"Joost-Pieter","family":"Katoen","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Klink","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Leucker","sequence":"additional","affiliation":[]},{"given":"Verena","family":"Wolf","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"37_CR1","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1145\/343369.343402","volume":"1","author":"A. Aziz","year":"2000","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model-checking continuous time Markov chains. ACM TOCL\u00a01, 162\u2013170 (2000)","journal-title":"ACM TOCL"},{"key":"37_CR2","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.tcs.2005.07.022","volume":"345","author":"C. Baier","year":"2005","unstructured":"Baier, C., Hermanns, H., Katoen, J.P., Haverkort, B.R.H.M.: Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. TCS\u00a0345, 2\u201326 (2005)","journal-title":"TCS"},{"key":"37_CR3","first-page":"524","volume":"29","author":"C. Baier","year":"2003","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE TSE\u00a029, 524\u2013541 (2003)","journal-title":"IEEE TSE"},{"key":"37_CR4","doi-asserted-by":"publisher","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. Information and Computation\u00a0200, 149\u2013214 (2005)","journal-title":"Information and Computation"},{"key":"37_CR5","doi-asserted-by":"crossref","unstructured":"Bause, F., Kritzinger, P.S.: Stochastic Petri nets: An introduction to the theory. SIGMETRICS Performance Evaluation Review 26 (1998)","DOI":"10.1145\/288197.581194"},{"key":"37_CR6","first-page":"189","volume-title":"QEST","author":"M. Mamoun Ben","year":"2006","unstructured":"Ben Mamoun, M., Pekergin, N., Youn\u00e8s, S.: Model checking of continuous-time Markov chains by closed-form bounding distributions. In: QEST, pp. 189\u2013198. IEEE CS, Los Alamitos (2006)"},{"key":"37_CR7","first-page":"167","volume-title":"QEST","author":"E. B\u00f6de","year":"2006","unstructured":"B\u00f6de, E., Herbstritt, M., Hermanns, H., Johr, S., Peikenkamp, T., Pulungan, R., Wimmer, R., Becker, B.: Compositional performability evaluation for Statemate. In: QEST, pp. 167\u2013178. IEEE CS, Los Alamitos (2006)"},{"key":"37_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1007\/978-3-540-45232-4_6","volume-title":"Computer Performance Evaluations. Modelling Techniques and Tools","author":"G. Ciardo","year":"2003","unstructured":"Ciardo, G., Jones III, R.L., Miner, A., Siminiceanu, R.: Logical and stochastic modeling with SMART. In: Kemper, P., Sanders, W.H. (eds.) TOOLS 2003. LNCS, vol.\u00a02794, pp. 78\u201397. Springer, Heidelberg (2003)"},{"key":"37_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"543","DOI":"10.1007\/978-3-540-30182-0_55","volume-title":"Computer and Information Sciences - ISCIS 2004","author":"D. D\u2019Aprile","year":"2004","unstructured":"D\u2019Aprile, D., Donatelli, S., Sproston, J.: CSL model checking for the GreatSPN tool. In: Aykanat, C., Dayar, T., K\u00f6rpeo\u011flu, \u0130. (eds.) ISCIS 2004. LNCS, vol.\u00a03280, pp. 543\u2013553. Springer, Heidelberg (2004)"},{"key":"37_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-44804-7_3","volume-title":"Process Algebra and Probabilistic Methods. Performance Modelling and Verification","author":"P.R. D\u2019Argenio","year":"2001","unstructured":"D\u2019Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reachability analysis of probabilistic systems by successive refinements. In: de Luca, L., Gilmore, S.T. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol.\u00a02165, pp. 39\u201356. Springer, Heidelberg (2001)"},{"key":"37_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/11691617_5","volume-title":"Model Checking Software","author":"H. Fecher","year":"2006","unstructured":"Fecher, H., Leucker, M., Wolf, V.: Don\u2019t know in probabilistic systems. In: Valmari, A. (ed.) Model Checking Software. LNCS, vol.\u00a03925, pp. 71\u201388. Springer, Heidelberg (2006)"},{"key":"37_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/3-540-58021-2_20","volume-title":"Computer Performance Evaluation","author":"S. Gilmore","year":"1994","unstructured":"Gilmore, S., Hillston, J.: The PEPA workbench: A tool to support a process algebra-based approach to performance modelling. In: Haring, G., Kotsis, G. (eds.) Computer Performance Evaluation. LNCS, vol.\u00a0794, pp. 353\u2013368. Springer, Heidelberg (1994)"},{"key":"37_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/11804192_19","volume-title":"Formal Methods for Components and Objects","author":"M. Groesser","year":"2006","unstructured":"Groesser, M., Baier, C.: Partial order reduction for Markov decision processes: a survey. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 408\u2013427. Springer, Heidelberg (2006)"},{"key":"37_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1007\/978-3-540-24611-4_12","volume-title":"Validation of Stochastic Systems","author":"M. Huth","year":"2004","unstructured":"Huth, M.: An abstraction framework for mixed non-deterministic and probabilistic systems. In: Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol.\u00a02925, pp. 419\u2013444. Springer, Heidelberg (2004)"},{"key":"37_CR15","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/j.tcs.2005.08.008","volume":"346","author":"M. Huth","year":"2005","unstructured":"Huth, M.: On finite-state approximants for probabilistic computation tree logic. TCS\u00a0346, 113\u2013134 (2005)","journal-title":"TCS"},{"key":"37_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/978-3-540-71209-1_9","volume-title":"TACAS 2007","author":"J.-P. Katoen","year":"2007","unstructured":"Katoen, J.-P., Kemna, T., Zapreev, I., Jansen, D.N.: Bisimulation minimisation mostly speeds up probabilistic model checking. In: TACAS 2007. LNCS, vol.\u00a04424, pp. 87\u2013102. Springer, Heidelberg (2007)"},{"key":"37_CR17","first-page":"243","volume-title":"QEST","author":"J.-P. Katoen","year":"2005","unstructured":"Katoen, J.-P., Khattri, M., Zapreev, I.S.: A Markov reward model checker. In: QEST, pp. 243\u2013244. IEEE Computer Society Press, Los Alamitos (2005)"},{"key":"37_CR18","first-page":"157","volume-title":"QEST","author":"M. Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Game-based abstraction for Markov decision processes. In: QEST, pp. 157\u2013166. IEEE Computer Society Press, Los Alamitos (2006)"},{"key":"37_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/11817963_23","volume-title":"Computer Aided Verification","author":"M. Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Symmetry reduction for probabilistic model checking. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 234\u2013248. Springer, Heidelberg (2006)"},{"key":"37_CR20","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/j.scico.2005.02.008","volume":"58","author":"D. Monniaux","year":"2005","unstructured":"Monniaux, D.: Abstract interpretation of programs as Markov decision processes. Science of Computer Programming\u00a058, 179\u2013205 (2005)","journal-title":"Science of Computer Programming"},{"key":"37_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1007\/978-3-540-31980-1_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Remke","year":"2005","unstructured":"Remke, A., Haverkort, B.R., Cloth, L.: Model checking infinite-state Markov chains. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 237\u2013252. Springer, Heidelberg (2005)"},{"key":"37_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/11691372_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Sen","year":"2006","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Model-checking Markov chains in the presence of uncertainties. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920, pp. 394\u2013410. Springer, Heidelberg (2006)"},{"key":"37_CR23","first-page":"531","volume":"32","author":"J. Sproston","year":"2006","unstructured":"Sproston, J., Donatelli, S.: Backward bisimulation in Markov chain model checking. IEEE TSE\u00a032, 531\u2013546 (2006)","journal-title":"IEEE TSE"},{"key":"37_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/978-3-540-71209-1_14","volume-title":"TACAS 2007","author":"L. Zhang","year":"2007","unstructured":"Zhang, L., Hermanns, H., Eisenbrand, F., Jansen, D.N.: Flow faster: efficient decision algorithms for probabilistic simulations. In: TACAS 2007. LNCS, vol.\u00a04424, pp. 155\u2013170. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73368-3_37.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:08:33Z","timestamp":1619518113000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73368-3_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540733676"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73368-3_37","relation":{},"subject":[]}}