Skip to main content

TS

Precongruence formats with lookahead through modal decomposition

Authors

Wan Fokkink and Rob van Glabbeek

DATA61

Vrije Universiteit Amsterdam

Abstract

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.

BibTeX Entry

  @inproceedings{Fokkink_Glabbeek_17,
    publisher        = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
    doi              = {10.4230/LIPIcs.CSL.2017.25},
    series           = {Leibniz International Proceedings in Informatics (LIPIcs)},
    booktitle        = {26th EACSL Annual Conference on Computer Science Logic (CSL'17)},
    author           = {Fokkink, Wan and van Glabbeek, Rob},
    month            = aug,
    volume           = {82},
    keywords         = {structural operational semantics congruence formats modal decomposition bounded lookahead trace
                        preorder},
    year             = {2017},
    date             = {2017-8-17},
    title            = {Precongruence Formats with Lookahead through Modal Decomposition},
    type             = {Conference Paper - Refereed},
    pages            = {20 p.},
    address          = {Stockholm, Sweden}
  }

Download

Served by Apache on Linux on seL4.