×

CCS with priority guards. (English) Zbl 1134.68042

Summary: It has long been recognised that standard process algebra has difficulty dealing with actions of different priority, such as for instance an interrupt action of high priority. Various solutions have been proposed. We introduce a new approach, involving the addition of “priority guards” to Milner’s process calculus CCS. In our approach, priority is unstratified, meaning that actions are not assigned fixed levels, so that the same action can have different priority depending where it appears in a program. Unlike in other unstratified accounts of priority in CCS (such as that of Camilleri and Winskel), we treat inputs and outputs symmetrically. We introduce the new calculus, give examples, develop its theory (including bisimulation and equational laws), and compare it with existing approaches. We use leader election problems to show that priority adds expressiveness to both CCS and the \(\pi \)-calculus.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Full Text: DOI

References:

[1] Baeten, J. C.M.; Bergstra, J.; Klop, J. W., Syntax and defining equations for an interrupt mechanism in process algebra, Fundam. Inform., 9, 127-168 (1986) · Zbl 0617.68027
[2] Bergstra, J.; Klop, J. W., Process algebra for synchronous communication, Inform. and Control, 60, 1-3, 109-137 (1984) · Zbl 0597.68027
[3] A. Bloch, M.V. Frederiksen, B. Haagensen, A Π;-calculus with prioritized actions with applications, DAT5 Project Report, Group B1-215B, supervisor H. Hüttel, Department of Computer Science, Aalborg University, 2004.; A. Bloch, M.V. Frederiksen, B. Haagensen, A Π;-calculus with prioritized actions with applications, DAT5 Project Report, Group B1-215B, supervisor H. Hüttel, Department of Computer Science, Aalborg University, 2004.
[4] Bougé, L., On the existence of symmetric algorithms to find leaders in networks of communicating sequential processes, Acta Inform., 25, 179-201 (1988) · Zbl 0621.68011
[5] Camilleri, J.; Winskel, G., CCS with priority choice, Inform. and Comput., 116, 1, 26-37 (1995) · Zbl 0818.68107
[6] Cardelli, L.; Gordon, A. D., Mobile ambients, Theoret. Comput. Sci., 240, 1, 177-213 (2000) · Zbl 0954.68108
[7] Cleaveland, R.; Hennessy, M. C.B., Priorities in process algebra, Inform. and Comput., 87, 1/2, 58-77 (1990) · Zbl 0726.68053
[8] Cleaveland, R.; Lüttgen, G.; Natarajan, V., Priority in process algebra, (Bergstra, J. A.; Ponse, A.; Smolka, S. A., Handbook of Process Algebra (2001), Elsevier), 391-424, (Chapter 12) · Zbl 1062.68079
[9] Ene, C.; Muntean, T., Expressiveness of point-to-point versus broadcast communications, (FCT ’99. FCT ’99, Lecture Notes in Computer Science, vol. 1684 (1999), Springer-Verlag), 258-268 · Zbl 0946.68096
[10] Fidge, C. J., A formal definition of priority in CSP, ACM Trans. Programming Languages Syst., 15, 4, 681-705 (1993)
[11] Hansson, H.; Orava, F., A process calculus with incomparable priorities, (Proceedings of the North American Process Algebra Workshop, Stony Brook, New York, Workshops in Computing (1992), Springer-Verlag), 43-64
[12] Hoare, C. A.R., Communicating sequential processes, Commun. Assoc. Comput. Mach., 21, 8, 666-677 (1978) · Zbl 0383.68028
[13] Hoare, C. A.R., Communicating Sequential Processes (1985), Prentice-Hall · Zbl 0637.68007
[14] A. Jeffrey, A typed, prioritized process algebra, Technical Report 13/93, Department of Computer Science, University of Sussex, 1993.; A. Jeffrey, A typed, prioritized process algebra, Technical Report 13/93, Department of Computer Science, University of Sussex, 1993.
[15] C.-T. Jensen, Prioritized and Independent Actions in Distributed Computer Systems, Ph.D. Thesis, Aarhus University, 1994.; C.-T. Jensen, Prioritized and Independent Actions in Distributed Computer Systems, Ph.D. Thesis, Aarhus University, 1994.
[16] Milner, R., A complete inference system for a class of regular behaviours, J. Comput. Syst. Sci., 28, 439-466 (1984) · Zbl 0562.68065
[17] Milner, R., Communication and Concurrency (1989), Prentice-Hall · Zbl 0683.68008
[18] Milner, R., A complete axiomatisation for observational congruence of finite-state behaviours, Inform. and Comput., 81, 227-247 (1989) · Zbl 0688.68050
[19] Milner, R., Communicating and Mobile Systems: the \(π\)-calculus (1999), Cambridge University Press · Zbl 0942.68002
[20] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, Inform. and Comput., 100, 1-77 (1992) · Zbl 0752.68037
[21] Natarajan, V.; Christoff, L.; Christoff, I.; Cleaveland, R., Priorities and abstraction in process algebra, (Thiagarajan, P. S., Foundations of Software Technology and Theoretical Computer Science, 14th Conference. Foundations of Software Technology and Theoretical Computer Science, 14th Conference, Lecture Notes in Computer Science, vol. 880 (1994), Springer-Verlag), 217-230 · Zbl 1044.68688
[22] Nestmann, U.; Pierce, B., Decoding choice encodings, Inform. and Comput., 163, 1, 1-59 (2000) · Zbl 1003.68080
[23] Palamidessi, C., Comparing the expressive power of the synchronous and the asynchronous \(π\)-calculi, Math. Structures Comput. Sci., 13, 5, 685-719 (2003)
[24] Phillips, I. C.C., CCS with priority guards, (Proceedings of 12th International Conference on Concurrency Theory, CONCUR 2001. Proceedings of 12th International Conference on Concurrency Theory, CONCUR 2001, Lecture Notes in Computer Science, vol. 2154 (2001), Springer-Verlag), 305-320 · Zbl 1006.68082
[25] Phillips, I. C.C.; Vigliotti, M. G., Electoral systems in ambient calculi, (Proceedings of 7th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2004. Proceedings of 7th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2004, Lecture Notes in Computer Science, vol. 2987 (2004), Springer-Verlag), 408-422 · Zbl 1126.68508
[26] Phillips, I. C.C.; Vigliotti, M. G., Leader election in rings of ambient processes, Theoret. Comput. Sci., 356, 3, 468-494 (2006) · Zbl 1092.68068
[27] Prasad, K. V.S., A calculus of broadcasting systems, Sci. Comput. Programming, 25, 2-3, 285-327 (1995)
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.