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 -