Implicit Relations for Symbolic State Space Generation
In the modern-day, the ever-growing dependence on information and communication technology has led to the development of a vast number of critical applications. Despite fast-paced production and the increasing complexity of systems, the expectation of building low-defect systems is inevitable. Symbolic model checking, one of the many system verification techniques, checks every state of the system against good and bad properties to assist in building a low-defect system and requires the entire state space of the system. Saturation, a symbolic state-space generation algorithm that works faster than most explicit techniques, traditionally uses decision diagrams for encoding systems and their reachability set. While decision diagrams compactly represent large sets of state, they cause significant overhead to saturation algorithm when used for representing system events.
In this thesis, we explore and build alternative novel data structures, “implicit relations” that are both compatible and efficient with saturation, for representing system events. Implicit relations are useful in representing Kronecker-consistent systems. We further the work through “hybrid relations” to include representation of the generic class of systems that can be modeled using extended Petri nets formalism. Experiments suggest that these representations are efficient compared to decision diagram based structures in terms of both time & memory, and are comparable to state-of-the-art methods.
Committee: Andrew Miner (major professor), Samik Basu, Gianfranco Ciardo, Robyn Lutz, and Wallapak Tavanapong
WebEx Meeting link: https://iastate.webex.com/iastate/j.php?MTID=m6fea0dbd58d12561e2068bffeb08a0a4
Meeting number: 120 672 6144
Password: bPspTUmk444