Please use this identifier to cite or link to this item:
Title: LTL generalized model checking revisited
Authors: Godefroid, Patrice
Piterman, Nir
First Published: 16-Sep-2010
Publisher: Springer
Citation: International Journal on Software Tools for Technology Transfer, 2011, 13 (6), pp. 571-584
Abstract: 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.
DOI Link: 10.1007/s10009-010-0169-3
ISSN: 1433-2779
eISSN: 1433-2787
Version: Post-print
Status: Peer-reviewed
Type: Journal Article
Rights: © Springer-Verlag 2010. Deposited with reference to the publisher's archiving policy available on the Journal website. The original publication is available at
Appears in Collections:Published Articles, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
main.pdf274.13 kBUnknownView/Open

Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.