–
Room P3.10, Mathematics Building
Operational semantics of guarded quiescent processes
We provide an operational semantics based on finite automata for the language of quiescent and guarded process terms presented by Costa and Sernadas in 1995. For each process there is a finite automaton that embodies the concepts of terminal and non-terminal states through the distinction between terms that denote processes in a quiescent (terminal) state and terms that denote processes in an active state (non-terminal). A rollback mechanism is also provided by transitions of "undo" actions from active states to another state (active or passive). The behaviour of a process is captured by a subset of the language recognised by the respective automaton. A relation of partial order between process terms is defined in order to prove full abstraction in this semantics for the closed terms of the language. Thus, we complete the Hennessys trinity, together with the denotational and the axiomatic semantics already introduced by Costa and Sernadas.