Efficient Computation of Inductive Invariants for Regular Abstraction Frameworks

The paper introduces regular abstraction frameworks, a generalization of the approach to regular model checking based on inductive invariants. It shows that the problem of deciding if the language of the automaton recognizing an overapproximation of the reachable configurations intersects a given regular set of unsafe configurations is EXPSPACE-complete. The paper also presents a learning algorithm that computes this automaton in a lazy manner, stopping whenever the current hypothesis is already strong enough to prove safety.