Publikation:

First-order logic with reachability for infinite-state systems

Vorschaubild

Dateien

Zu diesem Dokument gibt es keine Dateien.

Datum

2016

Autor:innen

Meyer, Roland
Zetzsche, Georg

Herausgeber:innen

Kontakt

ISSN der Zeitschrift

Electronic ISSN

ISBN

Bibliografische Daten

Verlag

Schriftenreihe

Auflagebezeichnung

URI (zitierfähiger Link)
DOI (zitierfähiger Link)
https://doi.org/10.1145/2933575.2934552
ArXiv-ID

Internationale Patentnummer

Angaben zur Forschungsförderung

Projekt

Open Access-Veröffentlichung

Sammlungen

Informatik und Informationswissenschaft: Publikationen
Core Facility der Universität Konstanz

Gesperrt bis

Titel in einer weiteren Sprache

Publikationstyp
Beitrag zu einem Konferenzband
Publikationsstatus
Published

Erschienen 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.2934552

Zusammenfassung

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.

Zusammenfassung in einer weiteren Sprache

Fachgebiet (DDC)
004 Informatik

Schlagwörter

first-order logic, reachability, decidability, valence automata, graph monoids, automatic structures

Konferenz

LICS '16 : 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 5. Juli 2016 - 8. Juli 2016, New York, NY, USA
Rezension
undefined / . - undefined, undefined

Forschungsvorhaben

Organisationseinheiten

Zeitschriftenheft

Zugehörige Datensätze in KOPS

Zitieren

ISO 690D'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.2934552
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}
}
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>

Interner Vermerk

xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter

Kontakt
URL der Originalveröffentl.

Prüfdatum der URL

Prüfungsdatum der Dissertation

Finanzierungsart

Kommentar zur Publikation

Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Nein
Begutachtet
Diese Publikation teilen