A formal language for specifying properties of systems over time, like "eventually safe" or "always avoid state X".