# How are safety/liveness languages defined on the set of finite or infinite words?

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.

• 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. – xavierm02 Sep 29 at 13:21
• @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.) – MdAyq7 Sep 29 at 13:26
• 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. – xavierm02 Sep 29 at 13:43
• @xavierm02 Thx. How about liveness? How about $Σ^ω∪Σ^∗$? – MdAyq7 Sep 29 at 16:58
• 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. – xavierm02 Sep 30 at 16:32

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