Publikation: Exploiting Adjoints in Property Directed Reachability Analysis
Lade...
Dateien
Datum
2023
Autor:innen
Herausgeber:innen
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
URI (zitierfähiger Link)
DOI (zitierfähiger Link)
ArXiv-ID
Internationale Patentnummer
Link zur Lizenz
Angaben zur Forschungsförderung
Projekt
Open Access-Veröffentlichung
Open Access Bookpart
Core Facility der Universität Konstanz
Titel in einer weiteren Sprache
Publikationstyp
Beitrag zu einem Konferenzband
Publikationsstatus
Published
Erschienen in
ENEA, Constantin, Hrsg., Akash LAL, Hrsg.. Computer Aided Verification : 35th International Conference, CAV 2023, Proceedings, Part II. Cham: Springer, 2023, S. 41-63. Lecture Notes in Computer Science (LNCS). 13965. ISBN 978-3-031-37702-0. Verfügbar unter: doi: 10.1007/978-3-031-37703-7_3
Zusammenfassung
We formulate, in lattice-theoretic terms, two novel algorithms inspired by Bradley’s property directed reachability algorithm. For finding safe invariants or counterexamples, the first algorithm exploits over-approximations of both forward and backward transition relations, expressed abstractly by the notion of adjoints. In the absence of adjoints, one can use the second algorithm, which exploits lower sets and their principals. As a notable example of application, we consider quantitative reachability problems for Markov Decision Processes.
Zusammenfassung in einer weiteren Sprache
Fachgebiet (DDC)
004 Informatik
Schlagwörter
Konferenz
Computer Aided Verification : 35th International Conference, CAV 2023, 17. Juli 2023 - 22. Juli 2023, Paris, France
Rezension
undefined / . - undefined, undefined
Zitieren
ISO 690
KORI, Mayuko, Flavio ASCARI, Filippo BONCHI, Roberto BRUNI, Roberta GORI, Ichiro HASUO, 2023. Exploiting Adjoints in Property Directed Reachability Analysis. Computer Aided Verification : 35th International Conference, CAV 2023. Paris, France, 17. Juli 2023 - 22. Juli 2023. In: ENEA, Constantin, Hrsg., Akash LAL, Hrsg.. Computer Aided Verification : 35th International Conference, CAV 2023, Proceedings, Part II. Cham: Springer, 2023, S. 41-63. Lecture Notes in Computer Science (LNCS). 13965. ISBN 978-3-031-37702-0. Verfügbar unter: doi: 10.1007/978-3-031-37703-7_3BibTex
@inproceedings{Kori2023-07Explo-76133,
title={Exploiting Adjoints in Property Directed Reachability Analysis},
year={2023},
doi={10.1007/978-3-031-37703-7_3},
number={13965},
isbn={978-3-031-37702-0},
address={Cham},
publisher={Springer},
series={Lecture Notes in Computer Science (LNCS)},
booktitle={Computer Aided Verification : 35th International Conference, CAV 2023, Proceedings, Part II},
pages={41--63},
editor={Enea, Constantin and Lal, Akash},
author={Kori, Mayuko and Ascari, Flavio and Bonchi, Filippo and Bruni, Roberto and Gori, Roberta and Hasuo, Ichiro}
}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/76133">
<dc:contributor>Bruni, Roberto</dc:contributor>
<void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
<dc:contributor>Hasuo, Ichiro</dc:contributor>
<dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/76133/1/Kori_2-c6kjw8bzv3hr7.pdf"/>
<dcterms:title>Exploiting Adjoints in Property Directed Reachability Analysis</dcterms:title>
<dc:language>eng</dc:language>
<dcterms:issued>2023-07</dcterms:issued>
<dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
<bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/76133"/>
<dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2026-02-05T14:08:02Z</dcterms:available>
<dc:contributor>Gori, Roberta</dc:contributor>
<dc:creator>Ascari, Flavio</dc:creator>
<dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
<dc:creator>Bruni, Roberto</dc:creator>
<dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2026-02-05T14:08:02Z</dc:date>
<dc:contributor>Bonchi, Filippo</dc:contributor>
<dc:rights>Attribution 4.0 International</dc:rights>
<foaf:homepage rdf:resource="http://localhost:8080/"/>
<dc:creator>Kori, Mayuko</dc:creator>
<dc:creator>Gori, Roberta</dc:creator>
<dcterms:abstract>We formulate, in lattice-theoretic terms, two novel algorithms inspired by Bradley’s property directed reachability algorithm. For finding safe invariants or counterexamples, the first algorithm exploits over-approximations of both forward and backward transition relations, expressed abstractly by the notion of adjoints. In the absence of adjoints, one can use the second algorithm, which exploits lower sets and their principals. As a notable example of application, we consider quantitative reachability problems for Markov Decision Processes.</dcterms:abstract>
<dcterms:rights rdf:resource="http://creativecommons.org/licenses/by/4.0/"/>
<dc:creator>Hasuo, Ichiro</dc:creator>
<dc:contributor>Kori, Mayuko</dc:contributor>
<dc:contributor>Ascari, Flavio</dc:contributor>
<dc:creator>Bonchi, Filippo</dc:creator>
<dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/76133/1/Kori_2-c6kjw8bzv3hr7.pdf"/>
</rdf:Description>
</rdf:RDF>Interner Vermerk
xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter
Prüfungsdatum der Dissertation
Finanzierungsart
Kommentar zur Publikation
Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Nein
