## Computing Simulations on Finite and Infinite Graphs

*Monika R. Henzinger,
Thomas A. Henzinger,
and Peter W. Kopke*

We present algorithms for computing similarity relations of labeled
graphs. Similarity relations have applications for the refinement and
verification of reactive systems. For finite graphs, we present an
*O(m · n)* algorithm for computing the similarity relation
of a graph with *n* vertices and *m* edges (assuming *m
> n*). For effectively presented infinite graphs, we present a
symbolic similarity-checking procedure that terminates if a finite
similarity relation exists. We show that 2D rectangular automata,
which model discrete reactive systems with continuous environments,
define effectively presented infinite graphs with finite similarity
relations. It follows that the refinement problem and the ACTL*
model-checking problem are decidable for 2D rectangular automata.

*Proceedings of the
36th Annual Symposium on Foundations of Computer Science*
(FOCS), IEEE Computer Society Press, 1995, pp. 453-462.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 1995 IEEE.