Computer Science Department
School of Computer Science, Carnegie Mellon University


A Compositional Proof System for the Modal Mu-calculus and CCS

Sergey Berezin, Dilian Gurov*

January 1997

Keywords: Automatic verification, theorem proving, model mu-calculus, compositional model checking

We present a Compositional Proof System for the modal @g-calculus and a generalized version of the parallel composition in CCS. The proof system is designed for inferring global properties of a system from the local properties of its components. This allows for efficient verification of parallel processes by decomposing the task into smaller problems of verifying the parallel components separately. In particular, the system can be used to combine model checking with theorem proving. Since parallel composition causes the largest blow-up in the number of states, this technique proposes an effective solution to the state space explosion problem. The Proof System is implemented in PVS theorem prover, and the proof of its soundness was thoroughly checked using PVS logic as a metalanguage. The proof strategy mechanism of PVS can be used to achieve some degree of automation in a proof search.

19 pages

*Department of Computer Science, University of Victoria,

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by