4 papers · 1 filter
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…
Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling
Michael Blondin, Javier Esparza, Martin Helfrich +2
We present a sound and complete method for the verification of qualitative liveness properties of replicated systems under stochastic scheduling. These are systems consisting of a…
Automatic Analysis of Expected Termination Time for Population Protocols
Michael Blondin, Javier Esparza, Antonín Kučera
Population protocols are a formal model of sensor networks consisting of identical mobile devices. Two devices can interact and thereby change their states. Computations are infini…