paperbot · PL 论文追踪

全部论文 待读 收藏

P2 On the Satisfiability of Context-free String Constraints with Subword-Ordering

具有子词序的上下文无关字符串约束的可满足性
LICS Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science2022匹配度 2/10 · 该论文属于形式化验证与自动机理论，研究带子词序的上下文无关字符串约束可满足性及下推系统可达性复杂度，但未涉及 LLM/Agent、静态分析、浮点程序分析或贝叶斯程序分析，与用户核心交叉方向几乎没有直接关联。引用 5 inbox
C. Aiswarya, Soumodev Mal, Prakash Saivasan
逻辑与自动机程序验证
crossref: 2026-09-12dblp: 2026-09-12

AI 速览

一句话：证明带子词序的上下文无关字符串约束一般不可判定，无环依赖片段为 NEXPTime 完全，并确定无环有损通道下推系统控制状态可达性的复杂度。

本文研究一类字符串约束的可满足性：变量需满足上下文无关语言的成员约束，并满足变量之间的子词序关系。作者首先指出该变体整体上是不可判定的。随后，他们考虑一个受限片段，其中子词序约束不在变量之间引入循环依赖，并证明该片段的可满足性是 NEXPTime 完全的。作为结果的应用，作者确定了无环有损通道下推系统中控制状态可达性问题的复杂度：该问题此前已知可判定，但没有基本上界，本文证明其同样是 NEXPTime 完全的。

问题
带上下文无关语言成员约束和子词序关系的字符串约束可满足性整体不可判定，需要识别可判定片段并确定其精确复杂度。
方法
通过限制子词序约束不产生变量间循环依赖，得到无环依赖片段，并对其可满足性进行复杂性分析，给出 NEXPTime 完全性证明。
评估
以理论复杂性证明为主要评估方式，证明该片段可满足性为 NEXPTime 完全，并将其应用于确定无环有损通道下推系统控制状态可达性的复杂度。
原文摘要（Abstract）

We consider a variant of string constraints given by membership constraints in context-free languages and subword relation between variables. The satisfiability problem for this variant turns out to be undecidable. We consider a fragment in which the subword-order constraints do not impose any cyclic dependency between variables. We show that this fragment is NexpTime-complete. As an application of our result, we settle the complexity of control state reachability in acyclic lossy channel pushdown systems, an important distributed system model. The problem was shown to be decidable in [8]. However, no elementary upper bound was known. We show that this problem is NexpTime-complete.

链接与引用

DOI 原文 · DBLP

BibTeX 
@inproceedings{AiswaryaMS22,
  title = {On the Satisfiability of Context-free String Constraints with Subword-Ordering},
  author = {C. Aiswarya and Soumodev Mal and Prakash Saivasan},
  booktitle = {LICS},
  year = {2022},
  doi = {10.1145/3531130.3533329}
}