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

Alex Simpson

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

Abstract

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)
Pages420-430
DOIs
Publication statusPublished - 1995

Publication series

NameLICS '95
PublisherIEEE Computer Society

Keywords

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

Fingerprint

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