Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Tenth Annual IEEE Symposium on

Logic in Computer Science (LICS 1995)

Paper: Partial Model Checking (at LICS 1995)

Authors: Henrik R. 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 R. Andersen},
    title = 	 {Partial Model Checking},
    booktitle =  {Proceedings of the Tenth Annual IEEE Symposium on Logic in Computer Science (LICS 1995)},
    year =	 {1995},
    month =	 {June}, 
    pages =      {398--407},
    location =   {San Diego, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2017-04-0512:37
Andrzej Murawski