{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:11:26Z","timestamp":1774987886020,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642401954","type":"print"},{"value":"9783642401961","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40196-1_4","type":"book-chapter","created":{"date-parts":[[2013,7,23]],"date-time":"2013-07-23T01:54:56Z","timestamp":1374544496000},"page":"39-54","source":"Crossref","is-referenced-by-count":17,"title":["High-Level Counterexamples for Probabilistic Automata"],"prefix":"10.1007","author":[{"given":"Ralf","family":"Wimmer","sequence":"first","affiliation":[]},{"given":"Nils","family":"Jansen","sequence":"additional","affiliation":[]},{"given":"Andreas","family":"Vorpahl","sequence":"additional","affiliation":[]},{"given":"Erika","family":"\u00c1brah\u00e1m","sequence":"additional","affiliation":[]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[]},{"given":"Bernd","family":"Becker","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-69850-0_1","volume-title":"25 Years of Model Checking","author":"E.M. Clarke","year":"2008","unstructured":"Clarke, E.M.: The birth of model checking. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol.\u00a05000, pp. 1\u201326. Springer, Heidelberg (2008)"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-70545-1_16","volume-title":"Computer Aided Verification","author":"H. Hermanns","year":"2008","unstructured":"Hermanns, H., Wachter, B., Zhang, L.: Probabilistic CEGAR. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 162\u2013175. Springer, Heidelberg (2008)"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-540-70545-1_14","volume-title":"Computer Aided Verification","author":"M.G. Bobaru","year":"2008","unstructured":"Bobaru, M.G., P\u0103s\u0103reanu, C.S., Giannakopoulou, D.: Automated assume-guarantee reasoning by abstraction refinement. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 135\u2013148. Springer, Heidelberg (2008)"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-642-31424-7_25","volume-title":"Computer Aided Verification","author":"A. Komuravelli","year":"2012","unstructured":"Komuravelli, A., P\u0103s\u0103reanu, C.S., Clarke, E.M.: Assume-guarantee abstraction refinement for probabilistic systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 310\u2013326. Springer, Heidelberg (2012)"},{"issue":"2","key":"4_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":"4_CR7","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":"4_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":"4_CR9","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)"},{"key":"4_CR10","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)"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-642-24372-1_33","volume-title":"Automated Technology for Verification and Analysis","author":"N. Jansen","year":"2011","unstructured":"Jansen, N., \u00c1brah\u00e1m, E., Katelaan, J., Wimmer, R., Katoen, J.-P., Becker, B.: Hierarchical counterexamples for discrete-time markov chains. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol.\u00a06996, pp. 443\u2013452. Springer, Heidelberg (2011)"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-642-28756-5_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Wimmer","year":"2012","unstructured":"Wimmer, R., Jansen, N., \u00c1brah\u00e1m, E., Becker, B., Katoen, J.-P.: Minimal critical subsystems for discrete-time markov models. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 299\u2013314. Springer, Heidelberg (2012)"},{"key":"4_CR13","unstructured":"Wimmer, R., Becker, B., Jansen, N., \u00c1brah\u00e1m, E., Katoen, J.P.: Minimal critical subsystems as counterexamples for \u03c9-regular DTMC properties. In: Proc. of MBMV, 169\u2013180. Verlag Dr. Kova\u010d (2012)"},{"key":"4_CR14","unstructured":"Wimmer, R., Jansen, N., \u00c1brah\u00e1m, E., Katoen, J.P., Becker, B.: Minimal counterexamples for refuting \u03c9-regular properties of Markov decision processes. Reports of SFB\/TR 14 AVACS\u00a088 (2012) ISSN: 1860-9821, http:\/\/www.avacs.org"},{"key":"4_CR15","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley (1986)"},{"key":"4_CR16","unstructured":"Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Massachusetts Institute of Technology (1995), available as Technical Report MIT\/LCS\/TR-676"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/3-540-60218-6_17","volume-title":"CONCUR \u201995 Concurrency Theory","author":"R. Segala","year":"1995","unstructured":"Segala, R.: A compositional trace-based semantics for probabilistic automata. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol.\u00a0962, pp. 234\u2013248. Springer, Heidelberg (1995)"},{"issue":"8","key":"4_CR18","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, non-determinacy and formal derivation of programs. Communications of the ACM\u00a018(8), 453\u2013457 (1975)","journal-title":"Communications of the ACM"},{"issue":"2-3","key":"4_CR19","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1016\/S0167-6423(96)00019-6","volume":"28","author":"J. He","year":"1997","unstructured":"He, J., Seidel, K., McIver, A.: Probabilistic models for the guarded command language. Science of Computer Programming\u00a028(2-3), 171\u2013192 (1997)","journal-title":"Science of Computer Programming"},{"key":"4_CR20","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press (2008)"},{"key":"4_CR21","unstructured":"Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman & Co. Ltd. (1979)"},{"issue":"1","key":"4_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s12532-008-0001-1","volume":"1","author":"T. Achterberg","year":"2009","unstructured":"Achterberg, T.: SCIP: Solving constraint integer programs. Mathematical Programming Computation\u00a01(1), 1\u201341 (2009)","journal-title":"Mathematical Programming Computation"},{"key":"4_CR23","unstructured":"IBM: CPLEX optimization studio, version 12.5 (2012), http:\/\/www-01.ibm.com\/software\/integration\/optimization\/cplex-optimization-studio\/"},{"key":"4_CR24","unstructured":"Gurobi Optimization, Inc.: Gurobi optimizer reference manual (2012), http:\/\/www.gurobi.com"},{"key":"4_CR25","unstructured":"Wimmer, R., Jansen, N., Vorpahl, A., \u00c1brah\u00e1m, E., Katoen, J.P., Becker, B.: High-level counterexamples for probabilistic automata (extended version). Technical Report arXiv:1305.5055 (2013), http:\/\/arxiv.org\/abs\/1305.5055"},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/3-540-45605-8_11","volume-title":"Process Algebra and Probabilistic Methods. Performance Modeling and Verification","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Sproston, J.: Probabilistic model checking of the IEEE 802.11 wireless local area network protocol. In: Hermanns, H., Segala, R. (eds.) PAPM-PROBMIV 2002. LNCS, vol.\u00a02399, pp. 169\u2013187. Springer, Heidelberg (2002)"},{"key":"4_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"A. Bianco","year":"1995","unstructured":"Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol.\u00a01026, pp. 499\u2013513. Springer, Heidelberg (1995)"},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: The PRISM benchmark suite. In: Proc. of QEST, pp. 203\u2013204. IEEE CS Press (2012)","DOI":"10.1109\/QEST.2012.14"},{"issue":"1","key":"4_CR29","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1016\/0196-6774(90)90021-6","volume":"15","author":"J. Aspnes","year":"1990","unstructured":"Aspnes, J., Herlihy, M.: Fast randomized consensus using shared memory. Journal of Algorithms\u00a015(1), 441\u2013460 (1990)","journal-title":"Journal of Algorithms"},{"issue":"3","key":"4_CR30","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/s001650300009","volume":"14","author":"M. Stoelinga","year":"2003","unstructured":"Stoelinga, M.: Fun with FireWire: A comparative study of formal verification methods applied to the IEEE 1394 Root Contention Protocol. Formal Aspects of Computing\u00a014(3), 328\u2013337 (2003)","journal-title":"Formal Aspects of Computing"}],"container-title":["Lecture Notes in Computer Science","Quantitative Evaluation of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40196-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,19]],"date-time":"2019-07-19T03:42:59Z","timestamp":1563507779000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40196-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642401954","9783642401961"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40196-1_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}