Graph pattern matching that aims to seek out answer graphs in a data graph matching a provided graph, plays a fundamental role as a part of graph search for graph databases. “Matching” indicates that the two graphs are correlated, such as bisimulation, isomorphism, simulation, etc. The strictness of bisimulation is between simulation and isomorphism. Seldom work has been done to search for bisimulation subgraphs. This research focuses on the problem. The symbol [Formula: see text] is introduced to fundamental modal logic language, thereby yielding [Formula: see text] language; the symbols [Formula: see text] is added for forming [Formula: see text] formulas. Then conclusions about graph bisimulations are shown. Subsequently, a theorem with detailed proof is presented, stating that [Formula: see text] formulas characterize finite directed graphs modulo bisimulation. According to the conclusions and theorem, algorithms for finding subgraphs are proposed. After dividing the query graph, the match graphs undergo the characterization using [Formula: see text] formulas. In the data graphs, by model checking the formulas, the answer graphs exhibiting bisimilarity to the match graphs are able to be captured.
Smooth Fano polytopes arising from finite directed graphs
