Symmetry and Reduced Symmetry in Model-checking

Patrice Godefroid, A. Prasad Sistla

To appear at 13th Conference on Computer-Aided Verification (CAV01), Paris, France, 18-22 July 2001


Abstract

The paper presents symmetry based methods for model-checking systems that exhibit less symmetry or no symmetry. Guarded Annotated Quotient Structures (GQS) are introduced for verification of such systems. New techniques based on formula decomposition and sub-formula tracking are presented. These techniques are employed with GQS for efficient model-checking.


Server START Conference Manager
Update Time 28 Mar 2001 at 08:36:01
Maintainer www-cav01@lsv.ens-cachan.fr.
Start Conference Manager
Conference Systems