Given a 3-valued abstraction of a program (possibly generated using
static program 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 preorder 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 classes of formulas for which the model complexity of
standard GMC
is reduced.