LTL Generalized Model Checking Revisited

Given a 3-valued abstraction of a program (possibly generated using rogram analysis and predicate abstraction) and a temporal logic formula, generalized model checking (GMC) checks whether there exists a concretization of that abstraction that satisfies the formula. In this paper, we revisit generalized model checking for linear time (LTL) properties. First, we show that LTL GMC is 2EXPTIME-complete in the size of the formula and polynomial in the model, where the degree of the polynomial depends on the formula, instead of EXPTIME-complete and quadratic as previously believed. The standard definition of GMC depends on a definition of concretization which is tailored for branching-time model checking. We then study a simpler linear completeness for relating program abstractions. We show that LTL GMC with this weaker preorder is only EXPSPACE-complete in the size of the formula, and can be solved in linear time and logarithmic space in the size of the model. Finally, we identify classe...

• Type: Conference
• Year: 2009
• Where: VMCAI
• Authors: Patrice Godefroid, Nir Piterman
• Keywords: Linear Time, LTL GMC, Model Checking, Software Engineering, VMCAI 2009