Theses and Dissertations

Issuing Body

Mississippi State University

Advisor

Hansen, Eric

Committee Member

Reese, Donna S.

Committee Member

Allen, Edward B.

Committee Member

Abdelwahed, Sherif

Committee Member

Bridges, Susan M.

Date of Degree

5-17-2014

Document Type

Dissertation - Open Access

Major

Computer Science

Degree Name

Doctor of Philosophy (Ph.D)

College

James Worth Bagley College of Engineering

Department

Department of Computer Science and Engineering

Abstract

Model checking problems suffer from state space explosion. State space explosion is the number of states in the graph increases exponentially with the number of variables in the state description. Searching the large graphs required in model checking requires an efficient algorithm. This dissertation explores several methods to improve an externalmemory search algorithm for model checking problems. A tool implementing these methods is built on top of the Murphi model checker. One improvement is a state cache for immediate detection leveraging the properties of state locality. A novel type of locality, intralayer locality is explained and shown to exist in a variety of search spaces. Another improvement, partial delayed duplicate detection, exploits interlayer locality to reduce search times. An automatic partitioning function is described that allows hash-based delayed duplicate detection to be used without domain knowledge of the state space. A phased delayed duplicate detection algorithm combining features of hash-based delayed duplicate detection and sorting-based delayed duplicate detection is explained and compared to the other methods.

URI

https://hdl.handle.net/11668/17740

Download

Share

COinS