19.2 SafeLTL

By Karoliina Lehtinen

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

By Michaël Cadilhac

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 →