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}\ σ'\} = ∅$.


Is there an accepted, meaningful definition of safety languages for finite words, i.e., "A set $P\subseteq Σ^*$ is called a safety language iff …"?
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$.


Is there an accepted, meaningful definition of liveness languages for finite words, i.e., "A set $P\subseteq Σ^*$ is called a liveness language iff …"?
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
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:



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


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