TY - GEN
T1 - Divide and congruence III
T2 - 28th International Conference on Concurrency Theory, CONCUR 2017
AU - Fokkink, Wan
AU - Glabbeek, Rob Van
AU - Luttik, Bas
PY - 2017
Y1 - 2017
N2 - In two earlier papers we derived congruence formats 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. Here this work is extended with important stability and divergence requirements. 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. 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 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. Here this work is extended with important stability and divergence requirements. 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. 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 - https://www.scopus.com/pages/publications/85030110903
UR - https://www.scopus.com/inward/citedby.url?scp=85030110903&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.CONCUR.2017.15
DO - 10.4230/LIPIcs.CONCUR.2017.15
M3 - Conference contribution
AN - SCOPUS:85030110903
T3 - Leibniz International Proceedings in Informatics
SP - 1
EP - 16
BT - 28th International Conference on Concurrency Theory (CONCUR 2017)
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Y2 - 5 September 2017 through 8 September 2017
ER -