TY - JOUR
T1 - Divide and congruence III
T2 - from decomposition of modal formulas to preservation of stability and divergence
AU - Fokkink, Wan J.
AU - van Glabbeek, Rob
AU - Luttik, Bas
PY - 2019/10
Y1 - 2019/10
N2 - 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.
AB - 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.
KW - Modal logic
KW - Structural operational semantics
KW - Weak semantics
UR - http://www.scopus.com/inward/record.url?scp=85070419516&partnerID=8YFLogxK
U2 - 10.1016/j.ic.2019.104435
DO - 10.1016/j.ic.2019.104435
M3 - Article
AN - SCOPUS:85070419516
SN - 0890-5401
VL - 268
JO - Information and Computation
JF - Information and Computation
M1 - 104435
ER -