Weighted Safety

Safety properties, which assert that the system always stays within
some allowed region, have been extensively studied and used. In the
last years, we see more and more research on quantitative formal
methods, where systems and specifications are weighted. We introduce
and study safety in the weighted setting. For a value $v \in \Q$, we
say that a weighted language $L:\Sigma^* \rightarrow \Q$ is $v$-safe
if every word with cost at least $v$ has a prefix all whose extensions
have cost at least $v$. The language $L$ is then weighted safe if $L$
is $v$-safe for some $v$.

Given a regular weighted language $L$, we study the set of values $v
\in \Q$ for which $L$ is $v$-safe. We show that this set need not be
closed upwards or downwards and we relate the $v$-safety of $L$ with
the safety of the (Boolean) language of words whose cost in $L$ is at
most $v$. We show that the latter need not be regular but is always
context free. Given a deterministic weighted automaton $\A$, we relate
the safety of $L(\A)$ with the structure of $\A$, and we study the
problem of deciding whether $L(\A)$ is $v$-safe for a given $v$. We
also study the weighted safety of $L(\A)$ and provide bounds on the
minimal value $|v|$ for which a weighted safe $L(\A)$ is $v$-safe.