A Behavioural Pseudometric based on λ--Bisimilarity

In order to describe approximate equivalence among processes, the notions of @l-bisimilarity and behavioural pseudometric have been introduced by Ying and van Breugel respectively. Van Breugel provides a distance function induced by @l-bisimilarity, and conjectures that his behavioural pseudometric coincides with this function. This paper is inspired by this conjecture. We give a negative answer for van Breugel's conjecture first. Moreover, we show that the distance function induced by @l-bisimilarity is a pseudometric on states, and provide a fixed point characterization of this pseudometric.