• People
• Events
• Research

Decidability and Completeness in Real-Time Processes

Abstract: By extending Milner's CCS with time, a general interleaving model for real-time systems is proposed. We make no assumption about the underlying nature of time and allow time to be discrete (such as the integers) or dense (such as the rationals or the reals). Time variables allow us to represent the notion of time dependency and in general the language is more expressive than those without time variables. We extend the notion of bisimulation to timed processes and show that strong equivalence is still decidable. Decidability is independent of the choice of time domain. Also we present a proof system in which there are no infinite proof rules. Again the proof system is independent of the choice of time domain. We show that the proof system is complete over dense time domains, but only complete for some subclass of processes over discrete time domains.

LFCS report ECS-LFCS-91-185

This report is available in the following formats:

• PostScript file
• Gzipped PostScript file
• LaTeX DVI file
• Gzipped LaTeX DVI file