← All problems
Unverified

Deciding upperboundedness of Z -CCRA

A cost register automaton (CRA) over (Z,min⁡,+)(\mathbb{Z}, \min, +) is a DFA equipped with a finite number of registers that take values in Z\mathbb{Z}. Each transition induces a transformation of the registers formulated with min⁡\min and ++; for instance x←min⁡{x,y+3}+zx \leftarrow \min\{x, y+3\} + z. Accepting states can then output one of the registers. Consider the model in which: Each update uses only min⁡\min's and addition with constants , For each transition, no register appears twice on the right-hand side of the updates. This model, which we call Z\mathbb{Z}-CCRA (the extra C standing for copyless ), can express for instance:

f(ai1#…#ain)=min⁡{i1,…,in},f(a^{i_1}\#\ldots\#a^{i_n}) = \min \{i_1, \ldots, i_n\}\enspace,

but couldn't express g(bi#w)=i+f(w)g(b^i\#w) = i + f(w) ---this would require either copying ii, or adding two registers. For weighted automata people, note that this model is equivalent to this, where W\mathcal{W} is a deterministic WA over (Z,min⁡,+)(\mathbb{Z}, \min, +): In [1], we showed that equivalence is undecidable for that model (even, and this is much more interesting, when restricted to N\mathbb{N}). We also showed that it is undecidable, given a Z\mathbb{Z}-CCRA, to decide whether the function it expresses is always negative. Question: Is it decidable, given a Z\mathbb{Z}-CCRA, whether the function it expresses is upper-bounded? That is, whether (∃c)(∀w)[f(w)≤c](\exists c)(\forall w)[f(w) \leq c]. [1] S. Almagor, M. Cadilhac, F. Mazowiecki, G. A. Pérez. Weak Cost Register Automata are Still Powerful. DLT'18. https://arxiv.org/abs/1804.06336

Coming soon

Organizer

Boyuan Wang portraitBoyuan Wang
Minghan Wang portraitMinghan Wang
Bochao Li portraitBochao Li
Hongwei Hu portraitHongwei Hu