Logic in Computer Science (LICS 1995)

Paper: Compositionality via Cut-Elimination: Hennessy-Milner Logic for an Arbitrary GSOS (at LICS 1995)

Authors: Alex K. Simpson

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.

BibTeX

  @InProceedings{Simpson-Compositionalityvia,
    author = 	 {Alex K. Simpson},
    title = 	 {Compositionality via Cut-Elimination: Hennessy-Milner Logic for an Arbitrary GSOS},
    booktitle =  {Proceedings of the Tenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1995},
    year =	 1995,
    editor =	 {Dexter Kozen},
    month =	 {June}, 
    pages =      {420-430},
    location =   {San Diego, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }