A Consistent Causality-Based View on a Timed Process Algebra Including Urgent Interactions

摘要

This paper discusses a timed variant of a process algebra akin to LOTOS, baptized UPA, in a causality- based setting. Two timed features are incorporated-a delay function which constrains the occurrence time of atomic actions and an urgency operator that forces (local or synchronized) actions to happen urgently. Timeouts are typical urgent phenomena. A novel timed extension of event structures is introduced and used as a vehicle to provide a denotational causality-based semantics for UPA. Recursion is dealt with by using standard fixpoint theory. In addition, an operational semantics is presented based on separate time- and action-transitions that is shown to be consistent with the event structure semantics.