Improvements in Explicit State Space Exploration for Colored Petri Nets
Term
4. term
Education
Publication year
2025
Submitted on
2025-06-12
Pages
32
Abstract
In model checking of colored Petri nets, the state of the art approach is to unfold colored nets into equivalent Petri nets. This allows the reuse of existing Petri net techniques but also adds additional overhead which in some cases is so large that unfolding within reasonable time is infeasible. Instead using an explicit state space exploration approach has shown promising results for reachability queries. In this thesis we extend the approach to include LTL queries as well as propose new optimisations and techniques, namely query simplification by over-approximation and using color constraints derived from the current state of the net when generating bindings. We implement these optimisations as an addition to the tool TAPAAL and experimentally test the performance on a dataset from the 2024 Model Checking Competition, an annual contest for tools in verifying properties for Petri nets. The experimental results indicate that both techniques are effective, as well as helping to solve different queries. The experiments for LTL queries show that our implementation overall performs significantly worse than the current unfolding approach but is able to find some unique answers. In the experiments for reachability queries, our implementation overall outperforms TAPAAL using unfolding answering 9% more queries. The improvement is especially significant for fireability queries as well as queries that can be solved by counter example.
Documents