<p>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:</p>

<p>$\forall w_1, w_2 \in \Sigma^{\omega}:\ d(w_1, w_2) = \frac{1}{2^n}$, where $n$ is the longest common prefix.</p>

<p>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.</p>

<p>According to this topology, every finite prefix $u \in \Sigma^{\ast}$ corresponds to the <em>ball</em> of all infinite extensions of $u$. The radius of that ball is inverse-exponentially related to the length of $u$.</p>

<p>I have one question:</p>

<blockquote>
  <p>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$?</p>
</blockquote>

<p><strong>What is meant by timeout, since temporal logic does not know about real time?</strong> 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.</p>

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

CC BY-SA 3.0
2015-09-08T09:39:56.723Z
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.
Radu GRIGore
CC BY-SA 3.0
2015-09-08T11:19:02.587Z
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$)
Klaus Draeger
CC BY-SA 3.0
2015-09-08T11:22:39.690Z
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.
Klaus Draeger
CC BY-SA 3.0
2015-09-08T22:31:06.600Z
@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).
Ahmed Nassar
CC BY-SA 3.0
2015-09-08T22:39:51.293Z
@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.
Ahmed Nassar
CC BY-SA 4.0
2019-05-01T06:29:52.233Z
You may want to have a look at “prompt” semantics, i.e. a semantics of temporal logics (LTL included), where for each model of a formula there is always an upper bound, although unknown, to the time every eventuality takes to be satisfied.
Nicola Gigante
<model-checking><approximation><topology><temporal-logic>
Approximating liveness properties with safety properties
Ahmed Nassar
# Approximating liveness properties with safety properties

(Asked by: username_0 on 2015-09-08)

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

**Tags:** model-checking, approximation, topology, temporal-logic
> **Comments:**
> **username_1**: 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.  
> **username_2**: 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$)  
> **username_2**: 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.  
> **username_0**: @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).  
> **username_0**: @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.  
> **username_3**: You may want to have a look at “prompt” semantics, i.e. a semantics of temporal logics (LTL included), where for each model of a formula there is always an upper bound, although unknown, to the time every eventuality takes to be satisfied.  

---

## 0 answers

