分而同III：从模态公式的分解到保稳保散
Divide and Congruence III: From Decomposition of Modal Formulas to Preservation of Stability and Divergence
摘要：
在两个较早的文件，我们推导出同余格式关于弱语义的转换系统规范的基础上的模态公式的分解方法。其思想是，语义的一致格式必须确保该语义的模态表征中的公式总是被分解为再次处于该模态表征中的公式。到目前为止，强加在许多已知的弱语义上的稳定性和发散性要求已经超出了这种方法的范围。稳定性是指不存在$τ$ -转变。我们展示了，使用分解方法，同余格式可以放松弱语义，是稳定的尊重。例如，这种放松将优先级算子带入了尊重稳定性的分支互模拟格式的范围内。发散，这是指存在一个无限序列的$τ$ -跃迁，逃避归纳分解方法。我们绕过这个问题，证明了一个稳定的弱语义的同余格式也是一个同余格式，其分歧保持对应。
英文摘要：
In two earlier papers we derived congruence formats with regard to transition system specifications for weak semantics on the basis of a decomposition method for modal formulas. The idea is that a congruence format for a semantics must ensure that the formulas in the modal characterisation of this semantics are always decomposed into formulas that are again in this modal characterisation. The stability and divergence requirements that are imposed on many of the known weak semantics have so far been outside the realm of this method. Stability refers to the absence of a $τ$-transition. We show, using the decomposition method, how congruence formats can be relaxed for weak semantics that are stability-respecting. This relaxation for instance brings the priority operator within the range of the stability-respecting branching bisimulation format. Divergence, which refers to the presence of an infinite sequence of $τ$-transitions, escapes the inductive decomposition method. We circumvent this problem by proving that a congruence format for a stability-respecting weak semantics is also a congruence format for its divergence-preserving counterpart.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
