4 papers · 1 filter
Verifying linear temporal specifications of constant-rate multi-mode systems
Michael Blondin, Philip Offtermatt, Alex Sansfaçon-Buchanan
Constant-rate multi-mode systems (MMS) are hybrid systems with finitely many modes and real-valued variables that evolve over continuous time according to mode-specific constant ra…
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…
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…