@inproceedings{e2795ce1db244078962ebfd84dd54f6e,

title = "Compositionality via Cut-Elimination: Hennessy-Milner Logic for an Arbitrary GSOS",

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.",

keywords = "Compositional proof systems, sequent calculus, cut- elimination, Hennessy-Milner logic, process algebra, GSOS systems",

author = "Alex Simpson",

year = "1995",

doi = "10.1109/LICS.1995.523276",

language = "English",

series = "LICS '95",

publisher = "Institute of Electrical and Electronics Engineers (IEEE)",

pages = "420--430",

booktitle = "Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science",

address = "United States",

}