一句话：提出带参数与Presburger约束的数据词逻辑pSDL，支持数值算术与数据计数，并给出可判定性和复杂度。
论文研究带数值数据的数据词推理问题。已有数据词逻辑（如两变量逻辑与数据自动机）虽能进行某种数据计数，却无法表达数值域上的算术。作者提出参数化半线性数据逻辑 pSDL，允许参数，并在数据值及等价类 Parikh 像上施加 Presburger 守卫，从而表达“每个数据值至多出现一次且为偶数”“可被 4 整除的位置子集 a/b 数量相等”“最高频数据值可被 3 整除”“数据值集合构成区间”等语言。文章给出该逻辑成员判定与可满足性判定的可判定性及复杂度结果；与两变量数据词逻辑和数据自动机相比，pSDL 的可满足性检查具有初等复杂度，表达能力不可比。作者还讨论了在数据库与验证中的应用潜力。
We introduce parametric semilinear data logic (pSDL) for reasoning about data words with numeric data. The logic allows parameters, and Presburger guards on the data and on the Parikh image of equivalence classes (i.e. data counting), allowing us to capture data languages like: (1) each data value occurs at most once in the word and is an even number, (2) the subset of the positions containing data values divisible by 4 has the same number of a’s and b’s, (3) the data value with the highest frequency in the word is divisible by 3, and (4) each data value occurs at most once, and the set of data values forms an interval. We provide decidability and complexity results for the problem of membership and satisfiability checking over these models. In contrast to two-variable logic of data words and data automata (which also permit a form of data counting but no arithmetics over numeric domains and have incomparable inexpressivity), pSDL has elementary complexity of satisfiability checking. We show interesting potential applications of our models in databases and verification.