反应式系统的条件互模拟等价性
Conditional Bisimilarity for Reactive Systems
AI总结：
本文在 Leifer-Milner 反应式系统中引入带应用条件的规则与条件互模拟等价性，给出多种等价定义及 up-to-context 证明技术，并通过 DPO 图重写示例与相关行为等价关系比较。
摘要：
Leifer 和 Milner 提出的反应式系统是一种抽象的范畴论重写框架，为推导互模拟同余关系提供了合适的框架。这一目标通过综合与环境的交互、从而获得组合式语义来实现。我们在两个层面上以条件丰富反应式系统的概念：首先，与早期工作一样，我们考虑用应用条件增强的规则；其次，我们研究条件互模拟等价性的概念。条件互模拟等价性使我们能够表述：只要环境满足给定条件，两个系统状态就是互模拟的。我们给出了条件互模拟等价性的若干等价定义，其中包括一个适用于具体证明、并采用 up-to-context（至上下文）技术的定义，并将其与相关行为等价关系进行比较。我们考虑了基于 DPO 图重写的示例，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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
