–
Room P3.10, Mathematics Building
Hélia Guerra, U Açores
A trinity for finite processes with global liveness requirements
We extend the quiescent model with two operators denoting global liveness requirements: ! and [-]. When the operator ! is applied to a process term we obtain the maximum activation of the corresponding process. The operator [-] applied to a process term induces a transactional behaviour until the execution of some determined action. The suitable semantics domains (denotational, axiomatic, and operational) are obtained through the introduction of new sets of traces, new axioms and new transition rules. The final result is a trinity in the sense of Hennessy (equivalencies among the three semantics domains).