Henzinger, Monika ; Henzinger, Thomas AIST Austria ; Kopke, Peter W
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⩾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 ∀CTL* model-checking problem are decidable for 2D rectangular automata
453 - 462
FOCS: Foundations of Computer Science
Henzinger M, Henzinger TA, Kopke P. Computing simulations on finite and infinite graphs. In: IEEE; 1995:453-462. doi:10.1109/SFCS.1995.492576
Henzinger, M., Henzinger, T. A., & Kopke, P. (1995). Computing simulations on finite and infinite graphs (pp. 453–462). Presented at the FOCS: Foundations of Computer Science, IEEE. https://doi.org/10.1109/SFCS.1995.492576
Henzinger, Monika, Thomas A Henzinger, and Peter Kopke. “Computing Simulations on Finite and Infinite Graphs,” 453–62. IEEE, 1995. https://doi.org/10.1109/SFCS.1995.492576.
M. Henzinger, T. A. Henzinger, and P. Kopke, “Computing simulations on finite and infinite graphs,” presented at the FOCS: Foundations of Computer Science, 1995, pp. 453–462.
Henzinger M, Henzinger TA, Kopke P. 1995. Computing simulations on finite and infinite graphs. FOCS: Foundations of Computer Science 453–462.
Henzinger, Monika, et al. Computing Simulations on Finite and Infinite Graphs. IEEE, 1995, pp. 453–62, doi:10.1109/SFCS.1995.492576.