Comparison of encoding schemes for symbolic model checking of bounded petri nets

Thumbnail Image
Date
2010-01-01
Authors
Arora, Nishtha
Major Professor
Advisor
Andrew Miner
Committee Member
Journal Title
Journal ISSN
Volume Title
Publisher
Altmetrics
Abstract

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.

Series Number
Journal Issue
Is Version Of
Versions
Series
Academic or Administrative Unit
Type
thesis
Comments
Rights Statement
Copyright
Fri Jan 01 00:00:00 UTC 2010
Funding
Subject Categories
Supplemental Resources
Source