Soundness, Structural Reductions, and Resource Extensions for Modal Workflow Nets
Author
Harbo, Jacob Buchreitz
Term
4. term
Education
Publication year
2016
Pages
43
Abstract
Vi introducerer modale workflow-net, en ny måde at modellere arbejdsgange på, som kombinerer modalitet fra modale transitionssystemer (der skelner mellem påkrævet og tilladt adfærd) med Petrinet-baserede arbejdsgangsmodeller. Vi viser, at det er PSPACE-komplet at afgøre soundness, dvs. om processer kan afsluttes korrekt, for disse net. For at dæmpe tilstandseksplosionen ved analyse af sådanne modeller giver vi strukturelle reduktioner, der bevarer soundness og dermed gør analyserne mere håndterbare. Vi udvider også modellen med ressourcer og viser, at de sædvanlige begreber soundness og boundedness (begrænsethed) er utilstrækkelige i den sammenhæng. Derfor introducerer vi strengere varianter, infinitær soundness og infinitær K-begrænsethed, tilpasset modale workflows med ressourcer. Endelig beviser vi, at infinitær soundness er afgørlig i PSPACE for net, der er infinitært K-begrænsede.
We introduce modal workflow nets, a new way to model workflows that combines modality from modal transition systems (to distinguish required and allowed behavior) with Petri net–based workflow models. We show that deciding soundness—whether processes can complete correctly—for these nets is PSPACE-complete. To mitigate the state-explosion that occurs during analysis, we provide structural reductions that preserve soundness and make verification more manageable. We further extend the model with resources and show that the conventional notions of soundness and boundedness are too weak in this setting. We therefore define stricter notions, called infinitary soundness and infinitary K-boundedness, tailored to modal workflows with resources. Finally, we prove that infinitary soundness is decidable in PSPACE for nets that are infinitary K-bounded.
[This abstract was generated with the help of AI]
Keywords
Documents