Graph Pattern Matching through Model Checking

Graph pattern matching is a hot spot in the big data era, which is to find answer graphs matching a given query graph in a data graph of graph databases. “Matching” means two graphs satisfy some relation, such as isomorphism, simulation, bisimulation, etc. Since there are seldom algorithms for the subgraph bisimulation, our work commits to solve the graph pattern matching problem involving bisimulation relations through the model checking technology. We characterize query graphs by modal formulas. By model checking the formulas in the data graphs, the answer graphs bisimilar to the query graphs can be discovered. We add _* to basic modal logic language resulting in ML + _* language, and add r* to form ML + _* formulas. Then a theorem which states that ML + _* formulas characterize finite directed graphs modulo bisimulation is put forward. Furthermore, we list steps to find answer graphs bisimilar to a query graph.