Linda-based applicative and imperative process algebras

The classical algebraic approach to the specification and verification of c oncurrent systems is tuned to distributed programs that rely on asynchronou s communications and permit explicit data exchange. An applicative process algebra, obtained by embedding the Linda primitives for interprocess commun ication in a CCS/CSP-like language, and an imperative one, obtained from th e applicative Variant by adding a construct for explicit assignment of valu es to variables, are introduced. The testing framework is used to define be havioural equivalences for both languages and sound and complete proof syst ems for them are described together with a fully abstract denotational mode l (namely, a variant of Strong Acceptance Trees). (C) 2000 Elsevier Science B.V. All rights reserved.