19.13 Does a $(\textsf{min,+})$-WA preserve REG by inverse image?

By Nathan Lhote

We are interested in functions realized by weighted automata over the semiring \(\mathbb N_{\mathsf{ min}}=\langle \mathbb N\cup\left\{ \infty \right\} , \mathsf{ min}, +, \infty,0\rangle\). An $\mathbb N\mathsf{ min}$-weighted automaton \(\mathcal A\) over alphabet \(\Sigma\) realizes a partial function \(\llbracket \mathcal A \rrbracket:\Sigma^*\rightarrow \mathbb N\). We want to decide given such a function if it preserves ``simple'' sets by inverse image. By simple we mean regular languages (\(\mathbb N\) is viewed a the set of words over a unary alphabet, hence the regular languages are the semilinear sets). Let us state the decision problem.

Continue Reading →

19.12 Reachability for bounded branching VASS

By Filip Mazowiecki

Recall that a $d$-VASS is a finite automaton, where transitions are labelled with $d$-dimensional vectors over integers. A configuration of a $d$-VASS is a pair of a state and a $d$-dimensional vector over naturals. Bounded VASS (BoVASS) are a variant of the classic VASS model where all values in all configurations are upper bounded by a fixed natural number, encoded in binary in the input. It is easy to see that the reachability is in PSPACE for BoVASS and it is not hard to show NP-hardness.

Continue Reading →

19.11 Shortest runs in 3-D VASS

By Wojciech Czerwiński

Is there a 3-D VASS with shortest run from source to target, which is longer than exponential? Best lower bound is exponential, best upper bound is tower. The case of VASSes with finite reachability set is probably the core of the problem. In my point this is one of the problems we should attack if we want to push theory of VASSes further.

19.10 Variants of one-counter systems universality

By Patrick Totzke

Problem 1:1 Given a 1-VASS, let \(L_n\) be its language where acceptance is by reaching a final state from a fixed initial state and initial counter value \(n\). Does there exist \(n\) such that \(\Sigma^* = L_n\) ?

Problem 2: Given a 1-VASS, let \(L^n\) be the language of the $n$-bounded system (the NFA where values 0..n are hard-coded) where acceptance is by reaching a final state from a fixed initial configuration. Does there exist \(n\) such that \(\Sigma^* \subseteq L^n\)?

Continue Reading →

19.8 Logic and automata for multiply nested-words

By Marie Fortin

Nested-word automata (NWA) are essentially visibly pushdown automata with multiple stacks. They accept languages of (multiply) nested-words, which are words equipped with a fixed number of binary nesting relations, connecting matching push and pop events. In the case of a single stack (that is, a single nesting relation), NWA are equivalent to monadic second-order logic (MSO). The binary predicates used in the logic are the direct successor relation, and the nesting relations. However, in the general case, and even with only two stacks, NWA are not closed under complementation, and strictly less expressive than MSO. In fact, for two stacks, NWA are equivalent to the existential fragment of MSO (EMSO). The equivalence with MSO can be recovered when restricting the set of possible behaviors, one classical example being phase-bounded nested words.

In the general case (more than two stack, arbitrary nested words), the exact expressive power of NWA is not known. In particular, the following question is open: can every first-order formula be translated into an equivalent NWA ?

19.7 Membership in logical classes for (succinct) finite automata

By Charles Paperman

Finite automata can be represented concisely in many way, including enriching their description with bounded-size stacks and registers, by allowing them to be two-way, etc…

Little is known of the complexity of checking membership of those representation of finite automaton into logical formalism (such as LTL, First-Order Logic). Most of the time, classical algorithms relies on testing algebraic properties of the transition semigroup of the automaton. The transition semigroup itself is exponential in the size of the automaton. A straight forward application of those methods to concise representation will lead to tower of exponential algorithms.

For specific kind of concise representations, smarter algorithms could lead to only an exponential blowup.

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.