An Interleaving Model for Real-Time Systems
Liang ChenAbstract: In this paper, we present a general interleaving model for real-time systems which is an extension of Milner's CCS with time. We make no assumption about the underlying nature of time, allowing time to be discrete (such as the integers) or dense (such as the rationals or the reals). We also make no assumption of the Maximal Progress Principle. The time variables allow us to represent the notion of time dependency and thus the language is more expressive than those without time variables. We extend bisimulations to timed processes and study the theories of strong equivalence, weak equivalence and observational congruence. Also we show that strong equivalence is decidable for finite processes, i.e. the processes without recursion. The decidability is independent of the choice of time domain.
LFCS report ECS-LFCS-91-184
This report is available in the following formats:
Previous | Index | Next