Symbolic Unfoldings of High-level Petri Nets

Kurzfassung

Unfoldings are a well known partial-order semantics of P/T (low-level) Petri nets that can be applied to various model checking or verification problems. For colored (high-level) Petri nets, the so-called symbolic unfolding generalizes this notion. A finite complete prefix of a P/T Petri net's unfolding contains all information to verify, e.g., reachability of markings. Würdemann et. al. unite these two concepts and define finite complete prefixes of the symbolic unfolding of colored Petri nets. We evaluate this extended algorithm through a prototype implementation on four novel benchmark families. We find that our approach is effective and is applicable for a class of nets where previous unfolding based approaches are cannot be applied.