\subsubsection{Linear Time Properties (LTL)} We refer to Section~\ref{sec:ltl} for intuition, as these tend to mostly be intuition exercises.