Skip to Main content Skip to Navigation
Conference papers

The quantitative linear-time–branching-time spectrum

Uli Fahrenberg 1 Axel Legay 1 Claus Thrane 2 
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 provide fixed-point characterizations of all system distances, and we 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

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/hal-01088038
Contributor : Uli Fahrenberg Connect in order to contact the contributor
Submitted on : Thursday, November 27, 2014 - 11:31:39 AM
Last modification on : Wednesday, February 2, 2022 - 3:50:40 PM
Long-term archiving on: : Monday, March 2, 2015 - 9:22:05 AM

File

fsttcs.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01088038, version 1

Citation

Uli Fahrenberg, Axel Legay, Claus Thrane. The quantitative linear-time–branching-time spectrum. FSTTCS - IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Dec 2011, Mumbai, India. pp.54 - 69. ⟨hal-01088038⟩

Share

Metrics

Record views

216

Files downloads

75