Metrics for Action-labelled Quantitative Transition Systems

       Yuxin Deng, Tom Chothia, Catuscia Palamidessi, and Jun Pang


 This paper defines {\em action-labelled quantitative transition systems} as
 a general framework for combining qualitative and quantitative
 analysis. We define {\em state-metrics} as a natural extension of
 bisimulation from non-quantitative systems to quantitative
 ones. We then prove that any single state-metric corresponds to a 
 bisimulation and that the greatest state-metric corresponds to bisimilarity. 
 Furthermore, we provide two extended examples which show that our
 results apply to both probabilistic and weighted automata as special cases 
 of action-labelled quantitative transition systems.