Degree Type


Date of Award


Degree Name

Doctor of Philosophy


Computer Science


Computer Science

First Advisor

Andrew S. Miner


Symbolic data structures and algorithms are increasingly popular tools for the analysis of complex systems. Given a high-level model of a system, such as a Petri Net, we can automatically verify certain properties about it. In this thesis, we develop data structures and techniques that can be used to improve such analyses.

First, we show how decision diagrams can be used efficiently in traditional explicit generation algorithms. Next, we show how symbolic reachability analysis can be used to detect deadlocks in Petri Nets. We also present a symbolic approach that can detect deadlocks in unbounded Petri Nets.

Finally, we introduce a new type of decision diagram, ESRBDD, that combines multiple reduction rules, is canonical, and produces a more compact representation than previous efforts. We show that operations on ESRBDDs are at least as efficient as those on the underlying decision diagrams and introduce extensions to ESRBDDs that improve on their compactness and operational efficiency.

Copyright Owner

Junaid Babar



File Format


File Size

168 pages

Available for download on Saturday, July 25, 2020