Simpson's Proof Systems for Process Verification: A Fine-tuning (short paper)

We refine Alex Simpson’s approach to formal verification of properties of concurrent systems via proof systems. Our new sequent calculus G3HMLGSOS seamlessly harmonises the GSOS semantics for process calculi (for system formalisation) with Hennessy-Milner logic (for formal property specification) in a pure G3-style system, from which the cut-rule is effectively eliminated. We achieve this substantial improvement by applying the geometrisation of formal theories introduced in the proof-theoretic literature by Roy Dyckhoff and Sara Negri. We communicate here our design methodology to fine-tune Simpson’s calculi, which we consider promising to cover, in the future, more expressive process algebra’s specification formalisms and logics in a principled and uniform manner.