Improvements in Explicit State Space Exploration for Colored Petri Nets
Authors
Pedersen, Kira Stæhr ; Brandt, Emil Normann ; Højriis, Jens Emil Fink
Term
4. term
Education
Publication year
2025
Submitted on
2025-06-12
Pages
32
Abstract
Petri nets model systems where many parts act at the same time. In colored Petri nets, tokens carry data (“colors”), allowing richer system descriptions. Model checking asks whether a system satisfies certain properties. The standard approach is to unfold colored nets into ordinary (uncolored) Petri nets so existing algorithms can be reused, but unfolding can blow up the model and become impractical. An alternative is explicit state-space exploration, which examines concrete states directly and has performed well for reachability (whether a particular state can be reached). In this thesis, we extend this approach to support LTL queries (Linear Temporal Logic, which expresses properties over sequences of states). We also propose two optimizations: (1) simplifying queries through over-approximation (a safe relaxation that can speed up checking), and (2) using color constraints derived from the current state when generating bindings (assignments) to narrow the search. We implemented these optimizations as an extension to the TAPAAL tool and evaluated performance on the 2024 Model Checking Competition dataset, an annual benchmark for Petri net verification tools. The results show that both techniques are effective and help with different query types. For LTL, our implementation performs overall worse than the unfolding-based approach but can find some unique answers. For reachability, our implementation outperforms TAPAAL with unfolding, answering 9% more queries. The gains are especially notable for fireability questions (whether a transition can fire) and for queries that can be decided by a counterexample.
Petri-net er modeller, der beskriver systemer med mange dele, der kører samtidig. I farvede Petri-net følger data ("farver") med tokens, så man kan udtrykke mere komplekse systemer. Modeltjek bruges til at afgøre, om et givent system opfylder bestemte egenskaber. Den mest brugte metode er at udfolde farvede net til almindelige (ufarvede) Petri-net, så eksisterende algoritmer kan genbruges. Udfoldning kan dog skabe meget store modeller og blive så tidskrævende, at den ikke er praktisk. Et alternativ er eksplicit tilstandsrums-eksploration, hvor man undersøger de konkrete tilstande direkte. Denne tilgang har vist lovende resultater for nåbarhed (om en bestemt tilstand kan nås). I denne afhandling udvider vi tilgangen til også at håndtere LTL-forespørgsler (Lineær Temporal Logik, som beskriver egenskaber over sekvenser af tilstande). Vi foreslår desuden to nye optimeringer: (1) forenkling af forespørgsler via overapproksimation (en sikker forenkling, der kan gøre tjek hurtigere), og (2) udnyttelse af farvebegrænsninger afledt af nettes aktuelle tilstand, når vi genererer bindings (tildelinger), så søgningen indsnævres. Vi har implementeret disse optimeringer som et tilføjelsesmodul til værktøjet TAPAAL og testet ydeevnen på datasættet fra Model Checking Competition 2024, en årlig konkurrence for værktøjer til verifikation af Petri-net. Eksperimenterne viser, at begge teknikker er effektive og hjælper med forskellige typer forespørgsler. For LTL-forespørgsler er vores løsning samlet set dårligere end den nuværende udfoldningsbaserede tilgang, men den finder nogle unikke svar. For nåbarhed overgår vores løsning TAPAALs udfoldningsbaserede tilgang og besvarer 9% flere forespørgsler. Forbedringen er især tydelig for spørgsmål om, hvorvidt en overgang kan affyres ("fireability"), samt for forespørgsler der kan afgøres via et modbevis (modeksempel).
[This apstract has been rewritten with the help of AI based on the project's original abstract]