The problem of checking if a program execution meets
a formal specification arises in many software engineering tasks
including runtime verification and designing test oracles.
When online analysis is not possible,
execution trace logs are stored for offline postmortem analysis,
often in a compressed format to reduce disk space and warehousing requirements.
A straightforward method for checking if a compressed execution
satisfies a property is to first decompress it
and then analyze the resulting uncompressed execution.

In this paper, we consider the problem of
checking if an execution trace, compressed using a
grammar-based lossless compression scheme, satisfies a specification expressed
in linear temporal logic, without explicitly decompressing it.
In general, this problem is known to be intractable (PSPACE-hard in the size
of the compressed trace and the LTL formula).
We show that the problem can be solved in \emph{polynomial time}
for the fragment LTL[F,G,X], which comprises of
all Boolean and modal operators of LTL except the \emph{until} operator.
Our algorithm for analyzing SLPs (a grammar-based compression scheme)
is effective in practice — for a suite of large execution traces obtained from
open source projects, our algorithm shows significant speed ups
when compared with the performance of checking LTL
properties over corresponding uncompressed traces.