Logic in Computer Science (LICS 1995)

Paper: Partial Model Checking (at LICS 1995)

Authors: Henrik Reif Andersen

Abstract

A major obstacle in applying finite-state model checking to the verification of large systems is the combinatorial explosion of the state space arising when many loosely coupled parallel processes are considered. The problem also known as the *state- explosion problem* has been attacked from various sides. This paper presents a new approach based on *partial model checking*: Parts of the concurrent system are gradually removed while transforming the specification accordingly. When the intermediate specifications constructed in this manner can be kept small, the state-explosion problem is avoided. Experimental results with a prototype implemented in Standard ML, shows that for Milner's Scheduler - an often used benchmark - this approach improves on the published results on Binary Decision Diagrams and is comparable to results obtained using generalized Decision Diagrams. Specifications are expressed in a variant of the modal mu- calculus.

BibTeX

  @InProceedings{Andersen-PartialModelCheckin,
    author = 	 {Henrik Reif Andersen},
    title = 	 {Partial Model Checking},
    booktitle =  {Proceedings of the Tenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1995},
    year =	 1995,
    editor =	 {Dexter Kozen},
    month =	 {June}, 
    pages =      {398-406},
    location =   {San Diego, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }