结构化简与失真敏感属性
摘要：关于满足omega正则语言(如LTL)的性质的验证的研究，在使用不同的归约策略时，利用“stutter insensitivity”可以获得巨大的好处。然而，由于使用了LTL的neXt运算符或在逻辑中采用了某种计数形式，导致不具有“stutter invariance”(即对stutter不敏感)的性质通常无法由这些技术来覆盖。本文提出研究一种比“stutter insensitivity”更弱的性质。在一个“stutter insensitive”语言中，无论在一个单词中增加还是删除stutter，都不会改变其接受性，任何stutter都可以被提取出来；通过将这个等价关系分解为两个蕴含关系，我们得到了更弱的条件。我们定义了一个“shortening insensitive”语言，其中任何 stutter 比该语言的一个单词少的单词也必须属于该语言。一个“lengthening insensitive”语言具有相反的属性。然后，引入了一个半决策程序，可以在处理一个系统的“reduction”的基础上，可靠地证明“shortening insensitive”属性或否认“lengthening insensitive”属性。一种reduction具有只能缩短runs的属性。Lipton的transaction reductions或Petri网聚集是合格的结构归约策略的例子。我们还提出了一种方法，可以使用属性语言的一个分割，将其分为stutter不敏感、shortening不敏感、lengthening不敏感和length敏感的部分，即使在处理任意属性时也可以使用结构归约。提供了一个实现和实验证据，显示大多数对stutter敏感的非随机属性实际上是shortening或lengthening不敏感的。
作者：Emmanuel Paviot-Adet and Denis Poitrenaud and Etienne Renault and Yann Thierry-Mieg
论文ID：2212.04218
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2022-12-09