The quantitative linear-time–branching-time spectrum - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Theoretical Computer Science Année : 2014

The quantitative linear-time–branching-time spectrum

Résumé

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.
Fichier principal
Vignette du fichier
qltbt.pdf (581.33 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-01087368 , version 1 (25-11-2014)

Identifiants

Citer

Uli Fahrenberg, Axel Legay. The quantitative linear-time–branching-time spectrum. Theoretical Computer Science, 2014, pp.54-69. ⟨10.1016/j.tcs.2013.07.030⟩. ⟨hal-01087368⟩
202 Consultations
91 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More