Timed Process Algebras with Urgent Interactions and a Unique Powerful Binary Operator

A timed process algebra called ρ1 is introduced, which offers operators for specifying time-dependent behaviours and, in particular, the urgency of a given (inter-)action involving one or more processes. The formal semantics of the language is given in a style similar to the one adopted by Tofts and Moller for TCCS: two independent sets of inference rules are provided, which handle, respectively, the occurrence of actions and the passing of time. The language, partly inspired to LOTOS, can specify in a natural way the “wait-until-timeout” scenario, and we prove that, due to its two time-related operators, it can simulate Turing machines. The formalism appears as a most natural transposition in the realm of process algebras of an expressivity-preserving subset of the well known Time Petri Nets of Merlin and Farber. An enhanced timed process algebra called ρ2, which includes only five operators, and preserves the expressivity of ρ1, is then proposed: it combines mutual disabling, choice, parallel composition with synchronization, and pure interleaving, into a unique, general-purpose, parametric binary operator.