Given a 3-valued abstraction of a program (possibly generated usingstatic program analysis and predicate abstraction) and a temporal logic formula,generalized model checking (GMC) checks whether there exists a concretiza-tion of that abstraction that satisfies the formula. In this paper, we revisit gen-eralized model checking for linear time (LTL) properties. First, we show thatLTL GMC is 2EXPTIME-complete in the size of the formula and polynomial inthe model, where the degree of the polynomial depends on the formula, insteadof EXPTIME-complete and quadratic as previously believed. The standard def-inition of GMC depends on a definition of concretization which is tailored forbranching-time model checking. We then study a simpler linear completenesspreorder for relating program abstractions. We show that LTL GMC with thisweaker preorder is only EXPSPACE-complete in the size of the formula, and canbe 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 GMCis reduced.
展开▼
