  TLA is a popular temporal logic for writing stuttering-invariant
specifications of digital systems. However, TLA lacks higher-order features
useful for specifying modern software written in higher-order programming
languages. We use categorical techniques to recast a real-time semantics for
TLA in terms of the actions of a group of time dilations, or "stutters," and an
extension by a monoid incorporating delays, or "falters." Via the geometric
morphism of the associated presheaf topoi induced by the inclusion of stutters
into falters, we construct the first model of a higher-order TLA.
