Elimination of Detached Regions in Dependency Graph Verification.

The formalism of dependency graphs by Liu and Smolka is a well-established method for on-the-fly computation of fixed points over Boolean domains with numerous applications in e.g. model checking, game synthesis, bisimulation checking and others. The original Liu and Smolka on-the-fly algorithm runs in linear time, and several extensions and improvements to this algorithm have recently been studied, including the notion of negation edges, certain-zero early termination as well as extensions towards abstract dependency graphs. We present a novel improvement for computing the least fixed-point assignment on dependency graphs, with the goal of avoiding the exploration of detached subgraphs that cannot contribute to the assignment value of the root node. We also experimentally evaluate different ways of resolving nondeterminism in the algorithm and execute experiments on CTL formulae from the annual Petri net model checking contest as well as on synthesis problems for Petri games. We find out that our algorithm significantly improves the state-of-the-art.