Metric Process Models

摘要

Among the various formal models proposed to provide semantics for concurrencyconstructs in programming languages, partial orders have the advantages of conceptual simplicity, mathematical tractability, and economy of expression. We first observe that the theory of enriched categories supplies a natural abstraction of the notion of partial order, the D-schedule. Varying the choice of temporal domain D allows for other forms of temporal constraint beyond that available from simple ordering. For example, having the constraints on inter-event delays be numeric bounds produces a generalized metric-space structure suitable for the discussion of real-time computation. We then construct an algebra of processes parametrized by notion of time. Here a process is a structure based on schedules that also incorporates nondeterminism. Since the model is category-based, we can define operations on D-schedules and processes via universal constructions that depend little on the choice of D. Also, given a suitable choice of process structure and process morphism, the constructions used for process operations and schedule operations are remarkably similar.