It feels very alive, somehow. When I think of LTL formulas, I imagine a collection of Since
formulas as little caterpillars, crawling down a linear structure searching for a state that satisfies
their hunger. This video gets kind of close to what I'm thinking of:
Honorable mention to this one, which I found is also quite cool: