An event-based operational semantics for a timed language of temporal ordering specifications (LOTOS)-like process algebra (http://wwwtios.cs.utwente.nl/lotos/) is introduced in this theoretical paper. The authors examine a language describing the processes built from a set Obs of observable actions having durations. This language supports both sequential and parallel composition, transfer of control, and refinement of an action by a more detailed process of the same duration and recursivity.
A first common approach of the semantics of such a language, the denotational true concurrency semantics, uses timed event structures. Such a structure consists of events labeled with actions, and connected by relations of causality and conflict. Two events e and e′ are in conflict if they cannot both occur in a single system run. If X is a set of events that are pairwise in conflict, X causes e if, when e happens, exactly one event in X happens before. How to interpret the language in a timed event structure is highly nontrivial. The summary given in paragraph 3.3 is impossible to understand, and one must go to the given references.
The heart of the paper is the introduction of an operational semantics defined by means of inference rules. Here, event identities are generated by annotating each action occurrence in expressions. The transition P → e,a,t P′ means that expression P can perform event e labeled with action a, finishes at time t, and then evolves into expression P′. One can write a list of axioms for this transition relation. The major result of the paper shows that the operational semantics is consistent with the previous denotational true concurrency semantics. If the matter is clearly not in its final stage, this operational approach seems to be more manageable.