An Abstract Coalgebraic Approach to Process Equivalence for Well-Behaved Operational Semantics
An Abstract Coalgebraic Approach to Process Equivalence for Well-Behaved Operational Semantics
复制标题
良好操作语义的过程等价的抽象代数方法
DOI：
--
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
Bartek Klin
中科院分区：
文献类型：
--
作者：
Bartek Klin
本论文是旨在寻找行为良好的结构操作语义的数学理论的计划的一部分。1997年，Turi和Plotkin在一篇开创性的论文中展示了一般性和基本的结果，从两个方向进行了扩展，旨在提高框架的表现力。Turi和Plotkin的所谓双代数框架是著名的结构化操作语义格式GSOS的抽象推广，提供了一种以互模拟等价为同余的操作语义规则理论。本论文的第一部分旨在将该框架扩展到包括其他操作等价和预序(例如迹等价)，统称为van GLabbeek谱。要做到这一点，需要一种新的协代数方法来处理进程上的关系，因为通常将余代数互模拟作为余代数的跨度的方法并不容易扩展到进程上的其他已知等价。提出了一种基于测试集纤化的方法。在此基础上，给出了同余格式的抽象刻画，并用期望合成的过程关系进行了参数化。然后，将该抽象刻画专门用于迹等价、完全迹等价和失败等价的情况。在后两种情况下，获得了新的同余格式，扩展了该研究领域的当前技术状态。论文的第二部分旨在扩展双代数框架以涵盖由(可能无保护的)递归方程定义的一类一般的递归语言结构。由于不设防的方程可能是发散的来源，整个框架被解释在适当的域类别中，而不是集合和函数的类别中。结果表明，一类称为正则方程的递归方程可以与GSOS运算规则无缝合并，从而为扩展了递归结构的语言提供了良好的运算语义。
This thesis is part of the programme aimed at finding a mathematical theory of well-behaved structural operational semantics. General and basic results shown in 1997 in a seminal paper by Turi and Plotkin are extended in two directions, aiming at greater expressivity of the framework. The so-called bialgebraic framework of Turi and Plotkin is an abstract generalization of the well-known structural operational semantics format GSOS, and provides a theory of operational semantic rules for which bisimulation equivalence is a congruence. The first part of this thesis aims at extending that framework to cover other operational equivalences and preorders (e.g. trace equivalence), known collectively as the van Glabbeek spectrum. To do this, a novel coalgebraic approach to relations on processes is desirable, since the usual approach to coalgebraic bisimulations as spans of coalgebras does not extend easily to other known equivalences on processes. Such an approach, based on fibrations of test suites, is presented. Based on this, an abstract characterization of congruence formats is given, parametrized by the relation on processes that is expected to be compositional. This abstract characterization is then specialized to the case of trace equivalence, completed trace equivalence and failures equivalence. In the two latter cases, novel congruence formats are obtained, extending the current state of the art in this area of research. The second part of the thesis aims at extending the bialgebraic framework to cover a general class of recursive language constructs, defined by (possibly unguarded) recursive equations. Since unguarded equations may be a source of divergence, the entire framework is interpreted in a suitable domain category, instead of the category of sets and functions. It is shown that a class of recursive equations called regular equations can be merged seamlessly with GSOS operational rules, yielding well-behaved operational semantics for languages extended with recursive constructs.