Decision diagrams: Extensions and applications to reachability analysis
Date
Authors
Major Professor
Advisor
Committee Member
Journal Title
Journal ISSN
Volume Title
Publisher
Authors
Research Projects
Organizational Units
Journal Issue
Is Version Of
Versions
Series
Department
Abstract
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.