19.6 HyperLTL satisfiability

By Corto Mascle

HyperLTL is an extension of LTL which allows quantification over traces. HyperLTL formulas are generated by the grammar: \[\phi::=\forall\pi.\phi\mid\exists\pi.\phi\mid\psi\] \[\psi::=a_\pi\mid\neg\psi\mid\psi\lor\psi\mid X\psi\mid\psi U\psi\] with the intuitive semantics. For example the formula \[\forall\pi.\exists\pi'.F(a_{\pi'}\land\neg a_\pi)\land G(a_\pi\Rightarrow a_{\pi'})\] expresses that for all traces there exists another trace satisfying \(a\) at strictly more positions; \(\{a\}^*\emptyset^\omega\) is a model of this formula. There are two main versions of the satisfiability problem for this logics: Given a formula \(\phi\), one can ask if there exists any set of traces satisfying \(\phi\), or if there exists a finite Kripke structure whose runs induce a set of traces satisfying \(\phi\). Unfortunately, both problems are undecidable in general.

Continue Reading →

19.5 On unambiguous grammars

By Lorenzo Clemente

The universality problem for context-free grammars is undecidable. For deterministic pushdown automata it is PTIME-complete. For unambiguous context-free grammars, which constitute a model of intermediate expressive power, the problem is still decidable. Using the existential theory of the reals (the existential fragment of Tarski's algebra), it can be shown to be in PSPACE. However, no lower-bound better than PTIME is known. Improving either the PSPACE upper or the PTIME lower-bound would be a major advance on this problem!

Continue Reading →

19.4 Separating words problem

By Wojciech Czerwiński

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

By Wojciech Czerwiński

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

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 →