一句话：刻画有界变量一阶查询参数化模型检测的空间复杂度，证明其按量词交替秩对树层级完备，并联系 Savitch 定理。
本文研究有界变量一阶句子（查询）在关系结构（数据库）上模型检测的参数化空间复杂度，参数为句子长度。作者引入由空间受限交替机定义的树层级，介于参数化对数空间与固定参数可处理时间之间；并证明按量词交替秩的每个界，该问题分别对该层级相应层次完备。文章进一步观察到，若存在针对存在性有界变量查询的参数化对数空间模型检测器，就能改进 Savitch 定理关于非确定对数空间的确定 O(log^2 n) 空间模拟。最后给出面向有界变量且量词交替秩有界查询的高空间效率模型检测器，并在假设 Savitch 定理最优时分析其最优性。
The parameterized model-checking problem for a class of first-order sentences (queries) asks to decide whether a given sentence from the class holds true in a given relational structure (database); the parameter is the length of the sentence. We study the parameterized space complexity of the model-checking problem for queries with a bounded number of variables. For each bound on the quantifier alternation rank the problem becomes complete for the corresponding level of what we call the tree hierarchy, a hierarchy of parameterized complexity classes defined via space bounded alternating machines between parameterized logarithmic space and fixed-parameter tractable time. We observe that a parameterized logarithmic space model-checker for existential bounded variable queries would allow to improve Savitch's classical simulation of nondeterministic logarithmic space in deterministic space $O(\log^2n)$. Further, we define a highly space efficient model-checker for queries with a bounded number of variables and bounded quantifier alternation rank. We study its optimality under the assumption that Savitch's Theorem is optimal.
@article{paperbot755,
title = {The parameterized space complexity of model-checking bounded variable first-order logic},
author = {Yijia Chen and Michael Elberfeld and Moritz Müller},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 3},
year = {2019},
doi = {10.23638/lmcs-15(3:31)2019}
}