论文标题
反应性系统的条件性双歧性
Conditional Bisimilarity for Reactive Systems
论文作者
论文摘要
反应性系统àlaLeifer and Milner是一个用于重写的抽象分类框架，为推导双仿真的框架提供了合适的框架。这是通过合成与环境的相互作用以获得组成语义来完成的。 我们通过两个层面的条件来丰富反应性系统的概念：首先，与较早的工作一样，我们认为规则富含应用条件，其次，我们研究了条件双性异性的概念。有条件的二元性使我们可以说，只要环境满足给定的条件，两个系统状态是双象体的。 我们提出了有条件双性恋的几个等效定义，其中包括一种对具体证明有用的，并且采用了一种最新的文本技术，我们将其与相关的行为等价进行了比较。我们考虑基于DPO图重写的示例，即反应性系统的实例化。
Reactive systems à la Leifer and Milner, an abstract categorical framework for rewriting, provide a suitable framework for deriving bisimulation congruences. This is done by synthesizing interactions with the environment in order to obtain a compositional semantics. We enrich the notion of reactive systems by conditions on two levels: first, as in earlier work, we consider rules enriched with application conditions and second, we investigate the notion of conditional bisimilarity. Conditional bisimilarity allows us to say that two system states are bisimilar provided that the environment satisfies a given condition. We present several equivalent definitions of conditional bisimilarity, including one that is useful for concrete proofs and that employs an up-to-context technique, and we compare with related behavioural equivalences. We consider examples based on DPO graph rewriting, an instantiation of reactive systems.
