Guarded Monotone Strict NP (GMSNP) extends Monotone Monadic Strict NP (MMSNP) by guarded existentially quantified predicates of arbitrary arities. We prove that the containment and the FO-rewritability problems for GMSNP are decidable, thereby settling an open question of Bienvenu, ten Cate, Lutz, and Wolter, later restated by Bourhis and Lutz. Our proof also comes with a 2NEXPTIME upper bound on the complexity of the two problems, which matches the lower bounds for MMSNP due to Bourhis and Lutz. To obtain these results, we significantly improve the state of knowledge of the model-theoretic properties of GMSNP. Bodirsky, Knäuer, and Starke previously showed that every GMSNP sentence defines a finite union of CSPs of $ω$-categorical structures. We show that these structures can be used to obtain a reduction from the containment problem for GMSNP to the much simpler problem of testing the existence of a recolouring; a careful analysis of this yields said upper bound for containment. The upper bound for FO-rewritability is subsequently obtained by an application of several standard techniques from the theory of infinite-domain CSPs. As our secondary contribution, we refine the construction of Bodirsky, Knäuer, and Starke by adding a restricted form of homogeneity to the properties of these structures, making the logic amenable to future complexity classifications for query evaluation using techniques developed for infinite-domain CSPs.

翻译：受保护单调严格NP（GMSNP）通过引入任意元数的受保护存在量化谓词，扩展了单调一元严格NP（MMSNP）。我们证明了GMSNP的包含问题和FO-重写问题是可判定的，从而解决了Bienvenu、ten Cate、Lutz和Wolter提出的开放性问题，该问题后来被Bourhis和Lutz重新阐述。我们的证明还给出了这两个问题复杂度的2NEXPTIME上界，这与Bourhis和Lutz针对MMSNP建立的下界相匹配。为了获得这些结果，我们显著改进了对GMSNP模型论性质的认识。Bodirsky、Knäuer和Starke先前证明了每个GMSNP语句定义了一组$ω$-范畴结构的CSP的有限并集。我们证明这些结构可用于将GMSNP的包含问题简化为测试重着色存在性的更简单问题；对此问题的细致分析得出了上述包含问题的上界。FO-重写问题的上界随后通过应用无限域CSP理论中的若干标准技术获得。作为次要贡献，我们通过向这些结构的性质添加受限形式的齐次性，改进了Bodirsky、Knäuer和Starke的构造，使得该逻辑能够利用为无限域CSP开发的技术进行未来查询评估的复杂度分类。