二元自动机的可计算外壳：多项式时间解决方案

"这篇论文探讨了二元自动机的A_（？）ne壳在多项式时间内的计算问题，特别是如何有效地处理无限状态系统的表示。文章介绍了二元自动机的新表示，这是一种对Nm子集的扩展，类似于NDD（Nested Depth-First Automata或Deterministic Nested Word Automata）。作者证明了在多项式时间内可以计算二元自动机表示的向量集的外壳，这在处理无限集合时具有重要意义。此外，论文还应用这一结果证明了包括计数器系统、广播协议、重置/转移Petri网和线性系统在内的多种理论计算模型，在多项式时间内是可计算的。文章涉及的关键词有Presburger算术、布尔壳、NDD以及二元自动机等。" 正文: 在理论计算机科学中，无限状态系统是那些其可达状态集合可能无限大的系统，这使得直接枚举所有状态变得不切实际。为了解决这个问题，研究者发展了各种符号模型检查技术，比如使用二元自动机（Binary Automata）和NDD（Nested Depth-First Automata或Deterministic Nested Word Automata）来有效地表示和操作这些无限集合。 NDD是一种强大的表示工具，它被用于各种符号模型检查器，如FAST、LASH和BABYLON。这些工具通常分析计数器系统，其中每个动作都由一个NDD来表示，这个NDD定义了能够触发该动作的配置集。NDD的特殊之处在于它们能够表达复杂的状态空间结构，特别是那些与子词关系和上下文无关语言相关的结构。 在本文中，作者Jérôme Leroux提出了一个新的二元自动机类，它自然地扩展了NDD的概念，并且证明了这个扩展的二元自动机的外壳（一种集合的简化表示）可以在多项式时间内计算。这个结果对于处理无限状态系统来说是一个重大突破，因为它允许更有效率地分析和理解系统的性质。 作者进一步展示了这个计算结果的应用，例如在计数器系统中的应用。计数器系统是一类抽象的计算模型，它们包括广播协议、重置/转移Petri网和线性系统等。通过在多项式时间内计算这些系统的外壳，我们可以快速地决定系统的某些属性，如一致性、安全性和可达性。 此外，Presburger算术是本文中的一个重要概念，它是一种一阶逻辑，用于处理整数的加法和比较，而不使用乘法。布尔壳则可能指的是用布尔代数来描述系统状态集合的边界或限制。这些理论工具的结合使得对二元自动机的外壳进行有效的计算成为可能，进而推动了对无限状态系统的研究。 这篇论文在理论计算机科学领域提供了新的见解，特别是在处理无限状态系统和复杂自动机表示方面。通过引入新的二元自动机表示和证明多项式时间内的计算方法，它为模型检查和验证工具的设计提供了理论基础，有助于解决实际工程和计算问题。