Sequent Calculi for Process Verification: Hennessy-Milner Logic for an Arbitrary GSOS

Alexander Simpson

Research output: Contribution to journalArticlepeer-review

Abstract

We argue that, by supporting a mixture of "compositional" and "structural" styles of proof, sequent-based proof systems provide a useful framework for the formal verification of processes. As a worked example, we present a sequent calculus for establishing that processes 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 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. Using a general algebraic notion of GSOS model, we prove a completeness theorem for the cut-free fragment of the proof system, thereby establishing the admissibility of the cut rule. Under mild (and necessary) conditions on the process algebra, an ω-completeness result, relative to the "intended" model of closed process terms, follows.
Original languageEnglish
Pages (from-to)287-322
Number of pages35
JournalJournal of Logic and Algebraic Programming
Volume60-61
DOIs
Publication statusPublished - 2004

Fingerprint

Dive into the research topics of 'Sequent Calculi for Process Verification: Hennessy-Milner Logic for an Arbitrary GSOS'. Together they form a unique fingerprint.

Cite this