Symbolic Representation of State Spaces

This lecture explores the concept of symbolic representation of state spaces using decision diagrams, focusing on high-level Petri nets. The instructor explains how to efficiently encode sets of vectors as products of domains, introduces decision diagrams, and discusses the benefits of using set decision diagrams over binary decision diagrams. The lecture also covers the clustering technique to split the computation of state spaces into separate processes and the partial net unfolding approach to handle unbounded algebras. Additionally, the instructor demonstrates the benchmark results of a model checker tool, Alpina, for reachability analysis of algebraic Petri nets, highlighting the tool's performance in handling concurrency and non-deterministic systems.