Causality for General LTL-definable Properties

Caltais, Georgiana; Guetlein, Sophie Linnea; Leue, Stefan

Causality for General LTL-definable Properties

Dateien

Caltais_2-1ufwi8yvlv1a61.pdfGröße: 316.53 KBDownloads: 172

Datum

2019

Autor:innen

Caltais, Georgiana

Guetlein, Sophie Linnea

Leue, Stefan

Publikationstyp

Beitrag zu einem Konferenzband

Publikationsstatus

Published

Erschienen in

FINKBEINER, Bernd, ed., Samantha KLEINBERG, ed.. Proceedings 3rd Workshop on formal reasoning about Causation, Responsibility, and Explanations in Science and Technology : CREST 2018. 2019, pp. 1-15. eISSN 2075-2180. Available under: doi: 10.4204/EPTCS.286.1

Zusammenfassung

In this paper we provide a notion of causality for the violation of general Linear Temporal Logic (LTL) properties. The current work is a natural extension of the previously proposed approach handling causality in the context of LTL-definable safety properties. The major difference is that now, counterexamples of general LTL properties are not merely finite traces, but infinite lasso-shaped traces. We analyze such infinite counterexamples and identify the relevant ordered occurrences of causal events, obtained by unfolding the looping part of the lasso shaped counterexample sufficiently many times. The focus is on LTL properties from practical considerations: the current results are to be implemented in QuantUM, a tool for causality checking, that exploits explicit state LTL model checking.

Fachgebiet (DDC)

004 Informatik

Konferenz

3rd Workshop on formal reasoning about Causation, Responsibility, and Explanations in Science and Technology : CREST 2018, 21. März 2018, Thessaloniki, Greece

Zitieren

ISO 690

CALTAIS, Georgiana, Sophie Linnea GUETLEIN, Stefan LEUE, 2019. Causality for General LTL-definable Properties. 3rd Workshop on formal reasoning about Causation, Responsibility, and Explanations in Science and Technology : CREST 2018. Thessaloniki, Greece, 21. März 2018. In: FINKBEINER, Bernd, ed., Samantha KLEINBERG, ed.. Proceedings 3rd Workshop on formal reasoning about Causation, Responsibility, and Explanations in Science and Technology : CREST 2018. 2019, pp. 1-15. eISSN 2075-2180. Available under: doi: 10.4204/EPTCS.286.1

BibTex

@inproceedings{Caltais2019Causa-47110,
  year={2019},
  doi={10.4204/EPTCS.286.1},
  title={Causality for General LTL-definable Properties},
  number={286},
  series={Electronic Proceedings in Theoretical Computer Science},
  booktitle={Proceedings 3rd Workshop on formal reasoning about Causation, Responsibility, and Explanations in Science and Technology : CREST 2018},
  pages={1--15},
  editor={Finkbeiner, Bernd and Kleinberg, Samantha},
  author={Caltais, Georgiana and Guetlein, Sophie Linnea and Leue, Stefan}
}

RDF

<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/47110">
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/43615"/>
    <dcterms:abstract xml:lang="eng">In this paper we provide a notion of causality for the violation of general Linear Temporal Logic (LTL) properties. The current work is a natural extension of the previously proposed approach handling causality in the context of LTL-definable safety properties. The major difference is that now, counterexamples of general LTL properties are not merely finite traces, but infinite lasso-shaped traces. We analyze such infinite counterexamples and identify the relevant ordered occurrences of causal events, obtained by unfolding the looping part of the lasso shaped counterexample sufficiently many times. The focus is on LTL properties from practical considerations: the current results are to be implemented in QuantUM, a tool for causality checking, that exploits explicit state LTL model checking.</dcterms:abstract>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2019-10-02T10:20:29Z</dc:date>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dc:creator>Guetlein, Sophie Linnea</dc:creator>
    <dcterms:issued>2019</dcterms:issued>
    <dc:rights>terms-of-use</dc:rights>
    <dc:contributor>Leue, Stefan</dc:contributor>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/47110/1/Caltais_2-1ufwi8yvlv1a61.pdf"/>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2019-10-02T10:20:29Z</dcterms:available>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/47110/1/Caltais_2-1ufwi8yvlv1a61.pdf"/>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dc:creator>Caltais, Georgiana</dc:creator>
    <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/47110"/>
    <dc:language>eng</dc:language>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dc:contributor>Guetlein, Sophie Linnea</dc:contributor>
    <dcterms:title>Causality for General LTL-definable Properties</dcterms:title>
    <dc:creator>Leue, Stefan</dc:creator>
    <dc:contributor>Caltais, Georgiana</dc:contributor>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/43615"/>
  </rdf:Description>
</rdf:RDF>

Universitätsbibliographie

Ja