颠倒的常规模型检测：一种基于不变量的方法
Regular Model Checking Upside-Down: An Invariant-Based Approach
AI总结：
本文提出一种从上方逼近可达配置集合的常规模型检测补充方法，利用归纳不变量的交集构造正则自动机，并分析其复杂度与所需子句数。
摘要：
常规模型检测是一种用于验证无限状态系统的技术，这些系统的配置可以表示为合适字母表上的有限单词。我们所研究的形式适用于初始配置集合是正则的、且转移关系由长度保持的转换器捕获的系统。为了验证安全性属性，常规模型检测迭代地计算识别越来越大的可达配置正则集合的自动机，并检查它们是否包含不安全配置。由于此过程通常不终止，因此已经开发了加速、抽象和加宽技术来计算可达配置的正则超集。在本文中，我们开发了一种补充性程序。我们不从下方逼近可达配置集合，而是从所有配置的集合开始，并从上方逼近它。我们利用可达配置集合等于系统所有归纳不变量的交集这一事实。由于该交集通常是非正则的，我们引入了b-不变量，定义为可由最多b个子句的CNF公式表示的那些不变量。我们证明，对于每个$b\geq0$，所有归纳b-不变量的交集是正则的，并构造了一个识别它的自动机。我们表明，对于每个$b\geq0$，该自动机是否接受某个不安全配置属于EXPSPACE，对于b=1则是PSPACE完全的。最后，我们研究了为了证明多个基准测试的安全性属性，b必须多大。
英文摘要：
Regular model checking is a technique for the verification of infinite-state systems whose configurations can be represented as finite words over a suitable alphabet. The form we are studying applies to systems whose set of initial configurations is regular, and whose transition relation is captured by a length-preserving transducer. To verify safety properties, regular model checking iteratively computes automata recognizing increasingly larger regular sets of reachable configurations, and checks if they contain unsafe configurations. Since this procedure often does not terminate, acceleration, abstraction, and widening techniques have been developed to compute a regular superset of the reachable configurations. In this paper, we develop a complementary procedure. Instead of approaching the set of reachable configurations from below, we start with the set of all configurations and approach it from above. We use that the set of reachable configurations is equal to the intersection of all inductive invariants of the system. Since this intersection is non-regular in general, we introduce b-invariants, defined as those representable by CNF-formulas with at most b clauses. We prove that, for every $b\geq0$, the intersection of all inductive b-invariants is regular, and we construct an automaton recognizing it. We show that whether this automaton accepts some unsafe configuration is in EXPSPACE for every $b\geq0$, and PSPACE-complete for b=1. Finally, we study how large must b be to prove safety properties of a number of benchmarks.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
