Enabling preserving bisimilarity is a refinement of strong bisimilarity, which preserves safety as well as liveness properties. To define it properly, labelled transition systems needed to be upgraded with a successor relation, capturing concurrency between transitions enabled in the same state. We enrich the well-known De Simone format to handle inductive definitions of this successor relation. We then establish that ep-bisimilarity is a congruence for the operators, as well as lean congruence for recursion, for all (enriched) De Simone languages.

翻译：使能保持双相似性是对强双相似性的精化，它同时保持了安全性和活性性质。为正确定义该概念，标记转换系统需要升级为带有后继关系，以捕获同一状态下使能转换之间的并发性。我们丰富了著名的德西蒙格式，以处理该后继关系的归纳定义。随后证明，对于所有（扩展的）德西蒙语言，EP-双相似性对于算子构成同余关系，而对于递归则构成精简同余关系。