Approximate bisimulation for metric doubly labeled transition system

Many researchers suggested extending bisimilarityto quantitative versions to avoid the rigidity of classical bisimilarity. To explore the relation between different notions of approximate bisimilarity mentioned in literature, in this paper, we present a quantitative extension of doubly labeled transition systems, MDLTS, where its states and actions form metric spaces. We then introduce two notions of approximate bisimilarity, (η, λ)-bisimilarity and (η, λ, α)-bisimilarity, and discuss their basic property. We also consider the special kind of (η, λ)-bisimilarity, λ-bisimilarity to characterize the branching distance with arbitrary discount α of metric labeled transition system. Finally, we discuss the translation between metric transition system and MDLTS which preserves the approximate bisimilarity.