2026-07-23T21:52:40Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3332 2024-03-06T10:34:04Z ddc:004 open_access

The Quantitative Linear-Time--Branching-Time Spectrum Fahrenberg, Uli Legay, Axel Thrane, Claus Quantitative verification System distance Distance hierarchy Linear time Branching time 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Uli Fahrenberg and Axel Legay and Claus Thrane 2011 Is Part Of LIPIcs, Volume 13, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2011.103 urn:nbn:de:0030-drops-33324 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2011.103 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode