Please use this identifier to cite or link to this item:
Title: Enhancing State Space Reduction Methods for Model Checking
Keywords: Model Checking, Symmetry Reduction, Partial Order Reduction, Fairness, Linearizability, Symmetry Detection
Issue Date: 23-Jan-2013
Citation: ZHANG SHAOJIE (2013-01-23). Enhancing State Space Reduction Methods for Model Checking. ScholarBank@NUS Repository.
Abstract: The applicability of model checking is often limited by the state space explosion problem. A variety of approaches have emerged to ameliorate this problem over years. However, basic reduction techniques generally do not take into account more sophisticated techniques. Therefore, in this thesis, we first study the problem in the context of model checking liveness properties with global fairness assumption. We prove that symmetry reduction and global fairness can be integrated without extra effort, and partial order reduction is not property preserving with global fairness. Second, we investigate the problem in the context of checking linearizability. We combine symmetry reduction and partial order reduction, which has never been explored before in refinement checking setting, to achieve maximum reduction. A fundamental yet often overlooked step for symmetry reduction is to obtain correct and sufficient knowledge of symmetries that can be exploited during model checking. We present a novel symmetry detection approach. It works for general concurrent systems and is able to detect various symmetries in a fully automatic way.
Appears in Collections:Ph.D Theses (Open)

Show full item record
Files in This Item:
File Description SizeFormatAccess SettingsVersion 
ZhangSJ.pdf764.08 kBAdobe PDF



Page view(s)

checked on May 11, 2019


checked on May 11, 2019

Google ScholarTM


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.