Document Open Access Logo

The Quantitative Linear-Time--Branching-Time Spectrum

Authors Uli Fahrenberg, Axel Legay, Claus Thrane

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2011.103.pdf
  • Filesize: 413 kB
  • 12 pages

Document Identifiers

Subject Classification

Keywords
  • Quantitative verification
  • System distance
  • Distance hierarchy
  • Linear time
  • Branching time

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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.

Cite As Get BibTex

Uli Fahrenberg, Axel Legay, and Claus Thrane. The Quantitative Linear-Time--Branching-Time Spectrum. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. 103-114, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011) https://doi.org/10.4230/LIPIcs.FSTTCS.2011.103

Author Details

Uli Fahrenberg
Axel Legay
Claus Thrane
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact