Symbolic Graphs: Linear Solutions to Connectivity Related Problems |
| |
Authors: | Raffaella Gentilini Carla Piazza Alberto Policriti |
| |
Affiliation: | (1) Università di Udine (DIMI), Via Le Scienze 206, 33100 Udine, Italy;(2) Department of Computer Science Reactive Systems Group, Kaiserslautern University, Kaiserslautern, Germany;(3) Institute of Applied Geonomics, Odine, Italy |
| |
Abstract: | The importance of symbolic data structures such as Ordered Binary Decision Diagrams (OBDD) is rapidly growing in many areas
of Computer Science where the large dimensions of the input models is a challenging feature: OBDD based graph representations
allowed to define truly new standards in the achievable dimensions for the Model Checking verification technique. However,
OBDD representations pose strict constraints in the algorithm design issue. For example, Depth-First Search (DFS) is not feasible
in a symbolic framework and, consequently, many state-of-the-art DFS based algorithms (e.g., connectivity procedures) cannot
be easily rearranged to work on symbolically represented graphs. We devise here a symbolic algorithmic strategy, based on
the new notion of spine-set, that is general enough to be the engine of linear symbolic step algorithms for both strongly connected components and biconnected
components. Our procedures improve on previously designed connectivity symbolic algorithms. Moreover, by an application to
the so-called “bad cycle detection problem”, our technique can be used to efficiently solve the emptiness problem for various
kinds of ω-automata.
This work is a revised and extended version of 22,23]. It is partially supported by the projects PRIN 2005015491 and BIOCHECK. |
| |
Keywords: | Strongly connected components Biconnected components Ordered binary decision diagrams Model checking Massive graphs |
本文献已被 SpringerLink 等数据库收录! |
|