Paper: A compositional proof system for the modal μ-calculus (at LICS 1994)
Authors: Henrik Reif Andersen Colin Stirling Glynn WinskelAbstract
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 Reif Andersen and Colin Stirling and Glynn Winskel}, title = {A compositional proof system for the modal μ-calculus}, booktitle = {Proceedings of the Ninth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1994}, year = 1994, editor = {Samson Abramsky}, month = {July}, pages = {144--153}, location = {Paris, France}, publisher = {IEEE Computer Society Press} }