A Coalgebraic Approach to Probabilistic Transition Systems
by
James Worrell
Department of Mathematics, Tulane University
Coauthors: Franck van Breugel (Department of Computer Science, York University, Toronto)

This talk is concerned with the semantics of a class of reactive probabilistic transition systems, namely the labelled Markov processes (lMps) of Desharnais, Gupta, Jagadeesan and Panangaden. We consider lMps as coalgebras of a certain functor on the category of measurable spaces; this functor is closely based on the Giry monad. One of our main results is to show the existence of a final lMp. This can be seen as a domain of bisimulation equivalence classes of probabilistic processes.

The construction of the final lMp proceeds indirectly. The idea is to consider the Hutchinson metric on probability measures and thus import techniques from metric domain theory. As a consequence we obtain a natural metric on the state space of the final lMp. Separately, we also define a `logical distance' pseudometric on the class of lMp s via a real-valued modal logic, and we show that the resultant space is equivalent (as a pseudometric space) to the final lMp. We characterize the logical distance of processes in terms of a quantitative notion of probabilistic bisimulation. The latter has an attractive description in terms of minimal-cost network flows. Finally, we give a free-algebra characterization of the Hutchinson metric.

http://www.cs.yorku.ca/~franck/research/verification.html

Date received: May 14, 2001

Copyright © 2001 by the author(s). The author(s) of this document and the organizers of the conference have granted their consent to include this abstract in Atlas Conferences Inc. Document # cagw-35.