arXiv subjects

Jiri Srba

Publications and source records attributed to Jiri Srba.

3 recordsLinked to original sources

arXiv2026

TAPAAL SMC: Statistical Model Checking of Stochastic Timed-Arc Petri Nets

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.

cs.DC↗

arXiv2023

Methods for Efficient Unfolding of Colored Petri Nets

Colored Petri nets offer a compact and user friendly representation of the traditional P/T nets and colored nets with finite color ranges can be unfolded into the underlying P/T nets, however, at the expense of an exponential explosion in size. We present two novel techniques based on static analysis in order to reduce the size of unfolded colored nets. The first method identifies colors that behave equivalently and groups them into equivalence classes, potentially reducing the number of used colors. The second method overapproximates the sets of colors that can appear in places and excludes colors that can never be present in a given place. Both methods are complementary and the combined approach allows us to significantly reduce the size of multiple colored Petri nets from the Model Checking Contest benchmark. We compare the performance of our unfolder with state-of-the-art techniques implemented in the tools MCC, Spike and ITS-Tools, and while our approach is competitive w.r.t. unfolding time, it also outperforms the existing approaches both in the size of unfolded nets as well as in the number of answered model checking queries from the 2021 Model Checking Contest.

cs.LO↗

arXiv2021

Learning Safe and Optimal Control Strategies for Storm Water Detention Ponds

Storm water detention ponds are used to manage the discharge of rainfall runoff from urban areas to nearby streams. Their purpose is to reduce the hydraulic impact and sediment loads of the receiving waters. Detention ponds are currently designed based on static controls: the output flow of a pond is capped at a fixed value. This is not optimal with respect to the current infrastructure capacity and for some detention ponds it might even violate current regulations set by the European Water Framework Directive. We apply formal methods to synthesize (i.e., derive automatically) a safe and optimal active controller. We model the storm water detention pond, including the urban catchment area and the rain forecasts, as a hybrid Markov decision process. Subsequently, we use the tool Uppaal Stratego to synthesize a control strategy minimizing the cost related to pollution (optimality) while guaranteeing no emergency overflow of the detention pond (safety). Simulation results for an existing pond show that Uppaal Stratego can learn optimal strategies that prevent emergency overflows, where the current static control is not always able to prevent it. At the same time, our approach can improve sedimentation during low rain periods.

eess.SY↗