0
$\begingroup$

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).

Improve this question
$\endgroup$
  • $\begingroup$ I'm a bit confused by the assertion that there's a clock but no time. (OK, "real" time. But why does it matter if it's "real"?) Unrelated, I'd note there are two kinds of approximations in your post: timeouts lead to under-approximation, while $\Sigma^\omega$ is an over-approximation. $\endgroup$ – Radu GRIGore Sep 8 '15 at 9:39
  • $\begingroup$ Regarding "timeouts", the more natural formalization is in terms of discrete steps rather than real time. This leads to bounded operators like $F_{\le n}$, which is essentially a shorthand ($F_{\le n}\varphi \equiv \varphi\vee X\varphi\vee\dots\vee X^n\varphi$) $\endgroup$ – Klaus Draeger Sep 8 '15 at 11:19
  • $\begingroup$ You have to be careful about the notion of approximation, though - for example, consider the word $ababbabbba\dots\in\Sigma^\omega$. It satisfies $GFa$, but not $GF_{\le n}a$ for any $n$, i.e. your approximations won't converge to the original property. $\endgroup$ – Klaus Draeger Sep 8 '15 at 11:22
  • $\begingroup$ @RaduGRIGore: I thought from a topological point of view, the only approximation possible might be an over-approximation, in which case it has to be $\Sigma^{\omega}$ itself because it is the closure (i.e., safety version) of any liveness property. Yet I thought someone might point to any prior work on under-approximations, which would be more interesting (if possible at all). $\endgroup$ – Ahmed Nassar Sep 8 '15 at 22:31
  • $\begingroup$ @KlausDraeger: Thanks for mentioning $\mathbf{F}_{\leq n}$. As for sequences like $ababbabbba\ldots$, I would expect any decent approximation theory to define some sort of probability measure over $\Sigma^{\omega}$ and perhaps talk about convergence of the set of un-approximable sequences to a set of measure zero. I am not sophisticated enough to know if that is easy to do :) I am interested in this problem from a practical viewpoint, so unlikely sets of sequences would be OK. $\endgroup$ – Ahmed Nassar Sep 8 '15 at 22:39

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.