On Hierarchical Communication Topologies in the π-calculus

D'Osualdo, Emanuele; Ong, C.-H. Luke

On Hierarchical Communication Topologies in the π-calculus

Dateien

Zu diesem Dokument gibt es keine Dateien.

Datum

2016

Autor:innen

D'Osualdo, Emanuele

Ong, C.-H. Luke

DOI (zitierfähiger Link)

https://doi.org/10.1007/978-3-662-49498-1_7

Sammlungen

Informatik und Informationswissenschaft

Publikationstyp

Beitrag zu einem Konferenzband

Publikationsstatus

Published

Erschienen in

THIEMANN, Peter, Hrsg.. Programming Languages and Systems : 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Proceedings. Berlin: Springer, 2016, S. 149-175. Lecture Notes in Computer Science (LNCS). 9632. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-662-49497-4. Verfügbar unter: doi: 10.1007/978-3-662-49498-1_7

Zusammenfassung

This paper is concerned with the shape invariants satisfied by the communication topology of π-terms, and the automatic inference of these invariants. A π-term P is hierarchical if there is a finite forest T such that the communication topology of every term reachable from P satisfies a T -shaped invariant. We design a static analysis to prove a term hierarchical by means of a novel type system that enjoys decidable inference. The soundness proof of the type system employs a non-standard view of π-calculus reactions. The coverability problem for hierarchical terms is decidable. This is proved by showing that every hierarchical term is depth-bounded, an undecidable property known in the literature. We thus obtain an expressive static fragment of the π-calculus with decidable safety verification problems.

Fachgebiet (DDC)

004 Informatik

Schlagwörter

Normal Form, Type System, Base Type, Typing Rule, Type Inference

Konferenz

25th European Symposium on Programming, ESOP 2016, 3. Apr. 2016 - 7. Apr. 2016, Eindhoven, The Netherlands

Zitieren

ISO 690

D'OSUALDO, Emanuele, C.-H. Luke ONG, 2016. On Hierarchical Communication Topologies in the π-calculus. 25th European Symposium on Programming, ESOP 2016. Eindhoven, The Netherlands, 3. Apr. 2016 - 7. Apr. 2016. In: THIEMANN, Peter, Hrsg.. Programming Languages and Systems : 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Proceedings. Berlin: Springer, 2016, S. 149-175. Lecture Notes in Computer Science (LNCS). 9632. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-662-49497-4. Verfügbar unter: doi: 10.1007/978-3-662-49498-1_7

BibTex

@inproceedings{DOsualdo2016Hiera-71004,
  year={2016},
  doi={10.1007/978-3-662-49498-1_7},
  title={On Hierarchical Communication Topologies in the π-calculus},
  number={9632},
  isbn={978-3-662-49497-4},
  issn={0302-9743},
  publisher={Springer},
  address={Berlin},
  series={Lecture Notes in Computer Science (LNCS)},
  booktitle={Programming Languages and Systems : 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Proceedings},
  pages={149--175},
  editor={Thiemann, Peter},
  author={D'Osualdo, Emanuele and Ong, C.-H. Luke}
}

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/71004">
    <dcterms:issued>2016</dcterms:issued>
    <dc:language>eng</dc:language>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2024-10-18T07:21:44Z</dcterms:available>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dcterms:title>On Hierarchical Communication Topologies in the π-calculus</dcterms:title>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2024-10-18T07:21:44Z</dc:date>
    <dcterms:abstract>This paper is concerned with the shape invariants satisfied by the communication topology of π-terms, and the automatic inference of these invariants. A π-term P is hierarchical if there is a finite forest T such that the communication topology of every term reachable from P satisfies a T -shaped invariant. We design a static analysis to prove a term hierarchical by means of a novel type system that enjoys decidable inference. The soundness proof of the type system employs a non-standard view of π-calculus reactions. The coverability problem for hierarchical terms is decidable. This is proved by showing that every hierarchical term is depth-bounded, an undecidable property known in the literature. We thus obtain an expressive static fragment of the π-calculus with decidable safety verification problems.</dcterms:abstract>
    <dc:creator>Ong, C.-H. Luke</dc:creator>
    <dc:contributor>Ong, C.-H. Luke</dc:contributor>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/71004"/>
    <dc:creator>D'Osualdo, Emanuele</dc:creator>
    <dc:contributor>D'Osualdo, Emanuele</dc:contributor>
  </rdf:Description>
</rdf:RDF>

Universitätsbibliographie

Nein