  We present two new hybrid techniques that replace the synchronized product
used in the automata-theoretic approach for LTL model checking. The proposed
products are explicit graphs of aggregates (symbolic sets of states) that can
be interpreted as B\"uchi automata. These hybrid approaches allow on the one
hand to use classical emptiness-check algorithms and build the graph
on-the-fly, and on the other hand, to have a compact encoding of the state
space thanks to the symbolic representation of the aggregates. The Symbolic
Observation Product assumes a globally stuttering property (e.g., LTL \ X) to
aggregate states. The Self-Loop Aggregation Product} does not require the
property to be globally stuttering (i.e., it can tackle full LTL), but
dynamically detects and exploits a form of stuttering where possible. Our
experiments show that these two variants, while incomparable with each other,
can outperform other existing approaches.
