Semantics of Behavioural Programs
PhD Thesis, March 1998

The behavioural paradigm was proposed by professor W.M.Turski as an alternative to the traditional computing paradigm. Behavioural programs are reactive programs in which the actions are durative, that is, the state in which the system is in at the time an action finishes execution is not necessarily the same in which it was launched.
The behavioural paradigm is formalised here as a coordination model between actions that modify a shared environment, that are durative and that are likely to be heterogeneous as regards the programming language in which they are given. This heterogeneity is possible due to the definition of contexts, which constitute the interfaces of the actions. Coordination is achieved through pre- and post-guards that establish criteria of activation/permission for the execution and productivity of actions.
We present here a semantics for programs in the behavioural paradigm in its three usual aspects: operational, denotational and axiomatic.
The rules of the operational semantics define a durative transition system (std). This concept is introduced in this work with the aim of generalising classical transition systems, in order to make it possible to represent durative actions.
We define a durative transition logic (LTD) the formulas of which are evaluated with respect to std-based models. The axiomatic semantics is expressed in LTD. This logic, which is sound and complete, allows us to express in a same formula the three states that characterise a durative action: the launching, accepting and resulting states.
Several equivalence relations between behavioural programs are presented that are based on bisimulation relations between stds. These relations correspond to different points of view concerning what is considered relevant in the execution of a program.
Behavioural properties of programs as, for example, stability, reachability, deadlock freedom, are defined in an operational way through restrictions to the std that is defined by the program and also in an axiomatic way, through LTD formulas.