Given a finite alphabet set $\Sigma$, the set $\Sigma^{\omega}$ of infinite words over $\Sigma$ can be topologized with a metric $d: \Sigma^{\omega} \rightarrow \mathbb{R}$ such as:
$\forall w_1, w_2 \in \Sigma^{\omega}:\ d(w_1, w_2) = \frac{1}{2^n}$, where $n$ is the longest common prefix.
Given a linear-time (LT) property $P \subseteq \Sigma^{\omega}$, $P$ is a liveness property iff it is a dense subset of $\Sigma^{\omega}$. Also, $P$ is a safety property iff it is a closed set.
According to this topology, every finite prefix $u \in \Sigma^{\ast}$ corresponds to the ball of all infinite extensions of $u$. The radius of that ball is inverse-exponentially related to the length of $u$.
I have one question:
Is there some precise sense in which a liveness property $P$ can be approximated with a safety property, e.g., by applying some (possibly arbitrarily large) timeouts on all eventualities in $P$?
What is meant by timeout, since temporal logic does not know about real time? This question mainly arose in synchronous digital circuits where there is a clock signal and every clock edge means an event $\sigma \in \Sigma$ depending on logic signal values observed by that edge.
This question might sound odd, but the answer will surely be illuminating to me (e.g., a topologist might say dense subsets can only be approximated by the entire space $\Sigma^{\omega}$, which is the only property that is both liveness and safety).