Dissertation/Thesis Abstract

Comparison of encoding schemes for symbolic model checking of bounded petri nets
by Arora, Nishtha, M.S., Iowa State University, 2010, 83; 1479680
Abstract (Summary)

Petri nets are a graph based formalism used for modelling concurrent systems. Binary Decision Diagrams or Multi-Valued Decision Diagrams can be used in the analysis of systems modelled by Petri nets. An encoding scheme is required to be able to map the Petri net state to decision diagram values. Various encodings like One-hot scheme, Logarithmic scheme and Mdd scheme exist for this purpose. This thesis compares the performance of the existing encodings based on time and space taken to represent and analyze the system modelled as Petri net. It also introduces and compares a new encoding scheme called k-hot encoding and shows a gradual improvement in performance of the scheme with increasing values of k. The process of analyzing properties like deadlock and starvation is explained and a comparison is made between the encoding schemes based on the time taken by each to analyze these properties.

Indexing (document details)
Advisor: Miner, Andrew S.
Commitee: Basu, Samik, Lutz, Robyn
School: Iowa State University
Department: Computer Science
School Location: United States -- Iowa
Source: MAI 49/01M, Masters Abstracts International
Subjects: Computer science
Publication Number: 1479680
ISBN: 9781124152400
Copyright © 2019 ProQuest LLC. All rights reserved. Terms and Conditions Privacy Policy Cookie Policy