Robust models for generalized model checking

Michael Huth

We review the motivation and utility of abstraction-based generalized model checking (GMC) through the example framework of modal transition systems, as proposed by Godefroid & Jagadeesan in their CAV'02 paper. We then explain why such frameworks have two potentially distinct notions of refinement. For GMC over modal transition systems we use an ordered framework model to prove that these refinements are equal in that case. Finally, we investigate whether semantic type constructors, notably powerdomains, preserve this desirable consistency property of framework models.