|
CMU-CS-97-105
Computer Science Department
School of Computer Science, Carnegie Mellon University
CMU-CS-97-105
A Compositional Proof System for the Modal Mu-calculus and CCS
Sergey Berezin, Dilian Gurov*
January 1997
CMU-CS-97-105.ps
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, dgurov@csr.uvic.ca
|