Information Services banner Edinburgh Research Archive The University of Edinburgh crest

Edinburgh Research Archive >
Informatics, School of >
Informatics thesis and dissertation collection >

Please use this identifier to cite or link to this item:

This item has been viewed 14 times in the last year. View Statistics

Files in This Item:

File Description SizeFormat
ECS-LFCS-93-271.dvi420.2 kBTeX dviView/Open
ECS-LFCS-93-271.PDF5.93 MBAdobe PDFView/Open
ECS-LFCS-93-271.ps834.65 kBPostscriptView/Open
Title: Timed Processes: Models, Axioms and Decidability
Authors: Chen, Liang
Supervisor(s): Anderson, Stuart
Power, John
Issue Date: Jul-1993
Publisher: University of Edinburgh. College of Science and Engineering. School of Informatics.
Abstract: This thesis presents and studies a timed computational model of parallelism, a Timed Calculus of Communicating Systems or Timed CCS for short. Timed CCS is an extension of Milner's CCS with time. We allow time to be discrete, such as the natural numbers, or dense, such as the non-negative rationals or the non-negative reals. We make no assumption of the Maximal Progress Principle, but the calculus is consistent with the principle. Time variables in the language allow us to express a notion of time dependency and the language is more expressive than those without time variables or infinite summation. We extend the well known notion of bisimulation to timed processes and study the abstract sensation of timed processes. We show that strong equivalence (the largest strong bisimulation) is decidable for finite processes, i.e. processes without recursion. The decidability is independent of the choice of time domain. We also present a simple proof system for strong equivalence and the proof system is again independent of the choice of time domain. We show that the proof system is sound and complete for finite processes over dense time domains, but only complete for a restricted language over discrete time domains. We discuss how to modify the definition of time expressions to get the restricted language. We also study behavioural abstraction in timed processes. The thesis also presents and studies a general model, Timed Synchronisation Trees, for timed calculi. Timed synchronisation trees are extensions of synchronisation trees with time. All constructions on timed synchronisation trees are continuous with respect to a natural complete partial order. We can interpret a wide range of real-time process algebras in timed synchronisation trees. As an example, we give a denotational semantics for Timed CCS based on timed synchronisation trees. We show that the denotational and operational semantics of Timed CCS coincide. CCS is a symbolic calculus in the sense that it treats solely the observation of events of a system. The relative time, location and duration of events are abstracted away from the consideration. If we postulate that every action has a non-zero constant duration, we can observe the usual notions of causality, concurrency and conflict relations of events of a system. By interpreting CCS in Timed CCS based on a postulation that for any two events which are causally related there is at least a non-zero constant delay between them, we get a timed semantics for CCS. The timed semantics of CCS is a partial order or true concurrency semantics. As a consequence, we develop a partial order or true concurrency semantics based on an interleaving approach.
Sponsor(s): TC scholarship (British Council)
Appears in Collections:Informatics thesis and dissertation collection

Items in ERA are protected by copyright, with all rights reserved, unless otherwise indicated.


Valid XHTML 1.0! Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh 2013, and/or the original authors. Privacy and Cookies Policy