---
res:
bibo_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) 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@eng
bibo_authorlist:
- foaf_Person:
foaf_givenName: Monika
foaf_name: Henzinger, Monika
foaf_surname: Henzinger
- foaf_Person:
foaf_givenName: Thomas A
foaf_name: Thomas Henzinger
foaf_surname: Henzinger
foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
orcid: 0000−0002−2985−7724
- foaf_Person:
foaf_givenName: Peter
foaf_name: Kopke, Peter W
foaf_surname: Kopke
bibo_doi: 10.1109/SFCS.1995.492576
dct_date: 1995^xs_gYear
dct_publisher: IEEE@
dct_title: Computing simulations on finite and infinite graphs@
...