The Quantitative Linear-Time--Branching-Time Spectrum

Authors Uli Fahrenberg, Axel Legay, Claus Thrane

Thumbnail PDF


  • Filesize: 413 kB
  • 12 pages

Document Identifiers

Author Details

Uli Fahrenberg
Axel Legay
Claus Thrane

Cite AsGet 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)


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.
  • Quantitative verification
  • System distance
  • Distance hierarchy
  • Linear time
  • Branching time


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail