Compositionality via Cut-Elimination: Hennessy-Milner Logic for an Arbitrary GSOS

Alex Simpson

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We present a sequent calculus for proving that processes in a process algebra satisfy assertions in Hennessy-Milner logic. The main novelty lies in the use of the operational semantics to derive introduction rules (on the left and right of sequents) for the different operators of the process calculus. This gives a generic proof system applicable to any process algebra with an operational semantics specified in the GSOS format. We identify the desirable property of compositionality with cut-elimination, and we prove that this holds for a class of sequents. Further, we show that the proof system enjoys good completeness and omega- completeness properties relative to its intended model.
Original languageEnglish
Title of host publicationProceedings of the 10th Annual IEEE Symposium on Logic in Computer Science
Place of PublicationWashington, DC, USA
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Publication statusPublished - 1995

Publication series

NameLICS '95
PublisherIEEE Computer Society


  • Compositional proof systems, sequent calculus, cut- elimination, Hennessy-Milner logic, process algebra, GSOS systems


Dive into the research topics of 'Compositionality via Cut-Elimination: Hennessy-Milner Logic for an Arbitrary GSOS'. Together they form a unique fingerprint.

Cite this