一句话：证明连续单计数器自动机可达性：全局界测试在 NC²，一般情形多项式时间，参数化情形在多项式层级内可判定。
本文研究连续单计数器自动机（COCA）的可达性问题。该模型的迁移带有对计数器值的上界与下界测试，并且迁移时的计数器更新可被 0 与 1 之间的非零因子非确定地缩小。作者针对三类设定给出复杂度结果：带全局上下界测试的 COCA 可达性属于 NC²；一般 COCA 可达性可在多项式时间内判定；带参数化计数器更新与界测试的 COCA 可达性可在多项式层级内判定。评估为理论复杂度证明，未涉及实现或基准测试。
We study the reachability problem for continuous one-counter automata, COCA for short. In such automata, transitions are guarded by upper and lower bound tests against the counter value. Additionally, the counter updates associated with taking transitions can be (non-deterministically) scaled down by a nonzero factor between zero and one. Our three main results are as follows: (1) We prove that the reachability problem for COCA with global upper and lower bound tests is in NC2; (2) that, in general, the problem is decidable in polynomial time; and (3) that it is decidable in the polynomial hierarchy for COCA with parametric counter updates and bound tests.
DOI 原文 ·
@inproceedings{paperbot6167,
title = {Continuous One-Counter Automata},
author = {Michael Blondin and Tim Leys and Filip Mazowiecki and Philip Offtermatt and Guillermo A. Perez},
booktitle = {LICS},
year = {2021},
doi = {10.1109/lics52264.2021.9470525}
}