A common characteristic of process algebras is that they permit us the partial description of concurrent systems by including non-deterministic behaviours. These non-deterministic components are abstractions of the actual ones, and they can be detailed in successive refinements. This paper proposes an enrichment of the above abstraction. It defines a formal description technique which is able to characterize the non-determinism in a probabilistic way. The proposed technique, called LOTOS-P is an upward compatible extension of LOTOS. The compatibility includes also the possibility of specifying non-deterministic behaviours; that is, without probabilistic characterization.

However in LOTOS, nothing has been foreseen to handle the particular problem of describing timedependent systems. Although possible in theory, a precise description of such systems in LOTOS is in most cases extremely tedious and results in extremely complex and poorly readable specifications. The need to formally specify time-dependent systems is real however. Most protocols are based on time-out mechanisms that are essential for the safety of their behaviour. Several new protocol mechanisms, as well as corresponding service facilities, strengthen this need. Isochronous data transfers, rate control, multimedia synchronization are some examples.