Efficient state space exploration of a concurrent program is a fundamental problem in algorithmic verification because of the known state explosion problem. In the past decades, dynamic partial order reductions and Petri net unfoldings have been two promising approaches to address the state explosion problem. However, these techniques typically focus on the combinatorial explosion caused by the potential linearizations of partial orders and do not generally address multiple ...