Lics

IEEE Symposium on Logic in Computer Science

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

Tenth Annual IEEE Symposium on

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 Symposium on Logic in Computer Science (LICS 1995)},
    year =	 {1995},
    month =	 {June}, 
    pages =      {420--430},
    location =   {San Diego, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2017-04-0512:37
Andrzej Murawski