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.
