|
A Fully Abstract Presheaf Semantics of SCCS with Finite Delay
Thomas Troels Hildebrandt September 1999 |
Abstract:
We present a presheaf model for the observation of
infinite as well as finite computations. We apply it to give a
denotational semantics of SCCS with finite delay, in which the meanings of
recursion are given by final coalgebras and meanings of finite delay by
initial algebras of the process equations for delay. This can be viewed
as a first step in representing fairness in presheaf semantics. We give
a concrete representation of the presheaf model as a category of
generalised synchronisation trees and show that it is coreflective in a
category of generalised transition systems, which are a special case of
the general transition systems of Hennessy and Stirling. The open map
bisimulation is shown to coincide with the extended bisimulation of
Hennessy and Stirling. Finally we formulate Milners operational semantics of
SCCS with finite delay in terms of generalised transition systems and prove
that the presheaf semantics is fully abstract with respect to extended
bisimulation
Available as PostScript, PDF, DVI. |