University of Leicester

computer science

Process languages with discrete relative time based on Ordered SOS format and rooted eager bisimulation,
Irek Ulidowski and Shoji Yuen, ,
Journal fo Logic and Algebraic Programming, 60-61, pp 401-460, 2004.


We propose a uniform framework, based on the Ordered Structural Operational Semantics (OSOS) approach of Ulidowski and Phillips \cite{UliPhi02}, for extending arbitrary process languages with discrete time. The generality of our framework allows the user to select the most suitable timed process language for a task in hand. This is possible because the user can choose any operators, whether they are standard operators or new application-specific operators, provided that they satisfy two conditions. Firstly, the operators must preserve a timed version of eager bisimulation and, secondly, all processes in the considered process language must satisfy the time determinacy property. Both of these conditions are verified easily by examining the structure of the OSOS rules defining the operators. We also propose several constraints on the type of OSOS definitions for the operators so that several properties, which reflect the nature of time passage, for example the maximal progress and time persistence properties, are satisfied.

This paper s available in the ps form.

| [University Home]|[Faculty of Science]|[MCS Home]|[CS Home]||[University Index A-Z]|[University Search]|[University Help]|

Author: Irek Ulidowski (
© University of Leicester. Last modified: 5th November 2005, 09:49:31
CS Web Maintainer.