On Hierarchical Communication Topologies in the pi-calculus.
File(s)1601.01725v2.pdf (801.26 KB)
Supporting information
Author(s)
D'Osualdo, E
Ong, C-HL
Type
Conference Paper
Abstract
This paper is concerned with the shape invariants satisfied by the communication topology of π-terms, and the automatic inference of these invariants. A π-termP 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.
Date Issued
2016-12-31
Date Acceptance
2015-12-09
Citation
Lecture Notes in Computer Science, 2016, 9632, pp.149-175
ISBN
978-3-662-49498-1
ISSN
0302-9743
Publisher
Springer Verlag
Start Page
149
End Page
175
Journal / Book Title
Lecture Notes in Computer Science
Volume
9632
Copyright Statement
The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-662-49498-1_7
Identifier
https://doi.org/10.1007/978-3-662-49498-1_7
Source
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, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings
Subjects
cs.PL
cs.LO
08 Information And Computing Sciences
Artificial Intelligence & Image Processing
Publication Status
Published