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.
|Period||12/12/2011 → 14/12/2011|
|Series||Leibniz International Proceedings in Informatics|
- Quantitative verification
- System distance
- Distance hierarchy
- Linear time
- Branching time