5 papers · 1 filter
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…
The 5th Reactive Synthesis Competition (SYNTCOMP 2018): Benchmarks, Participants & Results
Swen Jacobs, Roderick Bloem, Maximilien Colange +11
We report on the fifth reactive synthesis competition (SYNTCOMP 2018). We introduce four new benchmark classes that have been added to the SYNTCOMP library, and briefly describe th…
Practical Synthesis of Reactive Systems from LTL Specifications via Parity Games
Michael Luttenberger, Philipp J. Meyer, Salomon Sickert
The synthesis of reactive systems from linear temporal logic (LTL) specifications is an important aspect in the design of reliable software and hardware. We present our adaption of…
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…
Computing the concurrency threshold of sound free-choice workflow nets
Philipp J. Meyer, Javier Esparza, Hagen Völzer
Workflow graphs extend classical flow charts with concurrent fork and join nodes. They constitute the core of business processing languages such as BPMN or UML Activity Diagrams. T…