Compositional Proof System for the Modal micro-calculus and CCS

摘要

We present a Compositional Proof System for the modal micro-calculus and ageneralized version of the parallel composition in CCS 11Gamma12. 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 gamma, this technique proposes an effective solution to the state space explosion problem. The Proof System is implemented in PVS theorem prover 13gamma and the proof of its soundness was thoroughly checked using PVS logic as a meta-language. The proof strategy mechanism of PVS can be used to achieve some degree of automation in a proof search.