computer science

Abstract

In recent years a large number of process languages with time have been developed as more realistic formalisms for description and reasoning about concurrent systems. We propose a uniform framework, based on the ordered structural operational semantics (SOS) approach, 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 or new application-specific operators, provided that they preserve a version of weak bisimulation and all processes in the considered language satisfy the time determinacy property. We also propose several constraints on ordered SOS rules for the operators such that some other properties, which reflect the nature of time passage, for example the maximal progress and weak timelock freeness properties, are satisfied.

Author: Irek Ulidowski (I.Ulidowski@mcs.le.ac.uk).
© University of Leicester. Last modified: 13th January 2004, 16:31:50
CS Web Maintainer.