We study the (parameter) synthesis problem for one-counter automata with parameters. One-counter automata are obtained by extending classical finite-state automata with a counter whose value can range over non-negative integers and be tested for zero. The updates and tests applicable to the counter can further be made parametric by introducing a set of integer-valued variables called parameters. The synthesis problem for such automata asks whether there exists a valuation of the parameters such that all infinite runs of the automaton satisfy some omega-regular property. Lechner showed that (the complement of) the problem can be encoded in a restricted one-alternation fragment of Presburger arithmetic with divisibility. In this work (i) we argue that said fragment, called AERPADPLUS, is unfortunately undecidable. Nevertheless, by a careful re-encoding of the problem into a decidable restriction of AERPADPLUS, (ii) we prove that the synthesis problem is decidable in general and in N2EXP for several fixed omega-regular properties. Finally, (iii) we give a polynomial-space algorithm for the special case of the problem where parameters can only be used in tests, and not updates, of the counter.

翻译：我们用参数来研究单子自动自动成形器的合成问题(参数) 。 单子自动成形器是用一个计数器来延长典型的固定状态自动成形器,其值可以超过非负负整数,然后测试为零。 适用于该计数器的更新和测试还可以通过引入一套叫作参数的整数价值变量来进一步进行参数测量。 这种自动成形器的合成问题询问是否对参数进行了估价,使自动成形器的所有无限运行都满足了某些奥美加常规属性。 Lechner 显示, 问题( 其补充) 可以在一个限制的Presburger算术的单向化碎片中进行编码, 并且具有可辨别性。 在这项工作中, (一) 我们辩称, 所谓的AREPADDPLUS(ADPLUS) 的片段是不可分解的。 然而, 通过仔细的重新将问题归为AMEADPLUS(二), 我们证明合成问题一般是可以辨别的, 在N2EXP( ) 中, 一些固定的典型成正态成形的参数参数中, 我们只能给反式的反式的参数。 (三) 用于反式的反式的矩阵的参数。