期刊名称：Electronic Proceedings in Theoretical Computer Science
电子版ISSN：2075-2180
出版年度：2011
卷号：57
页码：134-147
DOI：10.4204/EPTCS.57.10
出版社：Open Publishing Association
摘要：We develop a general framework for reasoning about distances between transition systems with quantitative information. Taking as starting point an arbitrary distance on system traces, we show how this leads to natural definitions of a linear and a branching distance on states of such a transition system. We show that our framework generalizes and unifies a large variety of previously considered system distances, and we develop some general properties of our distances. We also show that if the trace distance admits a recursive characterization, then the corresponding branching distance can be obtained as a least fixed point to a similar recursive characterization. The central tool in our work is a theory of infinite path-building games with quantitative objectives.
