About fair asynchrony. (English) Zbl 0607.68016

Darondeau, Philippe

Theor. Comput. Sci. 37, 305-336 (1985).

This paper examines the joint influence of fairness and asynchrony on the semantic modelling of a CCS-like language. Fairness is the guarantee for every agent engaged in a computation to communicate with the other asynchronous agents if such communications are infinitely often possible. Programs are compared according to an implementation preorder which reflects the inclusion of observable properties: whenever, for every context \({\mathcal C}\) and for every program r, no computation of r experimenting upon \({\mathcal C}(p)\) allows to recognize p versus q, p is considered less than q. A fully abstract model of the preorder is constructed in a domain of infinitary languages, preferred here to classical algebraic domains. The restriction to bounded parallelism is analysed. In that simplified framework, the model turns effective and, moreover, decidable.

MSC:

68N25	Theory of operating systems
68Q65	Abstract data types; algebraic specification

Keywords:

fairness; asynchrony; semantic modelling of a CCS-like language; asynchronous agents; communications; infinitary languages; classical algebraic domains; parallelism

References:

[1]	Ben-Ari, M.; Manna, Z.; Pnueli, A., The temporal logic of branching time, (8th Ann. ACM Symp. on Principles of Programming Languages (1981)), 164-176
[2]	Brookes, S. D.; Hoare, C. A.R.; Roscoe, A. W., A theory of communicating sequential processes, J. Assoc. Comput. Mach., 31, 560-599 (1984) · Zbl 0628.68025
[3]	Costa, G.; Stirling, C., A fair calculus of communicating systems, Acta Inform., 21, 417-441 (1984) · Zbl 0538.68014
[4]	Darondeau, Ph., Quelques problémes relatifs à la composition paralléle, (Actes du Congrés de l’AFCET 1981 (1981), Hommes et Techniques: Hommes et Techniques Paris), 127-138
[5]	Darondeau, Ph., An enlarged definition and complete axiomatization of observational congruence of finite processes, (Dezani-Ciancaglini, M.; Montanari, U., 5th Internat. Symp. on Programming. 5th Internat. Symp. on Programming, Lecture Notes in Computer Science, 137 (1982), Springer: Springer Berlin/Heidelberg/New York), 47-62 · Zbl 0482.68025
[6]	Darondeau, Ph.; Kott, L., On the observational semantics of fair parallelism, (Diàz, J., 10th Internat. Coll. on Automata, Language and Programming, ’83. 10th Internat. Coll. on Automata, Language and Programming, ’83, Lecture Notes in Computer Science, 154 (1983), Springer: Springer Berlin/Heidelberg/New York), 147-159 · Zbl 0518.68014
[7]	Darondeau, Ph.; Kott, L., On the observational semantics of fair parallelism, INRIA Rept. No. 262 (1983) · Zbl 0518.68014
[8]	Darondeau, Ph.; Kott, L., A formal proof system for infinitary rational expressions, INRIA Rept. No. 218 (1983) · Zbl 0575.68083
[9]	Darondeau, Ph.; Kott, L., Towards a formal proof system for \(w = rational\) expressions, Inform. Process. Lett., 19, 173-177 (1984) · Zbl 0575.68082
[10]	Eilenberg, S., (Automata, Languages and Machines, Vol. A (1974), Academic Press: Academic Press New York) · Zbl 0317.94045
[11]	Guessarian, I., Algebraic Semantics, (Lecture Notes in Computer Science, 99 (1981), Springer: Springer Berlin/Heidelberg/New York) · Zbl 0602.68017
[12]	Gabbay, D.; Pnueli, A.; Shelah, S.; Stavi, J., On the temporal analysis of fairness, (7th Ann. ACM Symposium on Principles of Programming Languages (1980)), 163-173
[13]	Hennessy, M. C.B.; Milner, R., On observing nondeterminism and concurrency, (De Bakker, J.; Van Leeuwen, J., Internat. Coll. on Automata, Languages and Programming ’80. Internat. Coll. on Automata, Languages and Programming ’80, Lecture Notes in Computer Science, 85 (1980), Springer: Springer Berlin/Heidelberg/New York), 299-309 · Zbl 0441.68018
[14]	Hennesy, M. C.B., Synchronous and asynchronous experiments on processes, Inform. and Control, 59, 36-83 (1983) · Zbl 0544.68028
[15]	Hennessy, M. C.B., Modelling finite delay operators, (Internal Rept. CSR 153-83 (1983), Univ. of Edinburgh, Dept. of Computer Science)
[16]	Hennessy, M. C.B., An algebraic theory of fair asynchronous communicating processes, (Rept. (1984), Univ. of Edinburgh, Dept. of Computer Science) · Zbl 0437.68002
[17]	Jorrand, Ph., Specification of communicating processes and process implementation correctness, (Dezani-Ciancaglini, M.; Montanari, U., 5th Internat. Symp. on Programming. 5th Internat. Symp. on Programming, Lecture Notes in Computer Science, 137 (1982), Springer: Springer Berlin/Heidelberg/New York), 242-256
[18]	Milner, R., Fully abstract models of typed lambda-calculi, Theoret. Comput. Sci., 4, 1-23 (1977) · Zbl 0386.03006
[19]	Milner, R., Flowgraphs and flow algebras, J. Assoc. Comput. Mach., 26, 794-818 (1979) · Zbl 0421.68025
[20]	Milner, R., A Calculus of Communicating Systems, (Lecture Notes in Computer Science, 92 (1980), Springer: Springer Berlin/Heidelberg/New York) · Zbl 0452.68027
[21]	Milner, R., Calculi for synchrony and asynchrony, Theoret. Comput. Sci., 25, 267-310 (1983) · Zbl 0512.68026
[22]	Park, D., On the semantics of fair parallelism, (Björner, D., Abstract Software Specifications. Abstract Software Specifications, Lecture Notes in Computer Science, 86 (1980), Springer: Springer Berlin/Heidelberg/New York), 504-526
[23]	Parrow, J.; Gustavsson, R., Modelling distributed systems in an extension of C.C.S. with infinite experiments and temporal logics, (IFIP 4th Internat. Workshop on Protocol Specification, Testing and Verification (1984))
[24]	Plotkin, G., A structural approach to operational semantics, (Rept. DAIMI-FN 19 (1981), Univ. of Aarhus, Computer Science Dept) · Zbl 1082.68062
[25]	Stoy, J. E., Denotational Semantics (1977), M.I.T. Press: M.I.T. Press Cambridge, MA · Zbl 0468.68013