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 at 13:21
  • $\begingroup$ @xavierm02 If you consider citing, please don't cite anything you have not understood yourself: I've seen one blantantly bogus construction in a particular lecture. (That's why I ask here.) $\endgroup$ – MdAyq7 Sep 29 at 13:26
  • 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 at 13:43
  • $\begingroup$ @xavierm02 Thx. How about liveness? How about $Σ^ω∪Σ^∗$? $\endgroup$ – MdAyq7 Sep 29 at 16:58
  • $\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 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$.
$\endgroup$
  • $\begingroup$ Thx! That's what I'd had expected intuitively. But, any citation, perhaps? Is it the same as @xavierm02's suggestion? $\endgroup$ – MdAyq7 Sep 30 at 22:59

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.