Refine
Document Type
- Doctoral thesis (1)
Has Fulltext
- yes (1)
Is part of the Bibliography
- no (1)
Year of publication
- 2009 (1)
Language
- English (1)
Keywords
- Symbolische Analyse (1) (remove)
Institute
The research in this thesis focuses on different techniques which can improve efficiency of the symbolic analysis of Petri nets. Reduced ordered interval decision diagrams (ROIDDs) are employed to encode sets of states of k-bounded nets. We discuss implementation of an ROIDD package and special ROIDD operations needed in symbolic algorithms. We study then how to improve efficiency of the reachability analysis and propose a new saturation approach, which exploits the structure of ROIDDs and the structure of k-bounded P/T nets. It manages to keep sizes of intermediate diagrams smaller than other approaches and can drastically improve efficiency of the symbolic analysis. Saturation techniques are applied in the enumeration of strongly connected components and in model checking. Implementation of symbolic model checkers for k-bounded P/T nets are discussed. We consider CTL and a novel LTL model checker. A number of techniques to improve efficiency of the implementation are considered.