一句话：提出 shortening/lengthening 不敏感语言以推广 stutter 不敏感，并给出基于结构约简的半判定验证。
LTL 等 ω-正则性质的验证可利用 stutter 不敏感性进行约简，但含 next 算子或计数的性质通常不满足该性质。本文将 stutter 等价分解为两个蕴含，定义更弱的 shortening 不敏感和 lengthening 不敏感语言：前者要求 stutter 更少的词仍被接受，后者为其对偶。作者提出半判定过程，在仅能缩短运行的结构约简（如 Lipton 事务约简、Petri 网聚集）上证明 shortening 不敏感性质或否证 lengthening 不敏感性质。进一步将性质语言划分为 stutter 不敏感、shortening 不敏感、lengthening 不敏感和长度敏感四部分，使结构约简仍可用于任意性质。实现与实验表明，多数非随机且对 stutter 敏感的性质实际属于 shortening 或 lengthening 不敏感。
Verification of properties expressed as $\omega$-regular languages such as LTL can benefit hugely from stutter insensitivity, using a diverse set of reduction strategies. However properties that are not stutter invariant, for instance due to the use of the neXt operator of LTL or to some form of counting in the logic, are not covered by these techniques in general. We propose in this paper to study a weaker property than stutter insensitivity. In a stutter insensitive language both adding and removing stutter to a word does not change its acceptance, any stuttering can be abstracted away; by decomposing this equivalence relation into two implications we obtain weaker conditions. We define a shortening insensitive language where any word that stutters less than a word in the language must also belong to the language. A lengthening insensitive language has the dual property. A semi-decision procedure is then introduced to reliably prove shortening insensitive properties or deny lengthening insensitive properties while working with a \emph{reduction} of a system. A reduction has the property that it can only shorten runs. Lipton's transaction reductions or Petri net agglomerations are examples of eligible structural reduction strategies. We also present an approach that can reason using a partition of a property language into its stutter insensitive, shortening insensitive, lengthening insensitive and length sensitive parts to still use structural reductions even when working with arbitrary properties. An implementation and experimental evidence is provided showing most non-random properties sensitive to stutter are actually shortening or lengthening insensitive.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2212-04218,
title = {Structural Reductions and Stutter Sensitive Properties},
author = {Emmanuel Paviot-Adet and Denis Poitrenaud and Etienne Renault and Yann Thierry-Mieg},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 2},
year = {2025},
doi = {10.46298/lmcs-21(2:15)2025}
}