Coalgebraic Modelling of Timed Processes
Marco KickAbstract:
This thesis presents an abstract mathematical account of timed processes and their operational semantics, where time is modelled by a special kind of monoids, so-called time domains, and (the operational behaviour of) timed processes is represented by special labelled transition systems, so-called timed transition systems (TTSs), together with time bisimulation as an appropriate notion of equivalence of such processes.
The importance of monoid-related notions for describing timed phenomena is then illustrated by showing that TTSs are the same as the (partial) actions of the monoid of time; moreover, total monoid actions are also shown to arise naturally in this approach in the form of delay operators. The two kinds of monoid actions are suitably combined in a new notion of biaction which captures the interplay of two very important features of timed processes: letting time pass and delaying.
The TTSs are then characterised as coalgebras of a novel evolution comonad, which is inspired by well-known categorical descriptions of total monoid actions; in doing so, a coalgebraic description of time bisimulation is also provided. Additionally, biactions are characterised as bialgebras of a distributive law of a monad (for total monoid actions) over a comonad (the evolution comonad for partial monoid actions).
Building on these results, it is possible to obtain an abstract categorical treatment of operational rules for timed processes. The approach taken here is based on the framework by Turi and Plotkin [TP97], using distributive laws and bialgebras (similar to the treatment of biactions), and which, subsequently, is extended to accommodate behaviour comonads, as required for the coalgebraic description of TTSs.
These abstract rules then form the basis for the development of several new syntactic rule formats for timed processes which describe classes of particularly 'well-behaved' languages for specifying timed processes.
This is a 286-page thesis.
This report is available in the following formats:
Previous | Index | Next