A master thesis from Aalborg University
Soundness, Structural Reductions, and Resource Extensions for Modal Workflow Nets
Author(s)
Term
4. term
Education
Publication year
2016
Submitted on
2016-06-10
Pages
43 pages
Abstract
We study a specification formalism which combines modality, as known from modal transition systems, with Petri net-based workflows to create a new way of modelling workflows which we call modal workflow nets, and prove that deciding soundness for these modal workflow nets is PSPACE-complete. To combat the state-explosion problem in modal workflow nets we define a set of structural reductions which preserve soundness. We also extend the model with resources and show that conventional concepts of soundness and boundedness are insufficient when discussing modal workflows with resources, and we introduce stricter versions of both which we call infinitary soundness and infinitary K-boundedness. Finally, we prove that infinitary soundness is decidable in PSPACE for infinitary K-bounded nets.
Keywords
Documents
Colophon: This page is part of the AAU Student Projects portal, which is run by Aalborg University. Here, you can find and download publicly available bachelor's theses and master's projects from across the university dating from 2008 onwards. Student projects from before 2008 are available in printed form at Aalborg University Library.
If you have any questions about AAU Student Projects or the research registration, dissemination and analysis at Aalborg University, please feel free to contact the VBN team. You can also find more information in the AAU Student Projects FAQs.