{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T10:16:26Z","timestamp":1770977786364,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642243714","type":"print"},{"value":"9783642243721","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-24372-1_33","type":"book-chapter","created":{"date-parts":[[2011,9,29]],"date-time":"2011-09-29T05:41:14Z","timestamp":1317274874000},"page":"443-452","source":"Crossref","is-referenced-by-count":20,"title":["Hierarchical Counterexamples for Discrete-Time Markov Chains"],"prefix":"10.1007","author":[{"given":"Nils","family":"Jansen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Erika","family":"\u00c1brah\u00e1m","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jens","family":"Katelaan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ralf","family":"Wimmer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernd","family":"Becker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"33_CR1","doi-asserted-by":"crossref","unstructured":"\u00c1brah\u00e1m, E., Jansen, N., Katelaan, J., Wimmer, R., Katoen, J.P., Becker, B.: Hierarchical counterexamples for discrete-time Markov chains. Tech. rep., RWTH Aachen University (2011), http:\/\/sunsite.informatik.rwth-aachen.de\/Publications\/AIB\/2011\/2011-11.pdf","DOI":"10.1007\/978-3-642-24372-1_33"},{"key":"33_CR2","first-page":"37","volume-title":"Proc. of QEST","author":"E. \u00c1brah\u00e1m","year":"2010","unstructured":"\u00c1brah\u00e1m, E., Jansen, N., Wimmer, R., Katoen, J.P., Becker, B.: DTMC model checking by SCC reduction. In: Proc. of QEST, pp. 37\u201346. IEEE CS, Los Alamitos (2010)"},{"issue":"1","key":"33_CR3","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1109\/TSE.2009.57","volume":"36","author":"H. Aljazzar","year":"2010","unstructured":"Aljazzar, H., Leue, S.: Directed explicit state-space search in the generation of counterexamples for stochastic model checking. IEEE Trans. on Software Engineering\u00a036(1), 37\u201360 (2010)","journal-title":"IEEE Trans. on Software Engineering"},{"key":"33_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-642-01702-5_15","volume-title":"Hardware and Software: Verification and Testing","author":"M.E. Andr\u00e9s","year":"2009","unstructured":"Andr\u00e9s, M.E., D\u2019Argenio, P., van Rossum, P.: Significant diagnostic counterexamples in probabilistic model checking. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol.\u00a05394, pp. 129\u2013148. Springer, Heidelberg (2009)"},{"issue":"2","key":"33_CR5","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1109\/TSE.2009.5","volume":"35","author":"T. Han","year":"2009","unstructured":"Han, T., Katoen, J.P., Damman, B.: Counterexample generation in probabilistic model checking. IEEE Trans. on Software Engineering\u00a035(2), 241\u2013257 (2009)","journal-title":"IEEE Trans. on Software Engineering"},{"key":"33_CR6","doi-asserted-by":"crossref","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6(5), 512\u2013535 (1994)","DOI":"10.1007\/BF01211866"},{"issue":"1","key":"33_CR7","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1016\/0890-5401(90)90004-2","volume":"88","author":"A. Itai","year":"1990","unstructured":"Itai, A., Rodeh, M.: Symmetry breaking in distributed networks. Information and Computation\u00a088(1), 60\u201387 (1990)","journal-title":"Information and Computation"},{"key":"33_CR8","first-page":"167","volume-title":"Proc. of QEST","author":"J.P. Katoen","year":"2009","unstructured":"Katoen, J.P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. In: Proc. of QEST, pp. 167\u2013176. IEEE CS, Los Alamitos (2009)"},{"key":"33_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M. Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"issue":"1","key":"33_CR10","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/290163.290168","volume":"1","author":"M.K. Reiter","year":"1998","unstructured":"Reiter, M.K., Rubin, A.D.: Crowds: Anonymity for web transactions. ACM Trans. on Information and System Security\u00a01(1), 66\u201392 (1998)","journal-title":"ACM Trans. on Information and System Security"},{"key":"33_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/978-3-540-93900-9_29","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R. Wimmer","year":"2009","unstructured":"Wimmer, R., Braitling, B., Becker, B.: Counterexample generation for discrete-time Markov chains using bounded model checking. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol.\u00a05403, pp. 366\u2013380. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-24372-1_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,16]],"date-time":"2019-06-16T14:27:57Z","timestamp":1560695277000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24372-1_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642243714","9783642243721"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24372-1_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}