In this talk we present the content of a forthcoming CWI technical report, which introduces and discusses an operator specification format for labelled probabilistic transition systems. Because of its similarity to the known GSOS rules for nondeterministic systems, the format is called probabilistic GSOS. Early this year, we have already …read more
The talk will be about a recently finished paper of the same name (obtainable via my homepage at http://www.cwi.nl/~bartels).
Transition systems are often specified by operational rules in GSOS format, the models of which are known to be well behaved in many respects. Turi and Plotkin …read more
In the setting of (nondeterministic) labeled transition systems, Turi and Plotkin  found that GSOS rules essentially correspond to natural transformations of a certain type, which they call abstract GSOS. Those in turn correspond to distributive laws of a monad over a copointed functor as Lenisa, Power, and Watanabe [2 …read more
The carrier sets of final coalgebras have been shown (amongst others by Jan Rutten) to be a suitable domain to model infinite datatypes or the behaviour of dynamical systems. The basic means to characterise their elements (also called states here) is the coiteration schema, which is directly related to the …read more
For a given behavior type (functor), the carrier of a final coalgebra provides a unique representative for each possible behavior. This property immediately leads to a definition (and proof) principle - called `coiteration' here - for functions from an arbitrary set to this carrier: To define the function's value on a given …read more
Page 1 / 1