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.
Type de document :
Communication dans un congrès
FSTTCS - IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Dec 2011, Mumbai, India. 538, pp.54 - 69, 2014
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01088038
Contributeur : Uli Fahrenberg <>
Soumis le : jeudi 27 novembre 2014 - 11:31:39
Dernière modification le : mercredi 16 mai 2018 - 11:24:07
Document(s) archivé(s) le : lundi 2 mars 2015 - 09:22:05

Fichier

fsttcs.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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. 538, pp.54 - 69, 2014. 〈hal-01088038〉

Partager

Métriques

Consultations de la notice

334

Téléchargements de fichiers

68