Journal
THEORETICAL COMPUTER SCIENCE
Volume 538, Issue -, Pages 54-69Publisher
ELSEVIER
DOI: 10.1016/j.tcs.2013.07.030
Keywords
Quantitative verification; System distance; Distance hierarchy; Linear time; Branching time
Categories
Ask authors/readers for more resources
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. (C) 2013 Elsevier B.V. All rights reserved.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available