Computing Branching Distances Using Quantitative Games

TL;DR

This paper presents a unified method for computing branching distances in labeled transition systems by translating them into path-building games, enabling efficient solutions across the linear-time--branching-time spectrum.

Contribution

It introduces a general translation approach from quantitative games to path-building games for computing branching distances, applicable to all common types.

Findings

Method can compute all branching distances in the linear-time--branching-time spectrum.

Path-building games are solvable using existing quantitative game techniques.

Provides a unified framework for analyzing system behaviors.

Abstract

We lay out a general method for computing branching distances between labeled transition systems. We translate the quantitative games used for defining these distances to other, path-building games which are amenable to methods from the theory of quantitative games. We then show for all common types of branching distances how the resulting path-building games can be solved. In the end, we achieve a method which can be used to compute all branching distances in the linear-time--branching-time spectrum.