Branching vs. Linear Time: Semantical Perspective
Branching vs. Linear Time: Semantical Perspective
复制标题
分支与线性时间：语义视角
DOI：
10.1007/978-3-540-75596-8_4
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
Moshe Y. Vardi
中科院分区：
文献类型：
--
作者：
Sumit Nain;Moshe Y. Vardi
在计算机科学文献中，关于线性时间框架与分支时间框架的相对优点的讨论可以追溯到20世纪80年代初。主导这场讨论的一个信念是，线性时间框架在语义上表达不够，使得线性时间逻辑缺乏表达能力。在这项工作中，我们研究的分支线性问题的角度来看，进程等价，这是并发理论中最基本的概念之一，定义一个概念的进程等价基本上相当于定义语义的进程。在过去的三十年里，许多过程等效的概念已经提出。这一领域的研究人员不再试图确定“正确”的对等概念。相反，重点已经转移到提供分类框架，如“线性分支光谱”，为许多提出的概念，并试图确定适合不同的应用程序。我们假设三个原则，我们认为是根本的任何讨论过程的等效性。首先，我们借用指称语义学的研究，把观察对等作为对等的主要概念。这消除了许多测试场景，因为太强或太弱。其次，我们要求流程的描述来充分指定流程的所有相关行为方面。最后，我们要求可观察的流程行为反映在其输入/输出行为中。在这些假设下，线性语义和分支语义之间的区别趋于消失。作为一个例子，我们将这些原则的框架换能器，一个经典的概念，基于状态的过程，可以追溯到20世纪50年代，非常适合硬件建模。我们表明，我们的假设结果在一个独特的概念，这是基于跟踪，而不是基于树的过程等价。
The discussion in the computer-science literature of the relative merits of linear- versus branching-time frameworks goes back to early 1980s. One of the beliefs dominating this discussion has been that the linear-time framework is not expressive enough semantically, making linear-time logics lacking in expressiveness. In this work we examine the branching-linear issue from the perspective of process equivalence, which is one of the most fundamental notions in concurrency theory, as defining a notion of process equivalence essentially amounts to defining semantics for processes. Over the last three decades numerous notions of process equivalence have been proposed. Researchers in this area do not anymore try to identify the “right” notion of equivalence. Rather, focus has shifted to providing taxonomic frameworks, such as “the linear-branching spectrum”, for the many proposed notions and trying to determine suitability for different applications.We revisit here this issue from a fresh perspective. We postulate three principles that we view as fundamental to any discussion of process equivalence. First, we borrow from research in denotational semantics and take observational equivalence as the primary notion of equivalence. This eliminates many testing scenarios as either too strong or too weea. Second, we require the description of a process to fully specify all relevant behavioral aspects of the process. Finally, we require observable process behavior to be reflected in its input/output behavior. Under these postulates the distinctions between the linear and branching semantics tend to evaporate. As an example, we apply these principles to the framework of transducers, a classical notion of state-based processes that dates back to the 1950s and is well suited to hardware modeling. We show that our postulates result in a unique notion of process equivalence, which is trace based, rather than tree based.