The parallel composition of uniform processes with data
A general basis for the definition of a finite but unbounded number of parallel processes is the equation S(n, dt) = P(0, get(0, dt)) left-pointing open triangle eq(n, 0)right-pointing open triangle (P(n, get(n, dt)) parallel to S(n - 1, dt)). In this formula eq(n, 0) is an equality test, and get(n, dt) denotes the nth data element in table dt. We derive a linear process equation with the same behaviour as S(n, dt), and show that this equation is well-defined, provided one adopts the principle CL-RSP from Bezem. and Groote (Proceedings of Concur'94, Springer, Berlin, 1994, pp. 401-416). In order to demonstrate the strength of our result, we use it for the analysis of a standard example. We show that n + 1 concatenated buffers form a queue of capacity n + 1. (C) 2001 Elsevier Science BN. All rights reserved.
parallelism process algebra mu crl linear process expressions cones and foci method