# 19.4 Separating words problem

Given two words $$u, v$$ of length $$n$$ over $$\{a, b\}$$. Does there always exist an automaton of size $$O(\log n)$$ which distinguishes $$u$$ and $$v$$. Or bigger, like $$O(n^{1/3})$$? Best known bound is about $$O(n^{2/5} \log(n))$$.

# 19.3 Universality for unambiguous automata

Determine the complexity of universality problem for unambiguous finite automata. Problem is known to be in PTIME and (as far as I understand) in $$\textup{NC}^2$$, but is only known to be NL-hard.

# 19.2 SafeLTL

An $ω$-word language $$L\subseteq \Sigma^\omega$$ is a safety language if for all $$w\not \in L$$ there is a prefix $$v\in \Sigma^*$$ of $$w$$ such that for all $$u\in \Sigma^\omega$$, $$vu\not \in L$$.

safeLTL is the fragment of negation normal form LTL without Until nor Finally. SafeLTL captures exactly LTL expressible safety properties. However, to go from an LTL formula describing a safety property to an equivalent safeLTL formula, the best known translation seems to go via a deterministic safety automaton and then back to LTL, incurring a triple-exponential blow-up on the way.

Open problem: Is there a (more) concise translation from LTL to safeLTL? Are there safety properties that are exponentially more concisely expressible in LTL than safeLTL?

# 19.1 Deciding upperboundedness of $$\bbZ$$-CCRA

A cost register automaton (CRA) over $$(\bbZ, \min, +)$$ is a DFA equipped with a finite number of registers that take values in $$\bbZ$$. Each transition induces a transformation of the registers formulated with $$\min$$ and $$+$$; for instance $$x \leftarrow \min\{x, y+3\} + z$$. Accepting states can then output one of the registers.