A large number of observational semantics for process description
languages have been
developed, many of which are based on the notion of bisimulation. In this
paper, we
consider in detail the problem of defining a semantic framework to unify
these. The
discussion takes place in a purely algebraic setting. We introduce a
special class of algebras
called Structured Transition Systems. A structured transition
system can
be viewed as a
transition system with an algebraic structure both on states and
transitions. In this
framework, observations of behaviours are dealt with by means of maps
from the transitions to some algebra of observations.Using several examples, we show that this framework allows us to
describe a range of
observational semantics within a single underlying presentation: it is
enough to consider
different mappings and algebras of observations. Furthermore, we introduce
a notion of
bisimulation that is parameterized with respect to the choice of the
algebra of observations,
and we find circumstances under which a Structured Transition System
has good properties
with respect to this parameterized bisimulation.First, some general syntactic constraints, independent from the choice
of the algebra of
the observations, are given for Structured Transition System presentations.
We show that
these constraints ensure that parameterized bisimulation is always a
congruence. Next, we
address the problem of Minimal Realizations. We show that when
the presentation satisfies
the syntactic constraints there exists a minimal realization, i.e.,
there is a model of the
presentation whose elements fully characterize congruence classes under
bisimulation.
Gauged double field theory as an L∞ algebra
