A Practical Algorithm for Structure Embedding
I will start by introducing the concept of Predicate Automata and their use in concurrent program verification. Next, I'll describe the challenge of emptiness checking for such Predicate Automata --- How does one determine when to stop expanding a configuration of states? To do this, I introduce the notion of covering. If a configuration is covered by another already expanded configuration, then we can safely stop expanding. I will then show that the problem of determining coverability between two configurations is equivalent to the structure embedding problem. Finally, I’ll present MatchEmbeds, an algorithm for the structure embedding problem: given two finite first-order structures over a common relational vocabulary, does there exist an injective homomorphism from one to the other? The structure embedding problem is NP-complete in the general case, but for monadic structures (each predicate has arity 1) I observe that it can be solved in polytime by reduction to bipartite graph matching. My algorithm extends the bipartite matching approach to the general case by using it as the foundation of a backtracking search procedure. I show that MatchEmbeds outperforms state-of-the-art constraint satisfaction solvers on difficult random instances and significantly improves the performance of a client model checker for multi-threaded programs.