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.
My Menu
Saved Items

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)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.107 • Server: mpweb03
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)