PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Bolognesi T., Lucidi F. Timed process algebras with urgent interactions and a unique powerful binary operator. In: Real-Time: Theory in Practice - REX Workshop. (Mook, The Netherlands, 3 - 7 June 1991). Proceedings, pp. 124 - 148. J. W. De Bakker, C. Huizing, W. P. de Roever, G. Rozenberg (eds.). (Lecture Notes in Computer Science, vol. 600). Springer-Verlag, 1992.
 
 
Abstract
(English)
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.
Subject LOTOS
Timed process algebra
timed Petri Net


Icona documento 1) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional