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.

Continue Reading →