期刊文献+

Answering Reachability Queries on Incrementally Updated Graphs by Hierarchical Labeling Schema 被引量:1

Answering Reachability Queries on Incrementally Updated Graphs by Hierarchical Labeling Schema
原文传递
导出
摘要 We proposed a novel solution schema called the Hierarchical Labeling Schema (HLS) to answer reachability queries in directed graphs. Different from many existing approaches that focus on static directed acyclic graphs (DAGs), our schema focuses on directed cyclic graphs (DCGs) where vertices or arcs could be added to a graph incrementally. Unlike many of the traditional approaches, HLS does not require the graph to be acyclic in constructing its index. Therefore, it could, in fact, be applied to both DAGs and DCGs. When vertices or arcs are added to a graph, the HLS is capable of updating the index incrementally instead of re-computing the index from the scratch each time, making it more efficient than many other approaches in the practice. The basic idea of HLS is to create a tree for each vertex in a graph and link the trees together so that whenever two vertices are given, we can immediately know whether there is a path between them by referring to the appropriate trees. We conducted extensive experiments on both real-world datasets and synthesized datasets. We compared the performance of HLS, in terms of index construction time, query processing time and space consumption, with two state-of-the-art methodologies, the path-tree method and the 3-hop method. We also conducted simulations to model the situation when a graph is updated incrementally. The performance comparison of different algorithms against HLS on static graphs has also been studied. Our results show that HLS is highly competitive in the practice and is particularly useful in the cases where the graphs are updated frequently. We proposed a novel solution schema called the Hierarchical Labeling Schema (HLS) to answer reachability queries in directed graphs. Different from many existing approaches that focus on static directed acyclic graphs (DAGs), our schema focuses on directed cyclic graphs (DCGs) where vertices or arcs could be added to a graph incrementally. Unlike many of the traditional approaches, HLS does not require the graph to be acyclic in constructing its index. Therefore, it could, in fact, be applied to both DAGs and DCGs. When vertices or arcs are added to a graph, the HLS is capable of updating the index incrementally instead of re-computing the index from the scratch each time, making it more efficient than many other approaches in the practice. The basic idea of HLS is to create a tree for each vertex in a graph and link the trees together so that whenever two vertices are given, we can immediately know whether there is a path between them by referring to the appropriate trees. We conducted extensive experiments on both real-world datasets and synthesized datasets. We compared the performance of HLS, in terms of index construction time, query processing time and space consumption, with two state-of-the-art methodologies, the path-tree method and the 3-hop method. We also conducted simulations to model the situation when a graph is updated incrementally. The performance comparison of different algorithms against HLS on static graphs has also been studied. Our results show that HLS is highly competitive in the practice and is particularly useful in the cases where the graphs are updated frequently.
作者 Tak-Lam Wong
出处 《Journal of Computer Science & Technology》 SCIE EI CSCD 2016年第2期381-399,共19页 计算机科学技术学报(英文版)
关键词 graph indexing reachability query Hierarchical Labeling Schema (HLS) incremental update directed cyclic graph graph indexing, reachability query, Hierarchical Labeling Schema (HLS), incremental update, directed cyclic graph
  • 相关文献

参考文献3

二级参考文献77

  • 1Kropf T. Introduction to Formal Hardware Verification. Springer Verlag, 1999.
  • 2Aagaard M D, Jones R B, Seger C H. Combining theorem proving and trajectory evaluation in an industrial environment. In Proc. the 1998 Conference on Design Automation (DAC-98), Los Alamitos, CA, ACM/IEEE, Jun. 1998, pp.538-541.
  • 3Joyce J J, Seger C H (eds.). The HOL-Voss system: Model checking inside a general-purpose theorem prover. Lecture Notes in Computer Science 780, Springer, 1994, pp.185-198.
  • 4Schneider K, Kropf T. Verifying hardware correctness by combining theorem proving and model checking. Technical Report SFB 358-C2-5/95, Institut fiir Rechnerentwurf und Fehlertoleranz, 1995.
  • 5Kort S, Tahar S, Curzon P. Hierarchical verification using an MDG-HOL hybrid tool. International Journal on Software Tools for Technology Transfer, May 2003, 4(3): 313-322.
  • 6Mizouni R, Tahar S, Curzon P. Hybrid verification incorporating HOL theorem proving and MDG model checking. Microelectronies Journal, November 2006, 37(11): 1200-1207.
  • 7Rajan S, Shankar N, Srivas M K. An integration of model checking with automated proof checking. In Proe. the 7th International Conference on Computer Aided Verification, Wolper P (ed.), Liege, Belgium, LNCS 939, Springer Verlag, 1995, pp.84-97.
  • 8Schneider K, Hoffmann D. A HOL conversion for translating linear time temporal logic to ω-automata. In Proc. TPHOLs, Nice, France, LNCS 1690, Springer-Verlag, 1999, pp.255-272.
  • 9Amjad H. Programming a symbolic model checker in a fully expansive theorem prover. In Proc. the 16th International Conference on Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science 2758, Springer-Verlag, 2003, pp.171-187.
  • 10Gordon M J C. Programming combinations of deduction and BDD-based symbolic calculation. LMS Journal of Computation and Mathematics, Aug. 2002, ISSN 1461-1570, 5: 56-76.

共引文献35

同被引文献3

引证文献1

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部