×

zbMATH — the first resource for mathematics

Higher-level synchronising devices in Meije-SCCS. (English) Zbl 0598.68027
In an algebraic setting for parallelism and synchronisation due to R. Milner, we define a wide variety of synchronising operators on processes. We introduce them by the semantical conditional rules they obey. We prove they are higher-level nonprimitive operators from the original SCCS calculus, showing how to meet their behaviours with primitive expressions. Our purposes are: study of expressiveness - either ”semantic”, in the realm of transition systems, or ”syntaxic”, through translation of other formalisms in the calculus. Such operators allow one to specify formally sophisticated synchronisation modes dealing with (operational) products and transformations of transition systems, and still not lose their informal appealing intuition; for we then forget the realisation working with Meije-SCCS elementary synchronisation mechanisms (the mechanics below the hood). The defining rules are syntactically given, except for the allowed relations on the components’ actions monoids. This ”semantical” aspect allows us to treat many ”calculability” issues. This is especially true of closed terms, where we may claim constructive ”universality” amongst transition systems. The case of operators seems slightly more intricate. The proof of our main result has led us to a technical shaping of equivalence proofs for open expressions which shows to be interesting in its own right.

MSC:
68N25 Theory of operating systems
PDF BibTeX Cite
Full Text: DOI
References:
[1] Boudol, G., Notes on algebraic calculi of processes, () · Zbl 0578.68025
[2] Plotkin, G., A structural approach to operational semantics, () · Zbl 1082.68062
[3] Backhouse, R., Specification and proof of a regular language recogniser in SCCS, ()
[4] Bergstra, J.A.; Tiuryn, J., Process algebra semantics for queues, () · Zbl 0564.68025
[5] Austry, D.; Boudol, G., Algèbre de processus et synchronisation, Theoret. comput. sci., 30, 1, 91-131, (1984) · Zbl 0533.68026
[6] Elgot, C.C., Monadic computations and iterative algebraic theories, () · Zbl 0123.33502
[7] Hennessy, M., Proving systolic systems correct, () · Zbl 0598.68030
[8] Milner, R., Flowgraphs and flow algebras, J. ACM, 26, (1979) · Zbl 0421.68025
[9] Milner, R., Calculi for synchrony and asynchrony, Theoret. comput. sci., 25, 3, 267-310, (1983) · Zbl 0512.68026
[10] Milner, R., A complete inference system for a class of regular behaviours, J. comput. system sci., 28, (1984) · Zbl 0562.68065
[11] Parikh, R.; Parikh, R., Language generating devices, M.I.T. res. lab. electr. quart. prog. rept., J. ACM, 13, 60, 570-581, (1966), reprinted in
[12] de Simone, R., On {\scmeije} and SCCS: infinite sum operators vs. non-guarded definitions, Theoret. comput. sci., 30, 1, 133-138, (1984), (Note) · Zbl 0533.68015
[13] de Simone, R., Calculabilité et expressivité dans l’algèbre de processus parallèles {\scmeije}, ()
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.