{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T03:23:49Z","timestamp":1777519429060,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642214608","type":"print"},{"value":"9783642214615","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-21461-5_5","type":"book-chapter","created":{"date-parts":[[2011,6,10]],"date-time":"2011-06-10T09:25:36Z","timestamp":1307697936000},"page":"75-89","source":"Crossref","is-referenced-by-count":6,"title":["Counterexample Generation for Markov Chains Using SMT-Based Bounded Model Checking"],"prefix":"10.1007","author":[{"given":"Bettina","family":"Braitling","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ralf","family":"Wimmer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernd","family":"Becker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nils","family":"Jansen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Erika","family":"\u00c1brah\u00e1m","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5_CR1","volume-title":"Principles of Model Checking","author":"C. Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"issue":"8","key":"5_CR2","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers\u00a035(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Computers"},{"issue":"1","key":"5_CR3","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E.M. Clarke","year":"2001","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design\u00a019(1), 7\u201334 (2001)","journal-title":"Formal Methods in System Design"},{"issue":"5","key":"5_CR4","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing\u00a06(5), 512\u2013535 (1994)","journal-title":"Formal Aspects of Computing"},{"key":"5_CR5","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":"5_CR6","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":"5_CR7","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)"},{"issue":"1","key":"5_CR8","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":"5_CR9","doi-asserted-by":"crossref","unstructured":"\u00c1brah\u00e1m, E., Jansen, N., Wimmer, R., Katoen, J.P., Becker, B.: DTMC model checking by SCC reduction. In: Proc. of QEST, IEEE CS, pp. 37\u201346 (2010)","DOI":"10.1109\/QEST.2010.13"},{"key":"5_CR10","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems (TOPLAS)\u00a01, 245\u2013257 (1979)","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-540-71209-1_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Han","year":"2007","unstructured":"Han, T., Katoen, J.-P.: Counterexamples in probabilistic model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 72\u201386. Springer, Heidelberg (2007)"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-540-71209-1_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","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: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 87\u2013101. Springer, Heidelberg (2007)"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Derisavi, S.: Signature-based symbolic algorithm for optimal Markov chain lumping. In: Proc. of QEST, IEEE CS, pp. 141\u2013150 (2007)","DOI":"10.1109\/QEST.2007.27"},{"issue":"9","key":"5_CR14","doi-asserted-by":"publisher","first-page":"815","DOI":"10.1016\/j.peva.2009.12.008","volume":"67","author":"R. Wimmer","year":"2010","unstructured":"Wimmer, R., Derisavi, S., Hermanns, H.: Symbolic partition refinement with automatic balancing of time and space. Perf. Eval.\u00a067(9), 815\u2013835 (2010)","journal-title":"Perf. Eval."},{"key":"5_CR15","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-1-4899-5327-8_25","volume":"Part 2","author":"G.S. Tseitin","year":"1970","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic\u00a0Part 2, 115\u2013125 (1970)","journal-title":"Studies in Constructive Mathematics and Mathematical Logic"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"issue":"6","key":"5_CR17","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1145\/3812.3818","volume":"28","author":"S. Even","year":"1985","unstructured":"Even, S., Goldreich, O., Lempel, A.: A randomized protocol for signing contracts. Communications of the ACM\u00a028(6), 637\u2013647 (1985)","journal-title":"Communications of the ACM"},{"issue":"6","key":"5_CR18","doi-asserted-by":"publisher","first-page":"561","DOI":"10.3233\/JCS-2006-14604","volume":"14","author":"G. Norman","year":"2006","unstructured":"Norman, G., Shmatikov, V.: Analysis of probabilistic contract signing. Journal of Computer Security\u00a014(6), 561\u2013589 (2006)","journal-title":"Journal of Computer Security"},{"issue":"1","key":"5_CR19","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/290163.290168","volume":"1","author":"M. Reiter","year":"1998","unstructured":"Reiter, M., Rubin, A.: Crowds: Anonymity for web transactions. ACM Transactions on Information and System Security (TISSEC)\u00a01(1), 66\u201392 (1998)","journal-title":"ACM Transactions on Information and System Security (TISSEC)"},{"issue":"1","key":"5_CR20","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"},{"issue":"6","key":"5_CR21","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0020-0190(94)90103-1","volume":"49","author":"Z. Collin","year":"1994","unstructured":"Collin, Z., Dolev, S.: Self-stabilizing depth-first search. Information Processing Letters\u00a049(6), 297\u2013301 (1994)","journal-title":"Information Processing Letters"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/11691372_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Hinton","year":"2006","unstructured":"Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol.\u00a03920, pp. 441\u2013444. Springer, Heidelberg (2006)"},{"key":"5_CR23","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1145\/1772630.1772635","volume-title":"Int\u2019l Workshop on Dynamic Aspects in Dependability Models for Fault-Tolerant Systems (DYADEM-FTS)","author":"M. G\u00fcnther","year":"2010","unstructured":"G\u00fcnther, M., Schuster, J., Siegle, M.: Symbolic calculation of k-shortest paths and related measures with the stochastic process algebra tool Caspa. In: Int\u2019l Workshop on Dynamic Aspects in Dependability Models for Fault-Tolerant Systems (DYADEM-FTS), pp. 13\u201318. ACM Press, New York (2010)"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21461-5_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,11]],"date-time":"2019-06-11T12:20:07Z","timestamp":1560255607000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21461-5_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642214608","9783642214615"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21461-5_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}