Faster algorithms for the nonemptiness of streett automata and for communication protocol pruning

Abstract

This paper shows how a general technique, called lock-step search, used in dynamic graph algorithms, can be used to improve the running time of two problems arising in program verification and communication protocol design. (1) We consider the nonemptiness problemfor Streett automata: We are given a directed graph e = (V, E) with n = |V| and m = |E|, and a collection of pairs of subsets of vertices, called Streettpairs, {Li, Ui), i = 1..k. The question is whether G has a cycle (not necessarily simple) which, for each 1 ≤ i ≤ k, if it contains a vertex from Li then it also contains a vertex of Ui. Let b = (Formula Presented). The previously best algorithm takes time O((m+b)min{n, k}). We present an algorithm that takes time (Formula Presented) + b min{log n, k}). (2) In communication protocol pruning we are given a directed graph G = (V, E) with l special vertices. The problem is to efficiently maintain the strongly-connected components of the special vertices on a restricted set of edge deletions. Let mi be the number of edges in the strongly connected component of the ith special vertex. The previously best algorithm repeatedly recomputes the strongly-connected components which leads to a running time of (Formula Presented) m2i). We present an algorithm with time (Formula Presented).