Abstract A functional formalism for describing and reasoning about the time dependent behaviour of reactive systems is presented. The model is event based and can describe the histories of events with finite duration. It is a generalisation of the model of Caspi and Halbwachs (1986). A set of tools with their operations are introduced in the formalism and structure theorems characterising the algebra of events are proved. The power of this extended model is illustrated through the formal specification and correctness proof for a problem chosen from robotics.

Given k ≥ 2 circular disks D1, D2...Dkin a 2-dimensional region bounded by a finite set of polygonal obstacles, an algorithm to determine the existence of a collision free coordinated motion of the disks is given. The time complexity is shown to be O(nk} where n is the number of edges composing the walls. This algorithm is believed to be optimal.