On the trade-off between labels and weights in quantitative bisimulation

Abstract

Reductions for transition systems have been recently introduced as a uniform and principled method for comparing the expressiveness of system models with respect to a range of properties, especially bisimulations. In this paper we study the expressiveness (w.r.t. bisimulations) of models for quantitative computations such as weighted labelled transition systems (WLTSs), uniform labelled transition systems (ULTraSs), and state-to-function transition systems (FuTSs). We prove that there is a trade-off between labels and weights: at one extreme lays the class of (unlabelled) weighted transition systems where information is presented using weights only; at the other lays the class of labelled transition systems (LTSs) where information is shifted on labels. These categories of systems cannot be further reduced in any significant way and subsume all the aforementioned models.

References in corpus (7)

• Relating coalgebraic notions of bisimulation
• Behavioural equivalences for coalgebras with unobservable moves
• GSOS for non-deterministic processes with quantitative aspects
• Weak bisimulations for labelled transition systems weighted over semirings
• Bisimulation of Labelled State-to-Function Transition Systems Coalgebraically
• A Definition Scheme for Quantitative Bisimulation
• Reductions for Transition Systems at Work: Deriving a Logical Characterization of Quantitative Bisimulation