{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:49:12Z","timestamp":1775868552230,"version":"3.50.1"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2015,3,31]],"date-time":"2015-03-31T00:00:00Z","timestamp":1427760000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Providing compact and understandable counterexamples for violated system\nproperties is an essential task in model checking. Existing works on\ncounterexamples for probabilistic systems so far computed either a large set of\nsystem runs or a subset of the system's states, both of which are of limited\nuse in manual debugging. Many probabilistic systems are described in a guarded\ncommand language like the one used by the popular model checker PRISM. In this\npaper we describe how a smallest possible subset of the commands can be\nidentified which together make the system erroneous. We additionally show how\nthe selected commands can be further simplified to obtain a well-understandable\ncounterexample.<\/jats:p>","DOI":"10.2168\/lmcs-11(1:15)2015","type":"journal-article","created":{"date-parts":[[2015,5,18]],"date-time":"2015-05-18T07:33:27Z","timestamp":1431934407000},"source":"Crossref","is-referenced-by-count":13,"title":["High-level Counterexamples for Probabilistic Automata"],"prefix":"10.46298","volume":"Volume 11, Issue 1","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4973-7479","authenticated-orcid":false,"given":"Ralf","family":"Wimmer","sequence":"first","affiliation":[]},{"given":"Nils","family":"Jansen","sequence":"additional","affiliation":[]},{"given":"Erika","family":"\u00c3?brah\u00c3?m","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2015,3,31]]},"reference":[{"key":"957:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/945\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/945\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:59:39Z","timestamp":1681243179000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/945"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,3,31]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-11(1:15)2015","relation":{"is-same-as":[{"id-type":"arxiv","id":"1305.5055","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1305.5055","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,3,31]]},"article-number":"945"}}