Skip to Main content Skip to Navigation
Journal articles

The quantitative linear-time–branching-time spectrum

Uli Fahrenberg 1 Axel Legay 1 
1 ESTASYS - Efficient STAtistical methods in SYstems of systems
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : We present a distance-agnostic approach to quantitative verification. Taking as input an unspecified distance on system traces, or executions, we develop a game-based framework which allows us to define a spectrum of different interesting system distances corresponding to the given trace distance. Thus we extend the classic linear-time–branching-time spectrum to a quantitative setting, parametrized by trace distance. We also prove a general transfer principle which allows us to transfer counterexamples from the qualitative to the quantitative setting, showing that all system distances are mutually topologically inequivalent.
Complete list of metadata
Contributor : Uli Fahrenberg Connect in order to contact the contributor
Submitted on : Tuesday, November 25, 2014 - 10:00:10 PM
Last modification on : Wednesday, February 2, 2022 - 3:50:48 PM
Long-term archiving on: : Thursday, February 26, 2015 - 12:35:51 PM


Files produced by the author(s)



Uli Fahrenberg, Axel Legay. The quantitative linear-time–branching-time spectrum. Theoretical Computer Science, Elsevier, 2014, pp.54-69. ⟨10.1016/j.tcs.2013.07.030⟩. ⟨hal-01087368⟩



Record views


Files downloads