Rozdział w tomie pokonferencyjnym
Brak miniatury
Licencja
CC-BYCC-BY - Uznanie autorstwa
 

Fast Termination and Workflow Nets

Uproszczony widok
cris.lastimport.scopus2024-02-12T20:08:52Z
dc.abstract.enPetri nets are an established model of concurrency. A Petri net is terminating if for every initial marking there is a uniform bound on the length of all possible runs. Recent work on the termination of Petri nets suggests that, in general, practical models should terminate fast, i.e. in polynomial time. In this paper we focus on the termination of workflow nets, an established variant of Petri nets used for modelling business processes. We partially confirm the intuition on fast termination by showing a dichotomy: workflow nets are either non-terminating or they terminate in linear time. The central problem for workflow nets is to verify a correctness notion called soundness. In this paper we are interested in generalised soundness which, unlike other variants of soundness, preserves desirable properties like composition. We prove that verifying generalised soundness is coNP-complete for terminating workflow nets. In general the problem is PSPACE-complete, thus intractable. We utilize insights from the coNP upper bound to implement a procedure for generalised soundness using MILP solvers. Our novel approach is a semi-procedure in general, but is complete on the rich class of terminating workflow nets, which contains around 90% of benchmarks in a widely-used benchmark suite. The previous state-of-the-art approach for the problem is a different semi-procedure which is complete on the incomparable class of so-called free-choice workflow nets, thus our implementation improves on and complements the state-of-the-art. Lastly, we analyse a variant of termination time that allows parallelism. This is a natural extension, as workflow nets are a concurrent model by design, but the prior termination time analysis assumes sequential behavior of the workflow net. The sequential and parallel termination times can be seen as upper and lower bounds on the time a process represented as a workflow net needs to be executed. In our experimental section we show that on some benchmarks the two bounds differ significantly, which agrees with the intuition that parallelism is inherent to workflow nets.
dc.affiliationUniwersytet Warszawski
dc.affiliation.departmentWydział Matematyki, Informatyki i Mechaniki
dc.affiliation.instituteInstytut Informatyki
dc.conference35th International Conference on Computer Aided Verification, CAV
dc.conference.countryFrancja
dc.conference.placeParyż
dc.conference.shortcutCAV 2023
dc.contributor.authorOfftermatt, Philip
dc.contributor.authorMazowiecki, Filip
dc.contributor.authorHofman, Piotr
dc.date.accessioned2024-01-25T00:32:02Z
dc.date.available2024-01-25T00:32:02Z
dc.date.copyright2023-07-17
dc.date.issued2023
dc.description.accesstimeAT_PUBLICATION
dc.description.additional35th International Conference, CAV 2023, Paris, France, July 17–22, 2023, Proceedings, Part I
dc.description.financePublikacja bezkosztowa
dc.description.versionFINAL_PUBLISHED
dc.identifier.bibliographicCitationHofman, P., Mazowiecki, F., Offtermatt, P. (2023). Fast Termination and Workflow Nets. In: Enea, C., Lal, A. (eds) Computer Aided Verification. CAV 2023. Lecture Notes in Computer Science, vol 13964. Springer, Cham. https://doi.org/10.1007/978-3-031-37706-8_7
dc.identifier.doi10.1007/978-3-031-37706-8_7
dc.identifier.eisbn978-3-031-37706-8
dc.identifier.isbn978-3-031-37705-1
dc.identifier.urihttps://repozytorium.uw.edu.pl//handle/item/107002
dc.identifier.weblinkhttps://link.springer.com/chapter/10.1007/978-3-031-37706-8_7
dc.languageen
dc.pbn.affiliationcomputer and information sciences
dc.publisher.ministerialSpringer
dc.relation.bookComputer Aided Verification, Part I: Automata and logic; concurrency; cyber-physical and hybrid systems; synthesis
dc.relation.pages132-155
dc.rightsCC-BY
dc.sciencecloudnosend
dc.titleFast Termination and Workflow Nets
dc.typeMonographChapterConference
dspace.entity.typePublication