期刊
THEORETICAL COMPUTER SCIENCE
卷 813, 期 -, 页码 20-69出版社
ELSEVIER
DOI: 10.1016/j.tcs.2019.09.019
关键词
Trace metric; Testing metric; Bisimulation metric; Nondeterministic probabilistic processes
资金
- project 'Open Problems in the Equational Logic of Processes' (OPEL) of the Icelandic Research Fund [196050-051]
Behavioral equivalences were introduced as a simple and elegant proof methodology for establishing whether the behavior of two processes cannot be distinguished by an external observer. The knowledge of observers usually depends on the observations that they can make on process behavior. Furthermore, the combination of nondeterminism and probability in concurrent systems leads to several interpretations of process behavior. Clearly, different kinds of observations as well as different interpretations lead to different kinds of behavioral relations, such as (bi)simulations, traces and testing. If we restrict our attention to linear properties only, we can identify three main approaches to trace and testing semantics: the trace distributions, the trace-by-trace and the extremal probabilities approaches. In this paper, we propose novel notions of behavioral metrics that are based on the three classic approaches above, and that can be used to measure the disparities in the linear behavior of processes with respect to trace and testing semantics. We study the properties of these metrics, like compositionality (expressed in terms of the nonexpansiveness property), and we compare their expressive powers. More precisely, we compare them also to (bi)simulation metrics, thus obtaining the first metric linear time - branching time spectrum. (C) 2019 Elsevier B.V. All rights reserved.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据