We develop a pseudo-metric analogue of bisimulation for generalizedsemi-Markov processes. The kernel of this pseudo-metric corresponds tobisimulation; thus we have extended bisimulation for continuous-timeprobabilistic processes to a much broader class of distributions thanexponential distributions. This pseudo-metric gives a useful handle onapproximate reasoning in the presence of numerical information -- such asprobabilities and time -- in the model. We give a fixed point characterizationof the pseudo-metric. This makes available coinductive reasoning principles forreasoning about distances. We demonstrate that our approach is insensitive topotentially ad hoc articulations of distance by showing that it is intrinsic toan underlying uniformity. We provide a logical characterization of thisuniformity using a real-valued modal logic. We show that several quantitativeproperties of interest are continuous with respect to the pseudo-metric. Thus,if two processes are metrically close, then observable quantitative propertiesof interest are indeed close.
展开▼
