A Compositional Proof System for the Modal micro-calculas and CCS

Abstract

We present a Compositional Proof System for the modal mu-calculus and a generalized 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 gamma the system can be used to combine model checking 6 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 metalanguage. The proof strategy mechanism of PVS can be used to achieve some degree of automation in a proof search.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 15, 1997
Accession Number
ADA342066

Entities

People

  • Diliant Gurov
  • Sergey Berezin

Organizations

  • Carnegie Mellon University

Tags

DTIC Thesaurus Topics

  • Calculus
  • Classification
  • Complex Systems
  • Computer Science
  • Computers
  • Language
  • Notation
  • Point Theorem
  • Semantics
  • Specifications
  • Standards
  • Symbols
  • Universities
  • Verification

Fields of Study

  • Computer science

Readers

  • Analytical Mechanics
  • Computational Linguistics
  • Parallel and Distributed Computing.

Technology Areas

  • AI & ML
  • AI & ML - Bayesian Inference
  • AI & ML - Machine Learning Algorithms
  • Space