Rule-Based Graph Programs Matching the Time Complexity of Imperative Algorithms

TL;DR

This paper advances rule-based graph programming by enhancing data structures to match the time complexity of imperative algorithms, demonstrated through case studies including connectivity, acyclicity, and shortest paths.

Contribution

It overcomes previous limitations by improving the graph data structure in GP 2, enabling efficient implementations of fundamental algorithms on arbitrary graphs.

Findings

Linear time algorithms for connectivity and acyclicity on arbitrary graphs.

Shortest path program runs in O(nm) time, matching imperative Bellman-Ford.

Formal proofs and runtime experiments validate the approaches.

Abstract

We report on recent advances in rule-based graph programming, which allow us to match the time complexity of some fundamental imperative graph algorithms. In general, achieving the time complexity of graph algorithms implemented in conventional languages using a rule-based graph-transformation language is challenging due to the cost of graph matching. Previous work demonstrated that with rooted rules, certain algorithms can be implemented in the graph programming language GP 2 such that their runtime matches the time complexity of imperative implementations. However, this required input graphs to have a bounded node degree and (for some algorithms) to be connected. In this paper, we overcome these limitations by enhancing the graph data structure generated by the GP 2 compiler and exploiting the new structure in programs. We present three case studies: the first program checks whether input graphs are connected, the second program checks whether input graphs are acyclic, and the third program solves the single-source shortest-paths problem for graphs with integer edge-weights. The first two programs run in linear time on (possibly disconnected) input graphs with arbitrary node degrees. The third program runs in time $O(nm)$ on arbitrary input graphs, matching the time complexity of imperative implementations of the Bellman-Ford algorithm. For each program, we formally prove its correctness and time complexity, and provide runtime experiments on various graph classes.