TAPAAL SMC: Statistical Model Checking of Stochastic Timed-Arc Petri Nets
2026-06-01 • Distributed, Parallel, and Cluster Computing
Distributed, Parallel, and Cluster Computing
AI summaryⓘ
The authors extended a tool called Timed-Arc Petri Nets (TAPN), which helps model systems where timing and conditions matter, by adding a way to include randomness or chance (stochastic behavior). They developed new methods to check these models using statistical tests to see if certain properties hold, and implemented these methods in a software tool called TAPAAL. The authors also explained why they designed the random behavior the way they did and proved that it works well. They tested their approach on real-world examples to show it can be used effectively.
Timed-Arc Petri Netstokenstransition firingplace invariantsinhibitor arcstransport arcsstochastic semanticsstatistical model checkingTAPAALmodel verification
Authors
Tanguy Dubois, Kim G. Larsen, Jiri Srba
Abstract
Timed-Arc Petri net (TAPN) is a timed extension of the classical Petri net model where tokens have their age and input arcs are associated with time intervals restricting the ages of tokens available for transition firing. Additionally, a TAPN can also contain place invariants constraining the ages of tokens in places, inhibitor arcs preventing a transition from firing and transport arcs that preserve token ages upon firing. This set of features, as much as it allows us to model complex systems, also often makes verification problems computationally hard or even undecidable. Moreover, in order to model real-life examples, additional stochastic aspects are often necessary to capture the desired behaviour. We suggest the first stochastic semantics for TAPNs and design and implement the quantitative and qualitative Statistical Model Checking (SMC) algorithms in the model checker TAPAAL. We argue for the semantic choices we made in the stochastic semantics and prove that the semantics is well-behaving. On a number of case studies we demonstrate the practical applicability of our modelling formalism and its SMC implementation.