ACM/IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Twenty-Second Annual IEEE Symposium on

Logic in Computer Science (LICS 2007)

Paper: Bialgebraic Operational Semantics and Modal Logic (at LICS 2007)

Authors: Bartek Klin


A novel, general approach is proposed to proving the compositionality of process equivalences on languages defined by Structural Operational Semantics (SOS). The approach, based on modal logic, is inspired by the simple observation that if the set of formulas satisfied by a process can be derived from the corresponding sets for its subprocesses, then the logical equivalence is a congruence. Striving for generality, SOS rules are modeled categorically as bialgebraic distributive laws for some notions of process syntax and behaviour, and modal logics are modeled via coalgebraic polyadic modal logic. Compositionality is proved by providing a suitable notion of behaviour for the logic together with a dual distributive law, reflecting the one modeling the SOS specification. Concretely, the dual laws may appear as SOS-like rules where logical formulas play the role of processes, and their behaviour models logical decomposition over process syntax. The approach can be used either to proving compositionality for specific languages or for defining SOS congruence formats.


    author = 	 {Bartek Klin},
    title = 	 {Bialgebraic Operational Semantics and Modal Logic},
    booktitle =  {Proceedings of the Twenty-Second Annual IEEE Symposium on Logic in Computer Science (LICS 2007)},
    year =	 {2007},
    month =	 {July}, 
    pages =      {336--345},
    location =   {Wroclaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}

Last modified: 2022-10-3113:49
Sam Staton