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.
Type de document :
Article dans une revue
Theoretical Computer Science, Elsevier, 2014, pp.54-69. 〈10.1016/j.tcs.2013.07.030〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01087368
Contributeur : Uli Fahrenberg <>
Soumis le : mardi 25 novembre 2014 - 22:00:10
Dernière modification le : jeudi 17 mai 2018 - 12:52:03
Document(s) archivé(s) le : jeudi 26 février 2015 - 12:35:51

Fichier

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

Identifiants

Citation

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〉

Partager

Métriques

Consultations de la notice

358

Téléchargements de fichiers

84