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

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