Semantics Club 02 03 2001
In this talk, we will present a mathematical model of real time process algebras like Temporal CCS [MT90].
The two main notions will be a linearly ordered monoid M, representing the domain of time, and actions of that monoid. The monoid actions will serve to describe two different features: a total (left) action denoting a delaying operation on processes, and a partial (right) action denoting the passage of time, related in a suitable way.
Technically, the main ingredient is a "real time comonad" on the category of M-actions whose coalgebras will not only carry an M-action structure but also an additional partial M-action structure. Therefore we will call those structures "M-biactions".
We will then generalise the framework of [TP97], where it was shown that a set of GSOS rules corresponds to a natural transformation of a certain type parametrised in functorial notions of syntax and behaviour on the category Set, in order to accdomodate the view of transition systems as coalgebras for comonads, rather than just coalgebras for a behaviour endofunctor.
This will eventually lead to both a format for and side conditions on operational rules which will ensure that the transition system on processes as defined by the rules will be indeed an M-biaction structure.
[MT90] F. Moller, C. Tofts, A Temporal Calculus of Communicating Systems, CONCUR'90
[TP97] D. Turi, G. Plotkin, Towards a Mathematical Operational Semantics, LICS'97