Date of Award
Doctor of Philosophy
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.
Babar, Junaid, "Decision diagrams: Extensions and applications to reachability analysis" (2019). Graduate Theses and Dissertations. 17393.