The main contribution of Liu and Smolka is a linear-time, on-the-fly algorithm to find such a minimum stable assignment. The computation problem is to find a point-wise minimal assignment of vertices to the Boolean values 0 and 1 such that the assignment is stable: whenever there is a hyperedge where all children have the value 1 then also the father of the hyperedge has the value 1. Most recently, the DG approach to CTL model checking of Petri nets , implemented in the model checker TAPAAL , won the gold medal at the annual Model Checking Contest 2018 .Ī DG consists of a finite set of vertices and a finite set of hyperedges that connect a vertex to a number of children vertices. The DG approach offers a general and often performance-optimal way to solve these problem. checking behavioural equivalences between systems, model checking systems with respect to temporal logical properties , as well as synthesizing missing components of systems .
#Dependency graph online verification
We demonstrate that the performance of our generic implementation is comparable to, and sometimes even outperforms, dedicated special-purpose algorithms presented in the literature.ĭependency Graphs (DG) have demonstrated a wide applicability with respect to verification and synthesis of reactive systems, e.g. We show that existing approaches are concrete instances of our general framework and provide an open-source C++ library that implements the abstract algorithm. We suggest the notion of abstract dependency graphs where the vertex assignment is defined over an abstract algebraic structure of Noetherian partial orders with the least element. All these extensions require separate correctness proofs of the fixed-point algorithm as well as a one-purpose implementation. Recent works successfully extended the assignments in dependency graphs from the Boolean domain into more general domains in order to speed up the fixed-point computation or to apply the formalism to a more general setting of e.g.
Numerous model checking problems are reducible to a computation of the minimum fixed-point vertex assignment.
#Dependency graph online series
Book series (LNCS, volume 11427) Abstractĭependency graphs, invented by Liu and Smolka in 1998, are oriented graphs with hyperedges that represent dependencies among the values of the vertices.
0 kommentar(er)
