TY - GEN
T1 - A parameterized halting problem, the linear time hierarchy, and the MRDP theorem
AU - Chen, Yijia
AU - Müller, Moritz
AU - Yokoyama, Keita
N1 - Funding Information:
The collaboration of Yijia Chen and Keita Yokoyama has been supported by NSFC-JSPS Bilateral Joint Research Project (Grant No. 61511140100).
Funding Information:
Acknowledgements. Moritz Müller has been supported by the Austrian Science Fund (FWF) under Project P28699, and is supported by the European Research Council (ERC) under the European Unions Horizon 2020 research programme (grant agreement ERC-2014-CoG 648276 AUTAR). Keita Yokoyama is partially supported by JSPS KAKENHI (grant numbers 16K17640 and 15H03634).
Publisher Copyright:
© 2018 ACM.
PY - 2018/7/9
Y1 - 2018/7/9
N2 - The complexity of the parameterized halting problem for nondeterministic Turing machines p-Halt is known to be related to the question of whether there are logics capturing various complexity classes [10]. Among others, if p-Halt is in para-AC0, the parameterized version of the circuit complexity class AC0, then AC0, or equivalently, (+, ×)-invariant FO, has a logic. Although it is widely believed that p-Halt < para-AC0, we show that the problem is hard to settle by establishing a connection to the question in classical complexity of whether NE . LINH. Here, LINH denotes the linear time hierarchy. On the other hand,we suggest an approach toward proving NE ⊈ LINH using bounded arithmetic. More specifically, we demonstrate that if the much celebrated MRDP (for Matiyasevich-Robinson- Davis-Putnam) theorem can be proved in a certain fragment of arithmetic, then NE ⊈ LINH. Interestingly, central to this result is a para-AC0 lower bound for the parameterized model-checking problem for FO on arithmetical structures.
AB - The complexity of the parameterized halting problem for nondeterministic Turing machines p-Halt is known to be related to the question of whether there are logics capturing various complexity classes [10]. Among others, if p-Halt is in para-AC0, the parameterized version of the circuit complexity class AC0, then AC0, or equivalently, (+, ×)-invariant FO, has a logic. Although it is widely believed that p-Halt < para-AC0, we show that the problem is hard to settle by establishing a connection to the question in classical complexity of whether NE . LINH. Here, LINH denotes the linear time hierarchy. On the other hand,we suggest an approach toward proving NE ⊈ LINH using bounded arithmetic. More specifically, we demonstrate that if the much celebrated MRDP (for Matiyasevich-Robinson- Davis-Putnam) theorem can be proved in a certain fragment of arithmetic, then NE ⊈ LINH. Interestingly, central to this result is a para-AC0 lower bound for the parameterized model-checking problem for FO on arithmetical structures.
UR - http://www.scopus.com/inward/record.url?scp=85051132389&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85051132389&partnerID=8YFLogxK
U2 - 10.1145/3209108.3209155
DO - 10.1145/3209108.3209155
M3 - Conference contribution
AN - SCOPUS:85051132389
T3 - Proceedings - Symposium on Logic in Computer Science
SP - 235
EP - 244
BT - Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018
Y2 - 9 July 2018 through 12 July 2018
ER -