Induction and Model Checking



This chapter deals with the verification of systems that are generated out of similar or identical finite state components, using a simple rule. Systems of this type are commonplace — they occur in bus protocols and network protocols, I/O channels, and many other structures that are designed to be extensible by adding similar components. In particular, we are interested in verifying properties that hold independent of the number of components in the system. We may for example have used a model checker to verify some property of a multiprocessor with a fixed number of processors. Would that property continue to hold if we added one more processor. One hundred? One thousand? Clearly, at some point we will be unable to answer the question with the model checker alone. It would be far preferable to settle the question once and for all, regardless of the number of processors.


Model Check Atomic Proposition Kripke Model Induction Rule Simulation Relation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer Science+Business Media New York 1993

Authors and Affiliations

  1. 1.Carnegie Mellon UniversityAustralia

Personalised recommendations