1
$\begingroup$

Let $Σ$ be an alphabet (e.g., the powerset of atomic propositions coming from some Kripke structure, though such details are irrelevant here).

For infinite words, a language $P\subseteq Σ^ω$ is called a safety language iff every word $σ ∈ Σ^ω \setminus P$ has a finite prefix $σ̂$ such that $P ∩ \{σ' ∈ Σ^ω \mid σ̂\ \text{is a prefix of}\ σ'\} = ∅$.

  1. Is there an accepted, meaningful definition of safety languages for finite words, i.e., "A set $P\subseteq Σ^*$ is called a safety language iff …"?

  2. Is there an accepted, meaningful definition of safety languages for finite or infinite words, i.e., "A set $P\subseteq Σ^ω ∪ Σ^*$ is called a safety language iff …"?

For infinite words, a language $P\subseteq Σ^ω$ is called a liveness language iff each finite word from $Σ^*$ is a prefix of a word from $P$.

  1. Is there an accepted, meaningful definition of liveness languages for finite words, i.e., "A set $P\subseteq Σ^*$ is called a liveness language iff …"?

  2. Is there an accepted, meaningful definition of liveness languages for finite or infinite words, i.e., "A set $P\subseteq Σ^ω ∪ Σ^*$ is called a liveness language iff …"?

In cases 2 and 4, the definitions for finite-or-infinite words should be (intuitively speaking) compatible with the standard definitions for infinite words.

Of course, some folks prefer to speak about safety/liveness properties, which are predicates $𝒫(W)→\{0,1\}$, rather than about safety/liveness languages, which are subsets of $W$, where $W$ is the corresponding set of words ($Σ^ω$, $Σ^*$, or $Σ^ω∪Σ^*$). For this question, the preferred framework (predicates on the powerset vs. subsets) is irrelevant.

Needless to say: in case of a negative answer, please substantiate your concerns.

Crosspost: https://cs.stackexchange.com/questions/115156

$\endgroup$
  • $\begingroup$ Given a set of infinite words, you can construct the set of finite prefixes of those words. And given a set of finite words, you can build the set of infinite words that have infinitely many prefixes in the set. I think I've seen safety and liveness defined on sets of finite words in such a way that those two constructions preserved safety and liveness. I think it was in a Master 1 course though so it's possible it was introduced just to avoid speaking about infinite words. $\endgroup$ – xavierm02 Sep 29 '19 at 13:21
  • 1
    $\begingroup$ I did understand it. And if you call f the function that takes a language of finite words and returns the language of infinite words that have infinitely many prefixes in that language, then "f(L) is a safety language" is a correct definition for safety on languages of finite words, and you can rephrase it to not mention infinite words. $\endgroup$ – xavierm02 Sep 29 '19 at 13:43
  • $\begingroup$ Using f also works for liveness. I can't see any reasonable way to define it on languages with both finite and infinite words, other than defining g that applies f to the sublanguage of finite words and returns the union of that and the sublanguage of infinite words. But both definitions I described can't really bring anything new: in both cases, the language of finite words is just used to represent a language of infinite words, and aside from the representation, nothing changes. $\endgroup$ – xavierm02 Sep 30 '19 at 16:32
1
$\begingroup$

The answer is yes to all questions, so it is enough to answer 2 and 4, as the definitions work in particular for languages of finite words:

    1. A language $P\subseteq \Sigma^*\cup\Sigma^\omega$ is safety if whenever $u\notin P$, then $u$ has a finite prefix $u'\in\Sigma^*$ such that for any word $v$, $u'v\notin P$.
    1. A language $P\subseteq \Sigma^*\cup\Sigma^\omega$ is liveness if for any finite word $u\in\Sigma^*$, there is a word $v$ such that $uv\in P$.
| cite | improve this answer | |
$\endgroup$

Your Answer

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