Please use this identifier to cite or link to this item: http://scholarbank.nus.edu.sg/handle/10635/38797
Title: Enhancing State Space Reduction Methods for Model Checking
Authors: ZHANG SHAOJIE
Keywords: Model Checking, Symmetry Reduction, Partial Order Reduction, Fairness, Linearizability, Symmetry Detection
Issue Date: 23-Jan-2013
Source: 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.
URI: http://scholarbank.nus.edu.sg/handle/10635/38797
Appears in Collections:Ph.D Theses (Open)

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

OPEN

NoneView/Download

Page view(s)

142
checked on Dec 11, 2017

Download(s)

220
checked on Dec 11, 2017

Google ScholarTM

Check


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