Abstract Dependency Graphs and Their Application to Model CheckingBest paper nomination
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.
Tue 9 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:30 - 18:00 | |||
16:30 30mTalk | VoxLogicA: a Spatial Model Checker for Declarative Image Analysis TACAS Link to publication | ||
17:00 30mTalk | On Reachability in Parameterized Phaser Programs TACAS Link to publication | ||
17:30 30mTalk | Abstract Dependency Graphs and Their Application to Model CheckingBest paper nomination TACAS Link to publication |