First-order logic with reachability for infinite-state systems

Kurzanzeige
dc.contributor.authorD'Osualdo, Emanuele
dc.contributor.authorMeyer, Roland
dc.contributor.authorZetzsche, Georg
dc.date.accessioned2024-10-18T07:16:22Z
dc.date.available2024-10-18T07:16:22Z
dc.date.issued2016-07-05
dc.description.abstractFirst-order logic with the reachability predicate (FO[R]) is an important means of specification in system analysis. Its decidability status is known for some individual types of infinite-state systems such as pushdown (decidable) and vector addition systems (undecidable). This work aims at a general understanding of which types of systems admit decidability. As a unifying model, we employ valence systems over graph monoids, which feature a finite-state control and are parameterized by a monoid to represent their storage mechanism. As special cases, this includes pushdown systems, various types of counter systems (such as vector addition systems) and combinations thereof. Our main result is a characterization of those graph monoids where FO[R] is decidable for the resulting transition systems.
dc.description.versionpublisheddeu
dc.identifier.doi10.1145/2933575.2934552
dc.identifier.urihttps://kops.uni-konstanz.de/handle/123456789/71002
dc.language.isoeng
dc.subjectfirst-order logic
dc.subjectreachability
dc.subjectdecidability
dc.subjectvalence automata
dc.subjectgraph monoids
dc.subjectautomatic structures
dc.subject.ddc004
dc.titleFirst-order logic with reachability for infinite-state systemseng
dc.typeINPROCEEDINGS
dspace.entity.typePublication
kops.citation.bibtex
@inproceedings{DOsualdo2016-07-05First-71002,
  year={2016},
  doi={10.1145/2933575.2934552},
  title={First-order logic with reachability for infinite-state systems},
  isbn={978-1-4503-4391-6},
  publisher={ACM},
  address={New York},
  booktitle={LICS '16 : Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science},
  pages={457--466},
  editor={Grohe, Martin},
  author={D'Osualdo, Emanuele and Meyer, Roland and Zetzsche, Georg}
}
kops.citation.iso690D'OSUALDO, Emanuele, Roland MEYER, Georg ZETZSCHE, 2016. First-order logic with reachability for infinite-state systems. LICS '16 : 31st Annual ACM/IEEE Symposium on Logic in Computer Science. New York, NY, USA, 5. Juli 2016 - 8. Juli 2016. In: GROHE, Martin, Hrsg. und andere. LICS '16 : Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. New York: ACM, 2016, S. 457-466. ISBN 978-1-4503-4391-6. Verfügbar unter: doi: 10.1145/2933575.2934552deu
kops.citation.iso690D'OSUALDO, Emanuele, Roland MEYER, Georg ZETZSCHE, 2016. First-order logic with reachability for infinite-state systems. LICS '16 : 31st Annual ACM/IEEE Symposium on Logic in Computer Science. New York, NY, USA, Jul 5, 2016 - Jul 8, 2016. In: GROHE, Martin, ed. and others. LICS '16 : Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. New York: ACM, 2016, pp. 457-466. ISBN 978-1-4503-4391-6. Available under: doi: 10.1145/2933575.2934552eng
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/71002">
    <dcterms:issued>2016-07-05</dcterms:issued>
    <dc:creator>Meyer, Roland</dc:creator>
    <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/71002"/>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dc:contributor>D'Osualdo, Emanuele</dc:contributor>
    <dcterms:title>First-order logic with reachability for infinite-state systems</dcterms:title>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:contributor>Meyer, Roland</dc:contributor>
    <dcterms:abstract>First-order logic with the reachability predicate (FO[R]) is an important means of specification in system analysis. Its decidability status is known for some individual types of infinite-state systems such as pushdown (decidable) and vector addition systems (undecidable).

This work aims at a general understanding of which types of systems admit decidability. As a unifying model, we employ valence systems over graph monoids, which feature a finite-state control and are parameterized by a monoid to represent their storage mechanism. As special cases, this includes pushdown systems, various types of counter systems (such as vector addition systems) and combinations thereof. Our main result is a characterization of those graph monoids where FO[R] is decidable for the resulting transition systems.</dcterms:abstract>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2024-10-18T07:16:22Z</dcterms:available>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2024-10-18T07:16:22Z</dc:date>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dc:creator>Zetzsche, Georg</dc:creator>
    <dc:contributor>Zetzsche, Georg</dc:contributor>
    <dc:creator>D'Osualdo, Emanuele</dc:creator>
    <dc:language>eng</dc:language>
  </rdf:Description>
</rdf:RDF>
kops.conferencefieldLICS '16 : 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 5. Juli 2016 - 8. Juli 2016, New York, NY, USAdeu
kops.date.conferenceEnd2016-07-08
kops.date.conferenceStart2016-07-05
kops.flag.knbibliographyfalse
kops.location.conferenceNew York, NY, USA
kops.sourcefieldGROHE, Martin, Hrsg. und andere. <i>LICS '16 : Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science</i>. New York: ACM, 2016, S. 457-466. ISBN 978-1-4503-4391-6. Verfügbar unter: doi: 10.1145/2933575.2934552deu
kops.sourcefield.plainGROHE, Martin, Hrsg. und andere. LICS '16 : Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. New York: ACM, 2016, S. 457-466. ISBN 978-1-4503-4391-6. Verfügbar unter: doi: 10.1145/2933575.2934552deu
kops.sourcefield.plainGROHE, Martin, ed. and others. LICS '16 : Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. New York: ACM, 2016, pp. 457-466. ISBN 978-1-4503-4391-6. Available under: doi: 10.1145/2933575.2934552eng
kops.title.conferenceLICS '16 : 31st Annual ACM/IEEE Symposium on Logic in Computer Science
relation.isAuthorOfPublicationa922a71d-ac65-4324-bb6c-dee45cfd627e
relation.isAuthorOfPublication.latestForDiscoverya922a71d-ac65-4324-bb6c-dee45cfd627e
source.bibliographicInfo.fromPage457
source.bibliographicInfo.toPage466
source.contributor.editorGrohe, Martin
source.flag.etalEditortrue
source.identifier.isbn978-1-4503-4391-6
source.publisherACM
source.publisher.locationNew York
source.titleLICS '16 : Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science

Dateien

Sammlungen

Informatik und Informationswissenschaft: Publikationen