Precongruence formats with lookahead through modal decomposition

Wan Fokkink, Rob J. Van Glabbeek

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review


Bloom, Fokkink & van Glabbeek (2004) presented a method to decompose formulas from Hennessy-Milner logic with regard to a structural operational semantics specification. A term in the corresponding process algebra satisfies a Hennessy-Milner formula if and only if its subterms satisfy certain formulas, obtained by decomposing the original formula. They used this decomposition method to derive congruence formats in the realm of structural operational semantics. In this paper it is shown how this framework can be extended to specifications that include bounded lookahead in their premises. This extension is used in the derivation of a congruence format for the partial trace preorder.

Original languageEnglish
Title of host publicationComputer Science Logic 2017, CSL 2017
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959770453
Publication statusPublished - 1 Aug 2017
Event26th Annual EACSL Conference on Computer Science Logic, CSL 2017 - Stockholm, Sweden
Duration: 20 Aug 201724 Aug 2017


Conference26th Annual EACSL Conference on Computer Science Logic, CSL 2017


  • Compositionality
  • Congruence
  • Lookahead
  • Modal Decomposition
  • Modal Logic
  • Structural Operational Semantics


Dive into the research topics of 'Precongruence formats with lookahead through modal decomposition'. Together they form a unique fingerprint.

Cite this