Reductions for Transition Systems at Work: Deriving a Logical Characterization of Quantitative Bisimulation

TL;DR

This paper demonstrates that various weighted transition system models can be unified through reductions, enabling the derivation of a logical characterization of quantitative bisimulation applicable across these models.

Contribution

It shows the collapse of the hierarchy of meta-models under bisimulation-coherent encodings and derives a fully abstract logic for FuTSs from WLTSs.

Findings

Hierarchy of models collapses under bisimulation-coherent encodings

A fully abstract Hennessy-Milner logic for FuTSs is derived

Logical characterization of quantitative bisimulation is achieved

Abstract

Weighted labelled transition systems (WLTSs) are an established meta-model aiming to provide general results and tools for a wide range of systems such as non-deterministic, stochastic, and probabilistic systems. In order to encompass processes combining several quantitative aspects, extensions of the WLTS framework have been further proposed, state-to-function transition systems (FuTSs) and uniform labelled transition systems (ULTraSs) being two prominent examples. In this paper we show that this hierarchy of meta-models collapses when studied under the lens of bisimulation-coherent encodings. Taking advantage of these reductions, we derive a fully abstract Hennessy-Milner-style logic for FuTSs, i.e., which characterizes quantitative bisimilarity, from a fully-abstract logic for WLTSs.