JavaScript is disabled for your browser. Some features of this site may not work without it.

## Faster Algorithms for the Nonemptiness of Streett Automata and forCommunication Protocol Pruning

#####
**Author**

Henzinger, Monika; Telle, Jan

#####
**Abstract**

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})$.

#####
**Date Issued**

1995-12#####
**Publisher**

Cornell University

#####
**Subject**

computer science; technical report

#####
**Previously Published As**

http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR95-1561

#####
**Type**

technical report