A Kripke structure satisfies an LTL formula iff the synchronous product with the negated formula monitor has no accepting run. Nested DFS detects counterexample lassos on-the-fly in linear time.