Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
Symmetry and Reduced Symmetry in Model Checking?
| |
|
Symmetry and Reduced Symmetry in Model Checking?
A. Prasad Sistla6 and Patrice Godefroid7
| (6) |
Department of Electrical Engineering and Computer Science, University of Illinois at Chicago, Chicago, IL 60607, USA |
| (7) |
Bell Laboratories, Lucent Technologies, Naperville, IL 50566, USA |
Abstract
Symmetry reduction methods exploit symmetry in a system in order to efficiently verify its temporal properties. Two problems
may prevent the use of symmetry reduction in practice: (1) the property to be checked may distinguish symmetric states and
hence not be preserved by the symmetry, and (2) the system may exhibit little or no symmetry. In this paper, we present a
general framework that addresses both of these problems.We introduce “Guarded Annotated Quotient Structures” for compactly
representing the state space of systems even when those are asymmetric. We then present algorithms for checking any temporal
property on such representations, including non-symmetric properties.
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|