zbMATH — the first resource for mathematics

About fair asynchrony. (English) Zbl 0607.68016
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.

68N25 Theory of operating systems
68Q65 Abstract data types; algebraic specification
Full Text: DOI
[1] Ben-Ari, M.; Manna, Z.; Pnueli, A., The temporal logic of branching time, (), 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, (), 127-138
[5] Darondeau, Ph., An enlarged definition and complete axiomatization of observational congruence of finite processes, (), 47-62 · Zbl 0482.68025
[6] Darondeau, Ph.; Kott, L., On the observational semantics of fair parallelism, (), 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., ()
[11] Guessarian, I., Algebraic semantics, () · Zbl 0602.68017
[12] Gabbay, D.; Pnueli, A.; Shelah, S.; Stavi, J., On the temporal analysis of fairness, (), 163-173
[13] Hennessy, M.C.B.; Milner, R., On observing nondeterminism and concurrency, (), 299-309
[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, ()
[16] Hennessy, M.C.B., An algebraic theory of fair asynchronous communicating processes, () · Zbl 0437.68002
[17] Jorrand, Ph., Specification of communicating processes and process implementation correctness, (), 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, () · 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, (), 504-526
[23] Parrow, J.; Gustavsson, R., Modelling distributed systems in an extension of C.C.S. with infinite experiments and temporal logics, ()
[24] Plotkin, G., A structural approach to operational semantics, () · Zbl 1082.68062
[25] Stoy, J.E., Denotational semantics, (1977), M.I.T. Press Cambridge, MA · Zbl 0468.68013
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.