## Paper: A compositional proof system for the modal μ-calculus (at LICS 1994)

**Henrik R. Andersen Colin Stirling Glynn Winskel**

### Abstract

We present a proof system for determining satisfaction between processes in a fairly general process algebra and assertions of the modal μ-calculus. The proof system is compositional in the structure of processes. It extends earlier work on compositional reasoning within the modal μ-calculus and combines it with techniques from work on local model checking. The proof system is sound for all processes and complete for a class of finite-state processes

### BibTeX

@InProceedings{AndersenStirlingWin-Acompositionalproof, author = {Henrik R. Andersen and Colin Stirling and Glynn Winskel}, title = {A compositional proof system for the modal μ-calculus}, booktitle = {Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science (LICS 1994)}, year = {1994}, month = {July}, pages = {144--153}, location = {Paris, France}, publisher = {IEEE Computer Society Press} }