A master thesis from Aalborg University
Improvements in Explicit State Space Exploration for Colored Petri Nets
Author(s)
Term
4. term
Education
Publication year
2025
Submitted on
2025-06-12
Pages
32 pages
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
Colophon: This page is part of the AAU Student Projects portal, which is run by Aalborg University. Here, you can find and download publicly available bachelor's theses and master's projects from across the university dating from 2008 onwards. Student projects from before 2008 are available in printed form at Aalborg University Library.
If you have any questions about AAU Student Projects or the research registration, dissemination and analysis at Aalborg University, please feel free to contact the VBN team. You can also find more information in the AAU Student Projects FAQs.