Loading...
Please wait, while we are loading the content...
Similar Documents
Graph Algorithms for Massive Data-Sets
| Content Provider | Semantic Scholar |
|---|---|
| Author | Raffaella, Gentilini |
| Copyright Year | 2005 |
| Abstract | In this dissertation we face a number of fundamental graph problems which, on the one hand, share applications to the state explosion problem in model checking, and, on the other hand, pose interesting algorithmic questions when very large graphs are dealt with. In more detail, this thesis is divided into three main parts. Part I (Symbolic Graph Algorithms) deals with the algorithmic solution of fundamental graph problems (especially graph connectivity problems) assuming a symbolic OBDD-based graph representation. Working on symbolically represented data has potential: the standards achieved in graph sizes (playing a crucial role, for example, in verification, VLSI design, and CAD) are definitely higher. On the other hand, symbolic algorithm's design generates constraints as well. For example, Depth First Search is not feasible in the symbolic setting and our approach suggests a symbolic framework to tackle those problems which, in the standard case, are naturally solved by a DFS-based algorithm. Part II (Equivalence Based Graph Reduction) deals with well known bisimulation and simulation graph reductions. In particular, our purpose is to show a fil rouge connecting such notions, which consists in casting them into partition refinement problems (coarsest partition problems). Such a formulation is well known to be the engine of efficient computational strategies for bisimulation. In this thesis, we extend the picture to the, computationally more challenging, notion of simulation. Besides (we hope) a deeper understanding of the algebraic nature of simulation equivalence, the final byproduct is the definition of a new space efficient simulation algorithm refining a partition rather than a relation. Part III discusses some applications to model checking and builds connecting bridges among the material introduced in the first two parts of the dissertation. In particular, the strongly connected components symbolic algorithm defined in Part I is used to obtain a symbolic version of an efficient rank -based bisimulation reduction, recently defined in [39]. Finally, our symbolic procedure for strongly connected components turns out to be the key to cut down from O(V log V ) to O(V ) the number symbolic steps necessary to perform a number of tasks in model checking as bad cycle detection and Büchi as well as Streett automata language emptiness problems. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://es.cs.uni-kl.de/publications/datarsg/Gent04.pdf |
| Alternate Webpage(s) | http://www.dimi.uniud.it/phd/computer-science/la-ricerca/dottorato/informatica/cs2005-03-gentilini.pdf |
| Alternate Webpage(s) | http://91-641.wiki.uml.edu/file/view/cs2005-Graph+Algorithms+for+Massive+Data-Sets-gentilini.pdf/199590298/cs2005-Graph%20Algorithms%20for%20Massive%20Data-Sets-gentilini.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
