4 papers
The complexity of soundness in workflow nets
Michael Blondin, Filip Mazowiecki, Philip Offtermatt
Workflow nets are a popular variant of Petri nets that allow for algorithmic formal analysis of business processes. The central decision problems concerning workflow nets deal with…
Continuous One-Counter Automata
Michael Blondin, Tim Leys, Filip Mazowiecki +2
We study the reachability problem for continuous one-counter automata, COCA for short. In such automata, transitions are guarded by upper and lower bound tests against the counter…
Directed Reachability for Infinite-State Systems
Michael Blondin, Christoph Haase, Philip Offtermatt
Numerous tasks in program analysis and synthesis reduce to deciding reachability in possibly infinite graphs such as those induced by Petri nets. However, the Petri net reachabilit…
Computing the Expected Execution Time of Probabilistic Workflow Nets
Philipp J. Meyer, Javier Esparza, Philip Offtermatt
Free-Choice Workflow Petri nets, also known as Workflow Graphs, are a popular model in Business Process Modeling. In this paper we introduce Timed Probabilistic Workflow Nets (TPWN…