Divide and congruence III: From decomposition of modal formulas to preservation of stability and divergence

Wan Fokkink, Rob van Glabbeek, Bas Luttik

Research output: Contribution to JournalArticleAcademicpeer-review

Abstract

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.

Original languageEnglish
Article number104435
Pages (from-to)1-31
Number of pages31
JournalInformation and Computation
Volume268
Early online date24 Jul 2019
DOIs
Publication statusPublished - 1 Oct 2019

Fingerprint

Preservation
Congruence
Divides
Divergence
Semantics
Decomposition
Decompose
Decomposition Method
Bisimulation
Transition Systems
Branching
Specification
Specifications
Requirements
Operator
Range of data

Keywords

  • Modal logic
  • Structural operational semantics
  • Weak semantics

Cite this

@article{657739affb2d4526b07a6ce3a4105e74,
title = "Divide and congruence III: From decomposition of modal formulas to preservation of stability and divergence",
abstract = "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.",
keywords = "Modal logic, Structural operational semantics, Weak semantics",
author = "Wan Fokkink and {van Glabbeek}, Rob and Bas Luttik",
year = "2019",
month = "10",
day = "1",
doi = "10.1016/j.ic.2019.104435",
language = "English",
volume = "268",
pages = "1--31",
journal = "Information and Computation",
issn = "0890-5401",
publisher = "Elsevier Inc.",

}

Divide and congruence III : From decomposition of modal formulas to preservation of stability and divergence. / Fokkink, Wan; van Glabbeek, Rob; Luttik, Bas.

In: Information and Computation, Vol. 268, 104435, 01.10.2019, p. 1-31.

Research output: Contribution to JournalArticleAcademicpeer-review

TY - JOUR

T1 - Divide and congruence III

T2 - From decomposition of modal formulas to preservation of stability and divergence

AU - Fokkink, Wan

AU - van Glabbeek, Rob

AU - Luttik, Bas

PY - 2019/10/1

Y1 - 2019/10/1

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

UR - http://www.scopus.com/inward/citedby.url?scp=85070419516&partnerID=8YFLogxK

U2 - 10.1016/j.ic.2019.104435

DO - 10.1016/j.ic.2019.104435

M3 - Article

VL - 268

SP - 1

EP - 31

JO - Information and Computation

JF - Information and Computation

SN - 0890-5401

M1 - 104435

ER -