
CMUCS97105
Computer Science Department
School of Computer Science, Carnegie Mellon University
CMUCS97105
A Compositional Proof System for the Modal Mucalculus and CCS
Sergey Berezin, Dilian Gurov*
January 1997
CMUCS97105.ps
Keywords: Automatic verification, theorem proving, model mucalculus,
compositional model checking
We present a Compositional Proof System for the modal @gcalculus
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
blowup 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, dgurov@csr.uvic.ca
