36th Annual Symposium on Foundations of Computer Science (FOCS'95) Computing simulations on finite and infinite graphs Milwaukee, Wisconsin October 23-October 25 ISBN: 0-8186-7183-1
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) algorithm for computing the similarity relation of a graph with n vertices and m edges (assuming m/spl ges/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 /spl forall/CTL* model-checking problem are decidable for 2D rectangular automata.
Index Terms:
graph theory; decidability; automata theory; simulations computing; infinite graphs; finite graphs; similarity relations; labeled graphs; reactive systems verification; O(mn) algorithm; symbolic similarity-checking procedure; 2D rectangular automata; continuous environments; model-checking problem; decidability
Citation:
M.R. Henzinger, T.A. Henzinger, P.W. Kopke, "Computing simulations on finite and infinite graphs," focs, pp.453, 36th Annual Symposium on Foundations of Computer Science (FOCS'95), 1995 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||