AbstractMany real-time process algebras have the maximal progress assumption. In those process algebras, the time intervals in which actions are enabled are left-closed. This paper presents a process algebra that satisfies the maximal progress assumption and allows left-open intervals. A non-observable time step is introduced to model the time when an urgent action enabled in interval (0,1) is taken. Furthermore, we have to distinguish between observable actions and actions which only get enabled after a non-observable time step. This is necessary, since the latter actions may only produce internal actions. The distinction is done by extending the set of actions by marked actions.
The real-time process algebra presented here is an extension of Milner's CCS. This algebra can be used to model dynamic priority of actions at the same point in time. We introduce various equivalence relations based on bisimulation.
Categories and Subject Descriptors: F.1.2 [Computation by Abstract Devices]: Modes of Computation; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages
Additional Key Words and Phrases: real-time, process algebra, maximal progress, open intervals, bisimulation, priority
Selected references
- Eric Badouel and Philippe Darondeau. On guarded recursion. Theoretical Computer Science, 82(2):403-408, 31 May 1991. Note.
- J C M Baeten and J A Bergstra. Real time process algebra. Formal Aspects of Computing, 3(2):142-188, 1991.
- Rance Cleaveland and Matthew Hennessy. Priorities in process algebras. Information and Computation, 87(1/2):58-77, July/August 1990.
- Kim G. Larsen and Yi Wang. Time-abstracted bisimulation: Implicit specifications and decidability. Information and Computation, 134(2):75-101, 1 May 1997.
- G. M. Reed and A. W. Roscoe. A timed model for communicating sequential processes. Theoretical Computer Science, 58(1-3):249-261, July 1988.