Computing branching distances with quantitative games

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.

Authors

• Uli Fahrenberg
• Axel Legay
• Karin Quaas

Keywords

• Quantitative verification
• Branching distance
• Quantitative game
• Path-building game