×

On performance congruences for process algebras. (English) Zbl 0921.68031

Summary: Based on the hypothesis of durational actions and process synchronization with “busy waiting” mechanism, performance equivalence has been proposed to introduce a simple form of performance evaluation in process algebras. This equivalence enjoys many of the pleasant properties of those in the untimed setting but it is not a congruence for parallel composition with synchronization. In this paper, we give a bisimulation-based characterization of the coarsest congruence contained within performance equivalence (and discuss alternative formulations). This problem was left open in several papers. We study how the new equivalence, called performance congruence, relates with other closed equivalences in the literature and show that, unlike other proposals, it is a natural extension of those standard in the untimed setting. The weak version of performance congruence, which abstracts from internal details, is also studied. A number of examples of processes related or taken apart by performance congruence, and its weak version, are provided. A nontrivial one is also presented to illustrate the utility of the new congruences. The paper concludes with further observations concerning performance congruence and with a discussion on related and further interesting work. \(\copyright\) Academic Press.

MSC:

68Q05 Models of computation (Turing machines, etc.) (MSC2010)
68Q55 Semantics in the theory of computing
Full Text: DOI

References:

[1] Aceto, L.; Murphy, D., On the ill-timed but well-caused, Proceedings of CONCUR’93. Proceedings of CONCUR’93, Lecture Notes in Computer Science, 715 (1993), Springer-Verlag: Springer-Verlag Berlin, p. 97-111
[2] Aceto, L.; Murphy, D., Timing and causality in process algebra, Acta Informatica, 33, 317-350 (1996) · Zbl 0858.68036
[3] Boreale, M., Symbolic bisimulation for timed processes, Proceedings of AMAST’96. Proceedings of AMAST’96, Lecture Notes in Computer Science, 1101 (1996), Springer-Verlag: Springer-Verlag Berlin, p. 321-335
[4] Baeten, J.; Bergstra, J., Real time process algebra, Formal Aspects of Computing, 3, 142-188 (1991) · Zbl 0719.68020
[5] Boudol, G.; Castellani, I.; Hennessy, M.; Kiehn, A., A theory of processes with localities, Formal Aspects of Computing, 6, 165-200 (1993) · Zbl 0806.68070
[6] Cleaveland, R.; Natarajan, V., An algebraic theory of process efficiency, Proceedings of LICS’96 (1996), p. 63-72
[7] Cleaveland, R.; Natarajan, V., Predictability of real-time systems: A process-algebraic approach, Proceedings of Real-Time Systems Symposium (1996), IEEE Computer Soc. Press: IEEE Computer Soc. Press Los Alamitos
[8] Cleaveland, R.; Zwarico, A., A theory of testing for real-time, Proceedings of LICS’96 (1991), p. 110-119
[9] Corradini, F., Compositionality for processes with durational actions, Proceedings of ICTCS’95 (1995), World Scientific: World Scientific Singapore, p. 279-294
[10] Corradini, F., On performance congruences for process algebras, Technical Report (1996)
[11] Corradini, F.; Ferrari, G.; Pistore, M., Eager, busy-waiting and lazy actions in timed computation, Proceedings of Express’97. Proceedings of Express’97, Electronic Notes of Theoretical Computer Science (1997), p. 113-132 · Zbl 0911.68116
[12] Corradini, F.; Gorrieri, R.; Roccetti, M., Performance preorder: Ordering processes with respect to speed, Proceedings of MFCS’95. Proceedings of MFCS’95, Lecture Notes in Computer Science, 969 (1995), Springer-Verlag: Springer-Verlag Berlin, p. 444-453 · Zbl 1193.68173
[13] Corradini, F.; Gorrieri, R.; Roccetti, M., Performance preorder and competitive equivalence, Acta Informatica, 34, 805-835 (1997) · Zbl 0878.68081
[14] Corradini, F.; Pistore, M., Specification and verification of timed lazy systems, Proceedings of MFCS’96. Proceedings of MFCS’96, Lecture Notes in Computer Science, 1113 (1996), Springer-Verlag: Springer-Verlag Berlin, p. 279-290
[15] Corradini, F.; Pistore, M., Specification and verification of timed systems, Technical Report (1996) · Zbl 0909.68001
[16] Darondeau, Ph.; Degano, P., Causal trees, Automata, Languages and Programming. Automata, Languages and Programming, Lecture Notes in Computer Science, 372 (1989), Springer-Verlag: Springer-Verlag Berlin
[17] Degano, P.; De Nicola, R.; Montanari, M., Observational equivalences for concurrency models, Formal Description of Programming Concepts III (1987), North Holland: North Holland Berlin, p. 105-132
[18] De Nicola, R.; Hennessy, M., Testing equivalences for processes, Theoret. Comput. Sci., 34, 83-133 (1984) · Zbl 0985.68518
[19] Ferrari, G.-L.; Montanari, U., Dynamic matrices and the cost analysis of concurrent programs, Proceedings of AMAST’95. Proceedings of AMAST’95, Lecture Notes in Computer Science, 936 (1995), Springer-Verlag: Springer-Verlag Berlin, p. 307-321 · Zbl 1496.68106
[20] Gorrieri, R.; Roccetti, M., Toward performance evaluation in process algebras, Proceedings of AMAST’93. Proceedings of AMAST’93, Workshop in Computing Series (1993), Springer-Verlag: Springer-Verlag Berlin, p. 289-296
[21] Gorrieri, R.; Roccetti, M.; Stancampiano, E., A theory of processes with durational actions, Theoret. Comput. Sci., 140, 73-94 (1995) · Zbl 0874.68113
[22] van Glabbeek, R. J.; Vaandrager, F., Petri net models for algebraic theories of concurrency, Proceedings of PARLE II. Proceedings of PARLE II, Lecture Notes in Computer Science, 259 (1987), Springer-Verlag: Springer-Verlag Berlin, p. 224-242 · Zbl 0633.68054
[23] Hennessy, M., An Algebraic Theory of Processes. An Algebraic Theory of Processes, MIT Series in Computing (1988), MIT Press · Zbl 0744.68047
[24] Hennessy, M.; Lin, H., Symbolic bisimulations, Theoret. Comput. Sci., 138, 353-389 (1995) · Zbl 0874.68187
[25] Hennessy, M.; Regan, T., A temporal process algebras, Inform. and Comput., 117, 221-239 (1995) · Zbl 0826.68068
[26] Klusener, A. S., Completeness in real time process algebra, Proceedings of CONCUR’91. Proceedings of CONCUR’91, Lecture Notes in Computer Science, 527 (1991), Springer-Verlag: Springer-Verlag Berlin, p. 376-392
[27] Arun-Kumar, S.; Hennessy, M., An efficiency preorder for processes, Acta Informatica, 29, 737-760 (1992) · Zbl 0790.68039
[28] Milner, R., Communication and Concurrency. Communication and Concurrency, International Series on Computer Science (1989), Prentice-Hall · Zbl 0683.68008
[29] Milner, R.; Sangiorgi, D., Barbed bisimulations, Proceedings of ICALP’92. Proceedings of ICALP’92, Lecture Notes in Computer Science, 623 (1992), Springer-Verlag: Springer-Verlag Berlin · Zbl 1425.68298
[30] Murphy, D., Intervals and actions in a timed process algebras, Proceedings of MFPS’92 (1992)
[31] Moller, F.; Tofts, C., A temporal calculus of communicating systems, Proceedings of CONCUR’90. Proceedings of CONCUR’90, Lecture Notes in Computer Science, 459 (1990), Springer-Verlag: Springer-Verlag Berlin, p. 401-415
[32] Moller, F.; Tofts, C., Relating processes with respect to speed, Proceedings of CONCUR’91. Proceedings of CONCUR’91, Lecture Notes in Computer Science, 527 (1991), Springer-Verlag: Springer-Verlag Berlin, p. 424-438
[33] Montanari, U.; Yankelevich, D., Partial order localities, (Kuich, W., Proceedings of ICALP’92. Proceedings of ICALP’92, Lecture Notes in Computer Science, 623 (1992), Springer-Verlag: Springer-Verlag Berlin), 617-628 · Zbl 1427.68207
[34] Nielsen, M.; Thagarajan, P. S., Degrees of nondeterminism and concurrency, Proceedings of 4th Conf. on Found. of Soft. Tech. and Theoretical Computer Science. Proceedings of 4th Conf. on Found. of Soft. Tech. and Theoretical Computer Science, Lecture Notes in Computer Science, 181 (1984), Springer-Verlag: Springer-Verlag Berlin, p. 89-117 · Zbl 0595.68051
[35] Paige, R.; Tarjan, R., Three partitioning refinement algorithms, SIAM J. Comput., 16 (1987) · Zbl 0654.68072
[36] Reed, G. M.; Roscoe, A. W., Metric spaces as models for real-time concurrency, Proceedings of the Third Workshop on the Mathematical Foundations of Programming Languages Semantics. Proceedings of the Third Workshop on the Mathematical Foundations of Programming Languages Semantics, Lecture Notes in Computer Science, 298 (1987), Springer-Verlag: Springer-Verlag Berlin, p. 331-343 · Zbl 0644.68040
[37] Reed, G. M.; Roscoe, A. W., A timed model for communicating sequential processes, Theoret. Comput. Sci., 58, 249-261 (1988) · Zbl 0655.68031
[38] Vogler, W., Timed testing of concurrent systems, Inform. and Comput., 121, 149-171 (1995) · Zbl 0833.68048
[39] Wang, Y., Real time behaviour of asynchronous agents, Proceedings of CONCUR’90. Proceedings of CONCUR’90, Lecture Notes in Computer Science, 458 (1990), Springer-Verlag: Springer-Verlag Berlin, p. 502-520
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.