A Timed LOTOS Supporting a Dense Time Domain and Including New Timed Operators

A time extended version of LOTOS, denoted Timed LOTOS, is proposed for the modelling of quantitative timed behaviours. In this language neither the syntax nor the semantics are restricted to a specific time domain, i.e. a dense time domain is supported as well. Timed LOTOS incorporates a notion of urgency which is restricted to the internal actions. This is usually referred to as the maximal progress or minimum delay property. Timed LOTOS processes have also some pleasing properties such as the deadlock freeness property (i.e. processes can never stop the progression of time), and the persistency property (i.e. by idling, a process will not lose any capability of performing an action). In Timed LOTOS the delay operator is powerful because it allows the specification of a time interval in which the delay is nonderministically chosen. Two other powerful timed operators are defined which allow the expression of timed constraints on interactions, i.e. on actions involving several processes. The first one introduces a delay before the execution of any instance of a given action in a process. A second operator allows to start a time-out on any instance of a given action in a process, and to activate another process when such a time-out expires. The originality of these two operators is that they constrain interactions between processes, and support adequately a structured specification style.