Skip Navigation
York U: Redefine the PossibleHOME | Current Students | Faculty & Staff | Research | International
Search »FacultiesLibrariesCampus MapsYork U OrganizationDirectorySite Index
Future Students, Alumni & Visitors
2001 Technical Reports

An Algorithm for Quantitative Verification of Probabilistic Transition Systems

Franck van Breugel and James Worrell

Technical Report CS-2001-01

York University

April 2001


This paper is concerned with a notion of behavioral equivalence for reactive probabilistic transition systems as arise, say, in the operational semantics of probabilistic process calculi. We solve a domain equation in the category of metric spaces and nonexpansive maps involving a probabilistic powerdomain functor based on the Hutchinson metric on probability measures. The resultant domain can be considered as the space of bisimulation equivalence classes of (possibly continuous state) probabilistic processes. Furthermore, the metric on this space induces a natural pseudometric on the class of all probabilistic transition systems. This can be considered as a quantitative notion of behavioural equivalence for probabilistic processes which varies smoothly with respect to transition probabilities. Our main contribution is to give an algorithm to calculate the distance between finite state processes in polynomial time. The body of the main loop of the algorithm involves a linear optimization: the so-called transshipment problem.

Download paper in PDF format.

The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.