一句话：在 Leifer-Milner 反应式系统中引入条件互模拟，给出等价定义并比较相关行为等价。
本文研究 Leifer 与 Milner 提出的反应式系统——一种基于范畴的抽象重写框架，它通过合成与环境交互来导出互模拟同余。作者从两个层面加入条件：一是重写规则可带应用条件，二是提出条件互模拟，用以表达当环境满足给定条件时两个系统状态才互模拟。论文给出条件互模拟的多种等价定义，其中包括利用 up-to-context 技术、便于具体证明的定义，并与相关行为等价进行比较。文中还在 DPO 图重写这一反应式系统实例上给出示例，说明该理论的适用范围。
Reactive systems \`a 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.
@article{paperbot1747,
title = {Conditional Bisimilarity for Reactive Systems},
author = {Mathias Hülsbusch and Barbara König and Sebastian Küpper and Lara Stoltenow},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 1},
year = {2022},
doi = {10.46298/lmcs-18(1:6)2022}
}