TY - GEN
T1 - Precongruence formats with lookahead through modal decomposition
AU - Fokkink, Wan
AU - Van Glabbeek, Rob J.
PY - 2017
Y1 - 2017
N2 - 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.
AB - 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.
KW - Compositionality
KW - Congruence
KW - Lookahead
KW - Modal Decomposition
KW - Modal Logic
KW - Structural Operational Semantics
UR - http://www.scopus.com/inward/record.url?scp=85028713738&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85028713738&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.CSL.2017.25
DO - 10.4230/LIPIcs.CSL.2017.25
M3 - Conference contribution
AN - SCOPUS:85028713738
T3 - Leibniz International Proceedings in Informatics (LIPIcs)
SP - 1
EP - 20
BT - 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 26th Annual EACSL Conference on Computer Science Logic, CSL 2017
Y2 - 20 August 2017 through 24 August 2017
ER -