ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Tue 9 Apr 2019 17:30 - 18:00 at SUN I - Model Checking Chair(s): Florian Zuleger

Dependency graph, invented by Liu and Smolka in 1998, is an oriented graph with hyper-edges that represent causal dependencies among its vertices. Numerous model checking problems are reducible to a computation of the minimum fixed-point vertex assignment. Recent works successfully extended the assignments in dependency graphs from the Boolean domain into more general structures in order to speed up the fixed-point computation or to apply the formalism to a more general setting of e.g. weighted logics. All these extensions require separate cor- rectness proofs of the fixed-point algorithm as well as a one-purpose im- plementation, even though many of the common ideas are shared across the different application domains. We suggest the notion of abstract de- pendency graphs where the vertex assignment is defined over an abstract algebraic structure based on well-founded Noetherian partial orders. We show that the existing approaches are concrete instances of our general framework and provide an optimised open-source C++ library that im- plements the abstract algorithm. We demonstrate that the performance of our generic implementation is comparable to, and sometimes even outperforms, dedicated special-purpose algorithms presented in the lit- erature.