EECS 298-11: Special CAD Seminar Friday, April 26, 1996, 2pm 531 Cory Hall, Hogan Room Note the special time: Friday April 26, 2pm Computing Simulations on Finite and Infinite Graphs Peter Kopke Cornell University Joint work with Monika R. Henzinger (Digital Equipment Corporation) and Thomas A. Henzinger (UC Berkeley) Abstract 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(mn+n^2) algorithm for computing the similarity relation of a graph with $n$ vertices and $m$ edges. For effectively presented infinite graphs, we present a simple 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. Upcoming seminars: May 1: John Marren, Alex. Brown & Sons May 8: Ganesh Gopalakrishnan, Univ. of Utah May 10 (Friday 11AM): Dhiraj Pradhan, Texas A & M Univ.