Conferences in Research and Practice in Information Technology
  

Online Version - Last Updated - 20 Jan 2012

 

 
Home
 

 
Procedures and Resources for Authors

 
Information and Resources for Volume Editors
 

 
Orders and Subscriptions
 

 
Published Articles

 
Upcoming Volumes
 

 
Contact Us
 

 
Useful External Links
 

 
CRPIT Site Search
 
    

Linear Uniform Receptiveness in a Pi-Calculus with Location Failures

Finderup, P., Huettel, H., Knudsen, J. S. and Nielsen, J. G.

    The notion of receptiveness arises in the π-calculus as a guarantee of determinacy in the behaviour of callable entities and was first investigated by Sangiorgi. The DπF process calculus, introduced by Francalanza and Hennessy, extends the π-calculus with located processes and location and link failures. In this paper we extend the notion of receptiveness to DπF and give sound characterizations of the property of linear uniform receptiveness in DπF in the form of two type systems. Our first type system ensures receptiveness, the property that no pending output will ever be left unattended. We achieve this by ensuring linearity and by ensuring that the input and output remain at the same location, such that location failure will effectively remove either both or none. Our second type system allows for migration but ensures that input capabilities remain within locations which are hidden from the context and thus not subject to failures.
Cite as: Finderup, P., Huettel, H., Knudsen, J. S. and Nielsen, J. G. (2010). Linear Uniform Receptiveness in a Pi-Calculus with Location Failures. In Proc. Sixteenth Computing: The Australasian Theory Symposium (CATS 2010) Brisbane, Australia. CRPIT, 109. Viglas, T. and Potanin, A. Eds., ACS. 79-88
pdf (from crpit.com) pdf (local if available) BibTeX EndNote GS