Bidirectional Symbolic Reachability Analysis for Bounded Petri Nets using BDDs
Authors
Joensen, Niklas Egebak ; Rasmussen, Frederik Flemming Kærup ; Terp, Jonas Nagstrup
Term
4. term
Education
Publication year
2026
Submitted on
2026-06-03
Pages
36
Abstract
This thesis investigates whether bidirectional search techniques from planning can be applied to symbolic model checking of bounded Petri nets. It develops a comprehensive Boolean encoding of markings, transition relations, and linear arithmetic together with a propositional language, all compiled into Binary Decision Diagrams (BDDs). On this foundation, three state-space exploration algorithms are defined: a forward search from the initial marking, a backward search from the set of markings satisfying a target proposition, and a bidirectional variant combining both directions. Correctness is addressed by identifying markings that could lead to unrepresentable states and checking whether any such markings are reachable. The approach is evaluated by comparing the forward exploration to TINA tedd on models from the 2025 Model Checking Competition and by testing all three methods against TAPAAL in the reachability and cardinality categories. Findings indicate promise alongside limitations: the bidirectional method exhibits a fundamental weakness when the bound is unknown, often degenerating into a much slower forward search. Potential improvements include optimizing computational steps, introducing memoization, and experimenting with advanced variable reordering algorithms.
Afhandlingen undersøger, om tovejs-søgemetoder fra planlægningsområdet kan anvendes i symbolsk modeltjek af begrænsede Petri-net. Arbejdet udvikler en samlet boolesk kodning af markeringer, transitionsrelationer og lineære aritmetiske udtryk samt et propositionalt sprog, der alle oversættes til binære beslutningsdiagrammer (BDD’er). På denne basis konstrueres tre tilstandsrumsalgoritmer: en fremadrettet søgning fra den initiale markering, en bagudrettet søgning fra de markeringer, der opfylder en målproposition, og en tovejs-tilgang, der kombinerer begge retninger. Korrekthed behandles ved at identificere markeringer, som kan føre til ikke-repræsenterbare tilstande, og kontrollere, om sådanne findes blandt de nåelige markeringer. Metoderne evalueres ved at sammenligne den fremadrettede udforskning med TINA tedd på modeller fra Model Checking Competition 2025 og ved at teste alle tre tilgange mod TAPAAL i reachability- og cardinality-kategorierne. Resultaterne peger på potentiale, men også begrænsninger: især har tovejs-tilgangen en grundlæggende svaghed, når nettes bound er ukendt, hvor søgningen ofte degenererer til en langsommere fremadrettet metode. Mulige forbedringer inkluderer optimering af beregningstrin, udnyttelse af memoization og afprøvning af avancerede algoritmer til variabel-omordning.
[This apstract has been generated with the help of AI directly from the project full text]
Keywords
Model checking ; TAPAAL ; Petri net ; BDD