Faster Algorithms for the Nonemptiness of Streett Automata and forCommunication Protocol Pruning
This paper shows how a general technique, called {\it lock-step search}, developed for 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 {\it nonemptiness problem for Streett automata}: We are given a directed graph $G=(V,E)$ with $n=|V|$ and $m=|E|$, and a collection of pairs of subsets of vertices, called {\em Streett pairs}, $\langle L_i, U_i \rangle, i= 1..k$. The question is whether $G$ has a cycle (not necessarily simple) which, for each $1 \leq i \leq k$, either contains no vertex from $L_i$ or contains a vertex of $U_i$. Let $b= \sum_{i=1..k} |L_i|+|U_i|$. The previously best algorithm takes time $O((m+ b)\min{n,k})$. We present an algorithm that takes time $O(m \min { \sqrt{m \log n}, k, n} + b \min {\log n, k})$. (2) In {\it 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 $m_i$ be the number of edges in the strongly connected component of the $i$th special vertex. The previously best algorithm repeatedly recomputes the strongly-connected components which leads to a running time of $O(\sum_i m_i^2)$. We present an algorithm with time $O(\sqrt{l}\sum_i m_i^{1.5})$.