1 Department of Computer Science, The Technical Faculty of IT and Design, Aalborg University, VBN2 Distributed Systems and Semantics, The Technical Faculty of IT and Design, Aalborg University, VBN3 The Faculty of Engineering and Science (TECH), Aalborg University, VBN4 IRISA Rennes
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.
Lipics : Leibniz International Proceedings in Informatics, 2011
Quantitative verification; System distance; Distance hierarchy; Linear time; Branching time