Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Sequent-calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS
Authors: Alexander Simpson
Date: 2004
Publication Title:Journal of Logic and Algebraic Programming
Publication Type:Journal Article Publication Status:Published
Volume No:60-61 Page Nos:287-322
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 from 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 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 omega-completeness result, relative to the ``intended'' model of closed process terms, follows.
Links To Paper
No links available
Bibtex format
author = { Alexander Simpson },
title = {Sequent-calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS},
journal = {Journal of Logic and Algebraic Programming},
year = 2004,
volume = {60-61},
pages = {287-322},
doi = {10.1016/j.jlap.2004.03.004},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh