On hierarchical communication topologies in the -calculus

DOI10.1007/978-3-662-49498-1_7zbMATH Open1335.68166arXiv1601.01725OpenAlexW2228235215MaRDI QIDQ2802475FDOQ2802475

Authors: Emanuele D'Osualdo, C.-H. Luke Ong 

Publication date: 26 April 2016

Published in: Programming Languages and Systems (Search for Journal in Brave)

Abstract: This paper is concerned with the shape invariants satisfied by the communication topology of {pi}-terms, and the automatic inference of these invariants. A {pi}-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 {pi}-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 {pi}-calculus with decidable safety verification problems.

Full work available at URL: https://arxiv.org/abs/1601.01725

Recommendations

• Deciding Safety Properties in Infinite-State Pi-Calculus via Behavioural Types
• Termination Analysis for the $$\pi $$-Calculus by Reduction to Sequential Program Termination
• Type inference for a distributed \(\pi\)-calculus
• scientific article; zbMATH DE number 1956558
• Deciding safety properties in infinite-state pi-calculus via behavioural types

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• A theory of structural stationarity in the \(\pi\)-calculus
• Functions as processes
• Title not available (Why is that?)
• A calculus of mobile processes. I
• Well-structured transition systems everywhere!
• A theory of name boundedness
• Title not available (Why is that?)
• Title not available (Why is that?)
• On the Relationship between π-Calculus and Finite Place/Transition Petri Nets
• Behavioral equivalence in the polymorphic pi-calculus
• Title not available (Why is that?)
• Title not available (Why is that?)
• Ensuring termination by typability
• Forward analysis of depth-bounded processes
• Bounds on mobility
• Ideal abstractions for well-structured transition systems
• The Decidability of the Reachability Problem for CCS!

Cited In (4)

• Title not available (Why is that?)
• Network-conscious \(\pi\)-calculus -- a model of Pastry
• Communication errors in the \(\pi\)-calculus are undecidable
• Liveness in broadcast networks

Uses Software

• Petruchio

This page was built for publication: On hierarchical communication topologies in the \(\pi\)-calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2802475)