关于具有内部移动的余代数
On coalgebras with internal moves
摘要：
在本文的第一部分中，我们回顾了处理出现在不同的基于状态的系统语义中的所谓的不可见的转换的共代数方法。我们主张这些转移总是某个单子的单位的一部分。因此，具有内部移动的余代数恰是一元型上的余代数。本文的其余部分致力于支持我们的主张，通过研究两个重要的行为等价的基于状态的系统与内部移动，即：弱互模拟和跟踪语义。我们继续研究了富序单子上余代数的弱互模拟。在本文中使用的关键概念，并提出了我们在我们以前的工作是秩序饱和单子和饱和的概念。饱和算子可以直观地理解为自反的、传递的闭包算子。有两种方法来定义具有内部移动的余代数的饱和子。在这里，我们给出了必要条件，使他们产生相同的概念弱互模拟。最后，通过一致不动点算子给出了具有静默移动的余代数的迹语义的定义。我们比较了具有内部步骤的余代数的强、弱偏化以及迹语义。
英文摘要：
In the first part of the paper we recall the coalgebraic approach to handling the so-called invisible transitions that appear in different state-based systems semantics. We claim that these transitions are always part of the unit of a certain monad. Hence, coalgebras with internal moves are exactly coalgebras over a monadic type. The rest of the paper is devoted to supporting our claim by studying two important behavioural equivalences for state-based systems with internal moves, namely: weak bisimulation and trace semantics. We continue our research on weak bisimulations for coalgebras over order enriched monads. The key notions used in this paper and proposed by us in our previous work are the notions of an order saturation monad and a saturator. A saturator operator can be intuitively understood as a reflexive, transitive closure operator. There are two approaches towards defining saturators for coalgebras with internal moves. Here, we give necessary conditions for them to yield the same notion of weak bisimulation. Finally, we propose a definition of trace semantics for coalgebras with silent moves via a uniform fixed point operator. We compare strong and weak bisimilation together with trace semantics for coalgebras with internal steps.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
