×

zbMATH — the first resource for mathematics

Responsiveness in process calculi. (English) Zbl 1157.68050
Summary: A system guarantees responsive usage of a channel \(r\) if a communication along \(r\) is guaranteed to eventually take place. Responsiveness is important, for instance, to ensure that any request to a service be eventually replied. We propose two distinct type systems, each of which statically guarantees responsive usage of names in well-typed pi-calculus processes. In the first system, we achieve responsiveness by combining techniques for deadlock and livelock avoidance with linearity and receptiveness. The latter is a guarantee that a name is ready to receive as soon as it is created. These conditions imply relevant limitations on the nesting of actions and on multiple use of names in processes. In the second system, we relax these requirements so as to permit certain forms of nested inputs and multiple outputs. We demonstrate the expressive power of the two systems by showing that primitive recursive functions-in the case of the first system-and Cook and Misra’s service orchestration language orc-in the case of the second system-can be encoded into well-typed processes.

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Software:
TyPiCal
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Acciai, L.; Boreale, M., Responsiveness in process calculi, (), 136-150 · Zbl 1157.68050
[2] Berger, M.; Honda, K.; Yoshida, N., Sequentiality and the \(\pi\)-calculus, (), 29-45 · Zbl 0981.68037
[3] Boreale, M., On the expressiveness of internal mobility in name-passing calculi, Theoretical computer science, 195, 2, 205-226, (1998) · Zbl 0915.68059
[4] Cook, W.R.; Misra, J., Computation orchestration: A basis for wide-area computing, Software and systems modeling, 6, 1, 83-110, (2007)
[5] Y. Deng, D. Sangiorgi, Ensuring termination by typability, in: Proc. of IFIP TCS, 2004, pp. 619-632; Full version in Information and Computation 204 (7) (2006) 1045-1082 · Zbl 1088.68661
[6] Kobayashi, N., A type system for lock-free processes, Information and computation, 177, 2, 122-159, (2002) · Zbl 1093.68065
[7] Kobayashi, N., Type-based information flow analysis for the pi-calculus, Acta informartica, 42, 4-5, 291-347, (2005) · Zbl 1081.68061
[8] Kobayashi, N., A new type system for deadlock-free processes, (), 233-247 · Zbl 1151.68537
[9] N. Kobayashi, The tool. Available at: http://www.kb.ecei.tohoku.ac.jp/ koba/typical/
[10] N. Kobayashi, B.C. Pierce, D.N. Turner, Linearity and the Pi-calculus, in: Proc. of POPL, 1996; Full version in ACM Transactions on Programming Languages and Systems 21 (5) (1999) 914-947
[11] Merro, M.; Sangiorgi, D., On asynchrony in name-passing calculi, (), Mathematical structures in computer science, 14, 5, 715-767, (2004), Full version in · Zbl 1093.68026
[12] R. Milner, The polyadic \(\pi\)-calculus: A tutorial. Tec. Rep. LFCS Report ECS-LFCS-91-180, 1991; Also in Logic and Algebra of Specification, Springer-Verlag, 1993, pp. 203-246
[13] D. Sangiorgi, The name discipline of uniform receptiveness, in: Proc. of ICALP, 1997; TCS 221 (1-2) (1999) 457-493 · Zbl 0930.68035
[14] Sangiorgi, D.; Walker, D., The \(\pi\)-calculus: A theory of mobile processes, (2001), Cambridge University Press · Zbl 0981.68116
[15] Yoshida, N., Graph types for monadic mobile processes, (), 371-386
[16] N. Yoshida, Type-based liveness in the presence of nontermination and nondeterminism, MCS Technical Report, 2002-20, University of Leicester, 2002
[17] Yoshida, N.; Berger, M.; Honda, K., Strong normalisation in the \(\pi\)-calculus, (), Information and computation, 191, 2, 145-202, (2004), Also in · Zbl 1101.68705
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.