Soundness, Structural Reductions, and Resource Extensions for Modal Workflow Nets
Author
Term
4. term
Education
Publication year
2016
Submitted on
2016-06-10
Pages
43
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