Analysis of Agent-Based Systems Using Decision Procedures
Abstract
In recent years, model checking has emerged as a remarkably effective technique for the automated analysis of descriptions of hardware systems and communication protocols. To analyze software system descriptions, however, a direct application of model checking rarely succeeds, since these descriptions often have huge (often infinite) state spaces that are not amenable to the finite-state methods of model checking. More important, the computation of a fixpoint (the hallmark of the model-checking approach) is not always needed in practice for the verification of an interesting class of properties, viz, properties that are invariantly true in all reachable states or transitions of the system. To establish a property as an invariant, an induction proof, suitably augmented with automatically generated lemmas, often suffices.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jul 01, 2001
- Accession Number
- ADA465305
Entities
People
- Ramesh Bharadwaj
Organizations
- United States Naval Research Laboratory