A Fully Abstract Presheaf Semantics of SCCS with Finite Delay

We present a presheaf model for the observation of infinite as wellas finite computations. We apply it to give a denotational semantics ofSCCS with finite delay, in which the meanings of recursion are given byfinal coalgebras and meanings of finite delay by initial algebras of theprocess equations for delay. This can be viewed as a first step in representingfairness in presheaf semantics. We give a concrete representationof the presheaf model as a category of generalised synchronisationtrees and show that it is coreflective in a category of generalised transitionsystems, which are a special case of the general transition systemsof Hennessy and Stirling. The open map bisimulation is shown to coincidewith the extended bisimulation of Hennessy and Stirling. Finallywe formulate Milners operational semantics of SCCS with finite delayin terms of generalised transition systems and prove that the presheafsemantics is fully abstract with respect to extended bisimulation