@inproceedings{Aljazzar2010Direc-6116,
  year={2010},
  doi={10.1145/1808877.1808883},
  title={Directed and Heuristic Counterexample Generation for Probabilistic Model Checking - A Comparative Evaluation},
  isbn={978-1-60558-972-5},
  publisher={ACM Press},
  address={New York, New York, USA},
  booktitle={Proceedings of the 2010 ICSE Workshop on Quantitative Stochastic Models in the Verification and Design of Software Systems - QUOVADIS '10},
  pages={25--32},
  author={Aljazzar, Husain and Kuntz, Matthias and Leitner-Fischer, Florian and Leue, Stefan}
}

<rdf:RDF
    xmlns:dcterms="http://purl.org/dc/terms/"
    xmlns:dc="http://purl.org/dc/elements/1.1/"
    xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
    xmlns:bibo="http://purl.org/ontology/bibo/"
    xmlns:dspace="http://digital-repositories.org/ontologies/dspace/0.1.0#"
    xmlns:foaf="http://xmlns.com/foaf/0.1/"
    xmlns:void="http://rdfs.org/ns/void#"
    xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > 
  <rdf:Description rdf:about="https://kops.uni-konstanz.de/server/rdf/resource/123456789/6116">
    <dc:format>application/pdf</dc:format>
    <dcterms:bibliographicCitation>First publ. in: QUOVADIS '10 : Proceedings of the 2010 ICSE Workshop on Quantitative Stochastic Models in the Verification and Design of Software Systems May 3, 2010, Cape Town, South Africa / Carlo Ghezzi. New York, NY : ACM, 2010. pp. 25-32</dcterms:bibliographicCitation>
    <dc:contributor>Leue, Stefan</dc:contributor>
    <dcterms:abstract xml:lang="eng">The generation of counterexamples for probabilistic model checking has been an area of active research over the past five years. Tangible outcome of this research are novel directed and heuristic algorithms for efficient generation of probabilistic counterexamples, such as K* and XBF. In this paper we present an empirical evaluation of the efficiency of these algorithms and the well-known Eppstein's algorithm. We will also evaluate the effect of optimizations applied to Eppstein, K* and XBF. Additionally, we will show, how information produced during model checking can be used to guide the search for counterexamples. This is a first step towards automatically generating heuristic functions. The experimental evaluation of the various algorithms is done by applying them to one case study, known from the literature on probabilistic model checking and one case study taken from the automotive industry.</dcterms:abstract>
    <dc:contributor>Kuntz, Matthias</dc:contributor>
    <dcterms:issued>2010</dcterms:issued>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:09:38Z</dc:date>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/6116"/>
    <dcterms:title>Directed and Heuristic Counterexample Generation for Probabilistic Model Checking - A Comparative Evaluation</dcterms:title>
    <dc:language>eng</dc:language>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/6116/1/12845.pdf"/>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dc:contributor>Leitner-Fischer, Florian</dc:contributor>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:creator>Kuntz, Matthias</dc:creator>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/6116/1/12845.pdf"/>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dc:contributor>Aljazzar, Husain</dc:contributor>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:09:38Z</dcterms:available>
    <dc:creator>Leue, Stefan</dc:creator>
    <dc:creator>Aljazzar, Husain</dc:creator>
    <dc:rights>terms-of-use</dc:rights>
    <dc:creator>Leitner-Fischer, Florian</dc:creator>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
  </rdf:Description>
</rdf:RDF>