Marius Bozga and Radu Iosif
On Model Checking Generic Topologies (2004)
On Model Checking Generic Topologies (2004)
TR-2004-7.ps
Keywords: Graph topologies, Kleene algebra, Model checking
Abstract: This paper develops a method for verifying properties related to the topologies of finite graph structures. We introduce a generic framework for modeling graphs, based on Kleene algebras, and define an expressive logic which uses equivalences of regular expressions, allowing to state structural properties, such as: subgraph isomorphism, existence of cliques and strongly connected components, planarity, etc. We study the satisfiability and model checking problems for this logic and find that the former is undecidable and the latter is NP-hard. Second, we give a model checking algorithm and propose some heuristics for reducing its complexity. Finally, we describe possible uses of our technique to solve specific verification problems, such as shape analysis or checking consistency of UML models.
