论文标题
重新访问单表自动机的参数合成
Revisiting Parameter Synthesis for One-Counter Automata
论文作者
论文摘要
我们研究带有参数的单场自动机的（参数）合成问题。单场自动机是通过扩展经典有限状态自动机获得的，其值可以在非阴性整数范围内进行范围并进行零测试。可以通过引入一组称为参数的整数值变量来进一步进行参数。这种自动机的综合问题询问是否存在参数的估值，以使自动机的所有无限运行都满足某些omega-groumar属性。 Lechner表明，（补充）问题可以用限制性的一偏置片段和分裂性编码。在这项工作中（i）我们认为，不幸的是，所说的碎片被称为Aerpadplus。然而，通过将问题仔细地重新编码为Aerpadplus的可决定性限制，（ii）我们证明，对于几种固定的欧米茄属性，通常可以决定合成问题，而在N2EXP中是可以决定的。最后，（iii）我们为问题的特殊情况提供了一个多项式空间算法，在该问题的特殊情况下，只能在计数器的测试而不是更新中参数。
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.
