在从样本轨迹中推断正式行为规范方面取得了实质性进展,例如使用线性时间逻辑(LTL)。 然而,这些技术无法处理正确描述具有随机行为的系统特征的规范,这些规范通常发生在强化学习和正式验证中。 我们考虑从一组马尔可夫链中推断概率LTL(PLTL)公式的布尔组合的被动学习问题,被归类为正或负。 我们提出了一种新的学习算法,该算法可以推断出简洁的PLTL规范,利用基于语法的枚举,搜索启发式,概率模型检查和布尔设置覆盖程序。 我们在两个用例中展示了我们算法的有效性:从RL算法诱导的策略中学习,并从概率模型的变体中学习。 在这两种情况下,我们的方法自动有效地提取PLTL规范,简明扼要地表征策略或模型变体之间的时间差异。
位置编码(PE)似乎是确保变压器的表达性不可或缺的;没有它们,变压器就会减少到一个词袋模型。 具有独特硬性注意力机制的NoPE-transformers(即没有PE)最近被证明只能表达常规语言,即计数能力有限。 本文表明,在平均硬注意力机制下,NoPE-transformers仍然具有令人惊讶的表现力:他们可以表达与多变量多项式方程(即)的非负整数解对应的计数语言。 双胍方程),推理哪些是众所周知的不可判定。 事实上,我们提供了平均硬注意力NoPE-Transformers(NoPE-AHATs)可表达的语言的精确表征:它们精确地对应于我们所说的半代数集合,即对多变量多项式方程系统的一组非负整数解决方案的有限结合。 我们获得了我们特征的几个有趣的后果。 首先,NoPE-transformers可以表达比简化计数机和Petri net等已建立的模型更复杂的计数属性,但不能表示PARITY的非常简单的计数属性。 其次,分析NoPE变压器的问题是不可决定的,例如,给定的NoPE变压器是否将一个类的所有输入字符串进行分类。 为了补充我们的结果,我们展示了一种计数语言,即使使用任意PE,平均硬注意力变压器也无法表达,但在电路复杂性类 TC^0, 回答一个开放问题中也可以表达。
我们提出了一个完整的理论和经验框架,将前馈神经网络作为通用的有限状态机器(N-FSM)。 我们的结果证明,有限深度的ReLU和阈值网络可以通过将状态过渡到深度神经层来精确模拟确定性有限自动机(DFA),具有所需的深度,宽度和状态压缩的正式特征。 我们证明DFA过渡是线性可分离的,二进制阈值激活允许指数压缩,Myhill-Nereode等效类可以嵌入到连续的潜在空间中,同时保持可分离性。 我们还将表达式边界形式化:固定深度前馈网络无法识别需要无边界内存的不规则语言。 与以前的基于指导或探索性的研究不同,我们提供了建设性的证明,并设计了明确的DFA未滚动的神经架构,这些架构在经验上验证了每一项主张。 我们的结果将深度学习、自动机理论和神经符号计算联系起来,为如何在连续的神经系统中实现离散符号过程提供了严格的蓝图。
基于仿真的构图抽象有效地缓解了模型检查中的状态空间爆炸,特别是对于计时系统。 然而,现有方法不支持广播同步,这是多组分系统中非阻塞对多通信进行建模的重要机制。 因此,它们也缺乏一个并行组成运算符,它同时支持广播同步、二进制同步、共享变量和提交位置。 为了解决这个问题,我们提出了一个基于模拟的计时系统组合抽象框架,该框架支持这些建模概念,并与流行的UPPAAL模型检查器兼容。 我们的框架是通用的,唯一的额外限制是,在接收广播信号时,禁止计时自动机更新共享变量。 通过两个案例研究,我们的框架展示了与传统单体方法相比卓越的验证效率。
在从样本轨迹中推断正式行为规范方面取得了实质性进展,例如使用线性时间逻辑(LTL)。 然而,这些技术无法处理正确描述具有随机行为的系统特征的规范,这些规范通常发生在强化学习和正式验证中。 我们考虑从一组马尔可夫链中推断概率LTL(PLTL)公式的布尔组合的被动学习问题,被归类为正或负。 我们提出了一种新的学习算法,该算法可以推断出简洁的PLTL规范,利用基于语法的枚举,搜索启发式,概率模型检查和布尔设置覆盖程序。 我们在两个用例中展示了我们算法的有效性:从RL算法诱导的策略中学习,并从概率模型的变体中学习。 在这两种情况下,我们的方法自动有效地提取PLTL规范,简明扼要地表征策略或模型变体之间的时间差异。
位置编码(PE)似乎是确保变压器的表达性不可或缺的;没有它们,变压器就会减少到一个词袋模型。 具有独特硬性注意力机制的NoPE-transformers(即没有PE)最近被证明只能表达常规语言,即计数能力有限。 本文表明,在平均硬注意力机制下,NoPE-transformers仍然具有令人惊讶的表现力:他们可以表达与多变量多项式方程(即)的非负整数解对应的计数语言。 双胍方程),推理哪些是众所周知的不可判定。 事实上,我们提供了平均硬注意力NoPE-Transformers(NoPE-AHATs)可表达的语言的精确表征:它们精确地对应于我们所说的半代数集合,即对多变量多项式方程系统的一组非负整数解决方案的有限结合。 我们获得了我们特征的几个有趣的后果。 首先,NoPE-transformers可以表达比简化计数机和Petri net等已建立的模型更复杂的计数属性,但不能表示PARITY的非常简单的计数属性。 其次,分析NoPE变压器的问题是不可决定的,例如,给定的NoPE变压器是否将一个类的所有输入字符串进行分类。 为了补充我们的结果,我们展示了一种计数语言,即使使用任意PE,平均硬注意力变压器也无法表达,但在电路复杂性类 TC^0, 回答一个开放问题中也可以表达。
常规单词语法是限制上下文无上下文语法,定义所有可识别的单词语言。 本文将常规语法从单词推广到某些类别的图形,通过为无序无排名的树和树width 2的图形定义常规语法。 限定词“常规”是合理的,因为这些语法精确地定义了各自图形类的可识别(等效的,CMSO-definable)集合。 常规和可识别的图形集之间的等效性证明依赖于在语法的大小双重指数的有效构建。 这为(EXPTIME-hard)问题设定了一个2EXPTIME上限,即将无上下文语言包含在常规语言中,最多用于树幅2的图形。 对常规语法的进一步语法限制足以精确地捕获最多树width 2的MSO可定义的图集,即CMSO公式定义的集合,没有基数约束。 此外,我们表明MSO-definability与具有周期性并行组合半组的代数的可识别性相吻合,对于由树幅上绑定定义的每类图形。
无限字母表上的正式语言是承载数据的结构和过程的抽象。 无限字母表上的自动模型,例如经典的寄存器自动机或等价称轨道有限自动机,除非对控制能力或寄存器数量施加严格限制,否则往往会有计算困难甚至不可判定的推理问题。 这已被证明在自动机模型中具有名称分配,例如常规的非确定性标称自动机,即使在无限多寄存器的情况下,也可以决定基本复杂性的语言包容性,同时保留合理的表达水平。 在执行本工作中,我们证明基本复杂性在将控制力扩展到交替下生存:我们引入了定期交替的名义自动机(RANA),并表明它们的非空性和包容性问题即使寄存器的数量不受限制,也具有基本的复杂性。 此外,我们表明, ANAs 允许几乎完全的去改变,特别是去改变,达到一个单一的僵持的普遍状态。 作为我们结果的必然结果,我们提高了模型检查Bar-μTL味道的复杂性,Bar-μTL是一种定点逻辑,通过有限数据词进行名称分配,通过指数级。
使用一套不同的还原策略,验证以 ω 常规语言表示的属性,如 LTL 可以从口吃不敏感中受益匪浅。 然而,由于使用LTL的neXt运算符或逻辑中的某种形式的计数,不是stutter不变的属性,一般这些技术不包括。 我们在本文中建议研究比口吃不敏感更弱的特性。 在口吃不敏感的语言中,将口吃添加到单词中不会改变它的接受度,任何口吃都可以被抽象出来;通过将这种等价关系分解为两个含义,我们获得了较弱的条件。 我们定义了一个缩短的不敏感语言,其中任何口吃小于语言单词的单词也必须属于语言。 延长不敏感语言具有双重属性。 然后引入一个半决策程序,以可靠地证明缩短不敏感特性,或拒绝延长不敏感特性,同时减少系统。 减少具有只能缩短运行的特性。 立顿的交易减少或 Petri 净集聚是符合资格的结构削减战略的例子。 我们还提出了一种方法,可以使用属性语言的分区将其口感不敏感,缩短不敏感,延长不敏感和长度敏感部件,即使在使用任意属性时仍然使用结构减少。 提供了实现和实验证据,表明大多数对口吃敏感的非随机性实际上正在缩短或延长不敏感。
我们提出了一个完整的理论和经验框架,将前馈神经网络作为通用的有限状态机器(N-FSM)。 我们的结果证明,有限深度的ReLU和阈值网络可以通过将状态过渡到深度神经层来精确模拟确定性有限自动机(DFA),具有所需的深度,宽度和状态压缩的正式特征。 我们证明DFA过渡是线性可分离的,二进制阈值激活允许指数压缩,Myhill-Nereode等效类可以嵌入到连续的潜在空间中,同时保持可分离性。 我们还将表达式边界形式化:固定深度前馈网络无法识别需要无边界内存的不规则语言。 与以前的基于指导或探索性的研究不同,我们提供了建设性的证明,并设计了明确的DFA未滚动的神经架构,这些架构在经验上验证了每一项主张。 我们的结果将深度学习、自动机理论和神经符号计算联系起来,为如何在连续的神经系统中实现离散符号过程提供了严格的蓝图。
基于仿真的构图抽象有效地缓解了模型检查中的状态空间爆炸,特别是对于计时系统。 然而,现有方法不支持广播同步,这是多组分系统中非阻塞对多通信进行建模的重要机制。 因此,它们也缺乏一个并行组成运算符,它同时支持广播同步、二进制同步、共享变量和提交位置。 为了解决这个问题,我们提出了一个基于模拟的计时系统组合抽象框架,该框架支持这些建模概念,并与流行的UPPAAL模型检查器兼容。 我们的框架是通用的,唯一的额外限制是,在接收广播信号时,禁止计时自动机更新共享变量。 通过两个案例研究,我们的框架展示了与传统单体方法相比卓越的验证效率。
量子计算是一个相对较新的计算领域,它利用量子力学的基本概念来处理数据。 摩尔等人的开创性论文。 [2000]引入了量子语法,其中一组振幅连接到每个生产。 然而,他们没有研究派生词的最终概率。 阿鲁贾等人 [2025]考虑了量子无上下文语法(QCFG)形成良好的条件,以确保派生词的概率不超过一个。 在本文中,我们提出了某些必要和充分的条件(也称为统一条件),以实现 QCFGs 的良好形成。
反向强化学习是从专家的最佳策略或演示中推断奖励函数的问题。 在这项工作中,假设奖励表示为奖励机器,其过渡依赖于与马尔可夫决策过程(MDP)状态相关的原子命题。 我们的目标是使用有限信息识别真正的奖励机器。 为此,我们首先介绍了前缀树策略的概念,该策略将作用的分布与MDP的每个状态和每个可实现的有限序列的原子命题相关联。 然后,我们描述了一个等价的奖励机器类,这些奖励机器可以在前缀树策略上识别。 最后,我们提出了一个基于SAT的算法,该算法使用从前缀树策略中提取的信息来解决奖励机器。 事实证明,如果已知前缀树策略足够(但有限)深度,我们的算法将恢复精确的奖励机器到等价类。 这种足够的深度作为MDP状态数的函数导出,(上限)奖励机器的状态数。 这些结果进一步扩展到我们只能从最佳政策中获得示威的情况。 几个例子,包括离散网格和块世界,连续状态空间机器人手臂,以及来自小鼠实验的真实数据,用于证明该方法的有效性和通用性。
让 d 是 0 到 4 之间的整数,W 是二进制字母 0, 1, 其中 h, w 在 Z > 0 上的二维字 h x w。 假设在 W 中每次出现的字母 1 都与最多 d 字母 1 相邻。 我们提供了一个精确的公式,用于固定(h,w)中可以在W中发生的字母1的最大数。 作为副产品,我们推断一个h x w矩形中包含的最大蛇多米诺骨架长度的上限。
在本文中,我们考虑块语言,即具有相同长度的单词集,我们提出了这些语言的新表示。 特别是,给定一个大小为k和长度l的字母表,一个块语言可以用长度k^l的位图表示,其中每个位表示相应的单词,根据词法顺序,是否属于该语言(分别等于1或0)。 首先,我们展示了如何将位图转换为确定性和非确定性的有限自动机,并且我们证明机器是最小的。 然后,我们分析足以接受确定性和非确定性情况下每个块语言的最大状态数。 最后,我们研究了这些语言上几种操作的确定性和非确定性状态的复杂性。 作为有限语言的子类,以有限语言闻名的操作状态复杂性的上限也适用于块语言。 然而,在几种情况下,发现了较小的值。
带有状态(VASS)的矢量添加系统,也称为Petri nets,是并发系统的流行模型。 许多领域的许多问题都归结为VASS的可到达性问题,VASS包括决定VASS的目标配置是否可以从给定的初始配置中达到。 在本文中,我们通过嵌套零测试获得VASS中可到达性问题的Ackermannian(原始递归在固定尺寸)上界。 此外,我们提供了一个统一的方法,它也可以以相同的复杂性决定大多数相关问题,例如半线性和可分离性。 对于其中一些问题,如半线性度,即使对于普通VASS来说,复杂性也是未知的。
更高维自动机(HDA)是一种形式主义,可以忠实地模拟并发系统的行为。 对于普通的自动机,正则表达式、正则语言和有限自动机之间存在对应关系,这提供了代数证明与操作行为之间的强大联系。 Fahrenberg等人已经表明,有限HDA对应于由顺序和并行组成和非空迭代生成的接口区间pomset语言,从而对应于具有并行组成的Kleene代数(KA)的变体。 众所周知,这种对应关系不能扩展到并发KA,其中还有进程复制。 有限HDA的替代方案是局部有限HDA,其中每个状态只能达到有限许多其他状态,并且有限分支HDA。 在本文中,我们展示了HDA的两类在过程复制下都是封闭的,因此是并发KA的模型。 为了实现这一目标,我们证明HDA的类别在本地有限呈现,其中有限HDA生成所有其他HDA。 然后我们证明这有一个不幸的副作用,即所有的HDA都是局部有限的,这意味着与并发KA的对应关系微不足道。 同样,我们也表明,即使有限分支HDA在过程复制下关闭,生成的HDA必然具有无限多的初始状态。
量子指纹识别是一种将经典输入词映射到量子态的技术。 获得的量子态比原词短得多,其处理使用的资源更少,使其在量子算法、通信和密码学中有用。 量子指纹识别的一个例子是MOD_p={a^i· p| i ≥ 0} 语言的量子自动算法,其中p是一个质数。 然而,在当前量子硬件上实现这样的自动机效率不高。 量子指纹识别将长度 n 的字 x ∈{0,1}^n 映射到 O(log n) qubits 的状态 |ψ(x)⟩,并使用 O(n) 统一操作。 由于大量的量子操作,使用当前量子计算机的所有可用量子位计算量子指纹是不可行的。 为了让量子指纹识别实用,我们应该优化电路的深度而不是宽度,而不是与以前的作品相反。 我们提出了基于添加剂组合学工具(如广义算术进展(GAP))的量子指纹识别的明确方法,并证明这些方法提供了与概率方法相媲美的电路深度。 我们还将我们的方法与先前关于显式量子指纹识别方法的工作进行比较。
非通勤变量Σ中关于理性变量Σ的正文序列是映射 Σ^* →Q。 我们说,如果输出中的值不依赖于输入中符号的顺序,则序列是交换的。 类序列的交换性问题作为类的输入(有限呈现)序列,相当于确定它是否是交换的。 这是一个非常自然,尽管是非平凡的问题,以前没有从算法的角度考虑。 我们表明,对于构成所谓有效敷衍的所有类别的系列,可对重组是可判定的,这一概念概括了 Reutenauer 的形式系列。 例如,由Schützenberger在20世纪60年代引入的理性序列类是众所周知的有效(前)品种,因此对等是可决定的。 为了展示我们的结果的适用性,我们考虑正式系列的课程,概括理性。 我们考虑多项式自动机,洗牌自动机和渗透自动机,我们表明这些模型中的每一个都识别了正式系列的有效易用性。 因此,他们的交换问题是可决定的,这是一个新颖的结果。 我们发现,对于这些不同的计算模型,可以以统一的方式决定对交换性。 最后,我们介绍了形式系列理论之外的对向量的应用。 我们表明,我们可以在序列和功率序列中为代数差和微分方程的受限类决定可溶性,对于这些问题,这些问题在完全通用性上是不可决定的。 多亏了这一点,我们可以证明多变量多项式递归序列和可构造微分代数功率序列的语法是有效的,这是以前工作中留下的新结果。
在本文中,我们介绍了LTL的新团队语义,灵感来自好奇的逻辑。 由此产生的逻辑的主要特征,我们称之为InqLTL,是对暗示的直觉解释和分离的布尔语义。 我们表明,与布尔否定的InqLTL高度不可判定,并且严格来说比带有布尔否定的TeamLTL更不具有表现力。 在积极的一面,我们确定了InqLTL的一个有意义的片段,具有可判定的模型检查问题,可以表达相关的超属性类别。 据我们所知,这个片段代表了第一个超逻辑,具有可判定的模型检查问题,允许不受限制地使用时间模式和对痕迹进行普遍的二阶量化。
交替均等自动机(APA)为模拟无限行为提供了强大的形式主义,并在正式验证中发挥着核心作用。 尽管它们被广泛使用,但APA背后的代数理论在很大程度上仍未被探索。 在最近的工作中,引入了一个非确定性有限自动机(NFA)的符号,以及通过右线性代数对其方程理论进行声音和完全的公理化。 在本文中,我们将这一行工作扩展到无限单词的设置。 我们提出了双倍化的语法,根据右线性晶格表达式为APA生成符号,并就其方程理论相对于ω-正则语言的标准语言模型提供了自然公理化。 这种公理化的设计是以定点逻辑理论为指导的;事实上,完整性因素通过线性时间μ微积分的完整性而干净。
FC是一个一阶逻辑,它使用连接来推理有限词的所有因素,并且可以定义像所有平方(ww)这样的非常规语言。 在本文中,我们确定有常规语言不是FC定义的。 此外,我们在代数、自动机和正则表达式方面给出了 FC 定义的常规语言的可判定特征。 后者自然而简洁:无星的广义正则表达式与终端单词的Kleene星扩展。
我们提出了NFA册封问题的新视角,引入了中间最小化步骤,以减少飞行中的探索空间。 我们的方法必不可少的是所谓的等效注册表,它管理有关等效状态的信息,并允许采用进一步的优化技术,如凸闭包或模拟来提高性能。 由于我们方法的通用性,这些概念可以嵌入到经典的子集构造或Brzozowski的方法中。 我们根据自动序列的一组真实世界示例来评估我们的方法,并观察到我们能够改进特别是最坏情况。 我们在开源库中实现我们的方法,供用户尝试。
双相化对于验证概率系统中的过程等效性至关重要。 本文提出了一种新的逻辑框架,用于分析概率参数化系统中的双相,即有限状态概率系统的无限家族。 我们的框架建立在常规结构的第一顺序理论之上,它为推理这些系统提供了一个可判定的逻辑。 我们表明,匿名和统一等基本属性可以在这个框架内进行编码和验证,以符合演绎软件验证原则的方式,其中系统,属性和证明以统一的可判定逻辑表示。 通过集成语言推理技术,我们在合成候选人双相证明的匿名性和统一性方面实现了完全自动化。 我们通过解决几个具有挑战性的例子来证明我们方法的有效性,包括密码协议和随机算法,这些算法以前是完全自动化方法所无法企及的。