Exploiting Adjoints in Property Directed Reachability Analysis
| dc.contributor.author | Kori, Mayuko | |
| dc.contributor.author | Ascari, Flavio | |
| dc.contributor.author | Bonchi, Filippo | |
| dc.contributor.author | Bruni, Roberto | |
| dc.contributor.author | Gori, Roberta | |
| dc.contributor.author | Hasuo, Ichiro | |
| dc.date.accessioned | 2026-02-05T14:08:02Z | |
| dc.date.available | 2026-02-05T14:08:02Z | |
| dc.date.issued | 2023-07 | |
| dc.description.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. | |
| dc.description.version | published | deu |
| dc.identifier.arxiv | 2307.02817 | |
| dc.identifier.doi | 10.1007/978-3-031-37703-7_3 | |
| dc.identifier.ppn | 1960568477 | |
| dc.identifier.uri | https://kops.uni-konstanz.de/handle/123456789/76133 | |
| dc.language.iso | eng | |
| dc.rights | Attribution 4.0 International | |
| dc.rights.uri | http://creativecommons.org/licenses/by/4.0/ | |
| dc.subject.ddc | 004 | |
| dc.title | Exploiting Adjoints in Property Directed Reachability Analysis | eng |
| dc.type | INPROCEEDINGS | |
| dspace.entity.type | Publication | |
| kops.citation.bibtex | @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}
} | |
| kops.citation.iso690 | 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_3 | deu |
| kops.citation.iso690 | 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, Jul 17, 2023 - Jul 22, 2023. In: ENEA, Constantin, ed., Akash LAL, ed.. Computer Aided Verification : 35th International Conference, CAV 2023, Proceedings, Part II. Cham: Springer, 2023, pp. 41-63. Lecture Notes in Computer Science (LNCS). 13965. ISBN 978-3-031-37702-0. Available under: doi: 10.1007/978-3-031-37703-7_3 | eng |
| kops.citation.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> | |
| kops.conferencefield | Computer Aided Verification : 35th International Conference, CAV 2023, 17. Juli 2023 - 22. Juli 2023, Paris, France | deu |
| kops.date.conferenceEnd | 2023-07-22 | |
| kops.date.conferenceStart | 2023-07-17 | |
| kops.description.openAccess | openaccessbookpart | |
| kops.flag.knbibliography | false | |
| kops.identifier.nbn | urn:nbn:de:bsz:352-2-c6kjw8bzv3hr7 | |
| kops.location.conference | Paris, France | |
| kops.sourcefield | ENEA, Constantin, Hrsg., Akash LAL, Hrsg.. <i>Computer Aided Verification : 35th International Conference, CAV 2023, Proceedings, Part II</i>. 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 | deu |
| kops.sourcefield.plain | 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 | deu |
| kops.sourcefield.plain | ENEA, Constantin, ed., Akash LAL, ed.. Computer Aided Verification : 35th International Conference, CAV 2023, Proceedings, Part II. Cham: Springer, 2023, pp. 41-63. Lecture Notes in Computer Science (LNCS). 13965. ISBN 978-3-031-37702-0. Available under: doi: 10.1007/978-3-031-37703-7_3 | eng |
| kops.title.conference | Computer Aided Verification : 35th International Conference, CAV 2023 | |
| relation.isAuthorOfPublication | 0c59eb08-08c1-4e0a-9097-b41f3d89a2d0 | |
| relation.isAuthorOfPublication.latestForDiscovery | 0c59eb08-08c1-4e0a-9097-b41f3d89a2d0 | |
| source.bibliographicInfo.fromPage | 41 | |
| source.bibliographicInfo.seriesNumber | 13965 | |
| source.bibliographicInfo.toPage | 63 | |
| source.contributor.editor | Enea, Constantin | |
| source.contributor.editor | Lal, Akash | |
| source.identifier.isbn | 978-3-031-37702-0 | |
| source.publisher | Springer | |
| source.publisher.location | Cham | |
| source.relation.ispartofseries | Lecture Notes in Computer Science (LNCS) | |
| source.title | Computer Aided Verification : 35th International Conference, CAV 2023, Proceedings, Part II |
Dateien
Originalbündel
1 - 1 von 1
Vorschaubild nicht verfügbar
- Name:
- Kori_2-c6kjw8bzv3hr7.pdf
- Größe:
- 518.46 KB
- Format:
- Adobe Portable Document Format
