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 of $Σ^*$ 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://cstheory.stackexchange.com/questions/45609

$\endgroup$