Context-parameterized coordination model and semantics for behavioural programs

Abstract. In opposition to the traditional approaches to reactive systems in which the atomicity of actions is assumed, the behavioural paradigm deals with durative actions [9,10] in the sense that the results of a given action can interfere with other concurrently executing ones. This paradigm is, in its essence, a coordination model [6], which implies that the aspects of coordinationand computation are separated. This coordination is achieved through the use of guards, among other coordination primitives, that define not only the situations in which a given action is desired but also the ones in which its results can become obsolete. In this paper we present a coordination model for behavioural programs in which a given action can be considered obsolete not only at the time it finishes but also during its execution. This change in the semantics of the post-guard prevents the time-warp effect of obsolete actions, therefore allowing to simplify programs. We use a temporal logic where actions play a role to define an axiomatic semantics for behavioural programs. Keywords:Durative actions, interference, coordination, contexts, temporal logic. 1