Weak morphisms of higher dimensional automata
我们引入了高维自动机的弱态射，并利用它们定义了高维自动机的预序关系，其中包括同胚抽象和迹等价抽象。结果表明，同胚抽象本质上总是强于迹等价抽象。我们还定义了跟踪语言的HDA，并表明，对于一大类HDA，它是不变的跟踪等效抽象。
2013-03-08 cs.FL math.AT
Ultimate Traces of Cellular Automata
元胞自动机（CA）是一种并行同步计算模型，它由有限个自动机（元胞）并置组成，其状态根据其邻居的状态进行演化。它的迹是代表某个特定细胞所取的状态序列的无限字的集合。本文研究了CA和部分CA（CA限制于特定子移位）的最终迹。最终的痕迹是在CA长时间运行后观察到的痕迹。我们给出了一组无限字是某个CA的迹的充分条件，并证明了迹上所有性质的不可判定性，这些迹是通过最终重合而稳定的。
2011-02-12 cs.DM cs.FL nlin.CG
Learning Moore Machines from Input-Output Traces
Aalto University（阿尔托大学）；University of California, Berkeley（加州大学伯克利分校）
从示例轨迹（但没有等价或成员查询）学习自动机的问题是自动机学习理论和实践的基础。在本文中，我们研究这个问题的有限状态机的输入和输出，特别是摩尔机。我们提出了三种算法来解决这个问题：（1）PTAP算法，它将一组输入输出迹线转化为一个不完全的Moore机，然后用自循环来完成这个Moore机;（2）PRPNI算法，它使用著名的RPNI算法来学习一个编码Moore机的自动机的乘积;（3）MooreMI算法，该算法使用扩展了状态合并的PTAP直接学习Moore机。证明了MooreMI在极限性质上具有基本的一致性。我们还比较了算法实验方面的学习机器的大小和几个概念的准确性，本文介绍。最后，我们比较OSTIA，学习更一般的传感器类的算法，并发现OSTIA一般不学习摩尔机，即使当美联储的特征样本。
2016-09-02 cs.FL cs.LG
Trace Complexity of Chaotic Reversible Cellular Automata
Delvenne、Kürka和Blondel为任意符号系统定义了计算复杂性的新概念，并给出了在这个意义上计算通用的有效系统的例子。这个概念是根据系统的迹函数定义的，目的是捕捉其动态。我们提出了一个Devaney混沌可逆细胞自动机，在他们的意义上是普遍的，回答了一个问题，他们明确地离开开放。我们还讨论了一些建设的影响和局限性。
2014-04-17 cs.FL math.DS
Direct Construction of Program Alignment Automata for Equivalence Checking
检查两个程序在语义上是否等价的问题有着广泛的应用，因此具有非常重要的意义。有几种技术可以解决这个问题，主要是通过构建一个产品程序，使其更容易获得有用的不变量。一个新的除了这些是一种技术，使用对齐谓词来对齐两个程序的痕迹，以构建一个程序对齐自动机。由谓词引导不仅有利于处理句法差异，而且有利于保持与属性的相关性。然而，基于跟踪的技术也存在缺点。获得覆盖所有程序行为的跟踪是困难的，并且任何欠近似都可能导致不完整的产品程序。此外，这种间接结构不知道缺失的行为，并且无法控制上述不完整性。针对这些问题，本文提出了一种直接构造程序对齐自动机的算法。
2021-09-04 cs.FL cs.SE
Dynamic Input/Output Automata: a Formal and Compositional Model for Dynamic Systems
我们提出了动态I/O自动机（DIOA），动态系统的组合模型。在DIOA中，随着计算的进行，自动机可以动态地创建和销毁，并且自动机可以动态地改变其签名，即，它可以参与的一系列行动。DIOA具有用于并行组合、操作隐藏、操作重命名的操作符、自动机创建的概念以及通过跟踪包含的行为子类型的概念。DIOA可以使用签名修改来建模移动性，并且是分层的：一个动态变化的交互自动机系统本身被建模为单个自动机。我们还表明，并行组成，行动隐藏，行动重命名，和（受一些技术条件）自动机的创建都是单调的轨迹包含：如果一个组件被替换为另一个的痕迹是前者的一个子集，那么作为一个整体的系统的痕迹集只能减少。
2016-04-20 cs.DC cs.FL
Proving Safety with Trace Automata and Bounded Model Checking
循环欠近似是一种技术，它通过额外的分支来丰富C程序，这些分支代表了（有限的）循环迭代范围的效果。虽然这种技术可以显著地加速错误的检测，但它引入了冗余的执行跟踪，这可能使程序的验证复杂化。这对于基于有界模型检验的验证工具尤其如此，该工具结合了简化的算法来确定是否已经考虑了循环的所有可行迭代。我们提出了一种技术，使用\emph{trace automata}，以消除执行循环加速后的冗余执行。该方法减小了分析下的程序的直径，这在某些情况下足以允许使用有界模型检验的安全性证明。我们的转换是精确的-它不会引入假阳性，也不会掩盖任何错误。我们已经实现了分析作为一个源到源的转换，并提出了实验结果显示该技术的适用性。
2014-10-21 cs.FL cs.LO cs.PL
Inference of Deterministic Finite Automata via Q-Learning
Universität zu Lübeck（吕贝克大学）
本文提出用 Q-learning 被动推断 DFA，将学习到的 Q 函数重解释为有限域上的转移函数，从而连接强化学习与符号自动机表示，并通过示例验证可行性。
2025-10-20 cs.AI cs.FL
String Diagrammatic Trace Theory
本文将幺半范畴中的形式语言理论扩展至多类对称情形，通过引入对称幺半自动机统一了 Mazurkiewicz 迹语言与 Zielonka 异步自动机，并利用字符串图推导迹的串行化。
2023-06-28 cs.FL math.CT
A Myhill-Nerode Theorem for Register Automata and Symbolic Trace Languages
我们提出了一个新的符号跟踪语义寄存器自动机（扩展的有限状态机），它记录的输入符号，在运行过程中发生的序列，以及输入参数的约束，由这个运行。我们的主要结果是一个推广的经典Myhill-Nerode定理，这个符号设置。我们的推广需要使用三个关系来捕捉寄存器自动机的附加结构。位置等价$\equiv_l$捕获符号轨迹在相同位置结束，转换等价$\equiv_t$捕获它们共享相同的最终转换，并且部分等价关系$\equiv_r$捕获符号值$v$和$v'$分别在符号轨迹$w$和$w'$之后存储在相同寄存器中。如果存在满足一定条件的关系$\equiv_l$，$\equiv_t$和$\equiv_r$，特别是它们都有有限索引，则符号语言被定义为正则语言.我们表明，符号语言相关的寄存器自动机是定期的，我们构造，为每个定期符号语言，一个寄存器自动机，接受这种语言。我们的研究结果提供了一个灰盒学习算法的基础，在设置中，数据参数的约束可以从代码中提取，例如符号/concolic执行或污染的工具。我们相信，转移到灰盒设置是必不可少的，以克服国家的最先进的黑盒学习算法的可扩展性问题。
2021-03-31 cs.FL cs.LO
Quantum Turing automata
在有限维希尔伯特空间的匕首紧闭范畴中定义了具有量子控制的量子图灵机的指称语义。利用Moore-Penrose广义逆，在此范畴对等距的限制上引入了一个新的可加迹，并将其推广到作为Monoidal自动机的有向量子图灵机上.然后使用Joyal-Street-Verity Int构造将该结构扩展为可逆双向结构。
2014-04-01 cs.FL cs.IT math.IT
Multi-Buffer Simulations for Trace Language Inclusion
我们认为模拟游戏之间的破坏者和复制两个Büchi自动机，其中的选择由破坏者可以缓冲复制在几个缓冲区之前，她执行他们对她的结构。我们表明，模拟游戏是有用的，以近似包含跟踪封闭的语言接受有限状态自动机，这是已知的不可判定的。我们研究的可判定性和复杂性，并表明，有界缓冲区的游戏可以决定在多项式时间，而一个无界和一个有界缓冲区的游戏是高度不可判定的。我们还显示了一些充分条件的自动机复制器赢得比赛（无界缓冲区）。
2016-09-14 cs.FL cs.LO
Are Agents Probabilistic Automata? A Trace-Based, Memory-Constrained Theory of Agentic AI
JetBrains Research, Amsterdam, the Netherlands（JetBrains研究院，荷兰阿姆斯特丹）；Delft University of Technology, Delft, the Netherlands（代尔夫特理工大学，荷兰代尔夫特）；Constructor University, Bremen, Germany（Constructor大学，德国不来梅）
本文提出了一种基于轨迹的、内存受限的智能体AI理论，通过自动机理论模型分析智能体与环境交互行为的概率分布，并探讨了不同内存限制下轨迹语言的可判定性。
2026-01-30 cs.AI cs.FL
Automata for Hyperlanguages
Department of Computer Science, Iowa State University（爱荷华州立大学计算机科学系）；Department of Software Engineering, ORT Braude College（ORT布拉德学院软件工程系）
超属性将常规的跟踪属性从一组执行跟踪提升到一组执行跟踪。超性质已被证明是一个强大的形式主义表达和推理的信息流安全策略和重要属性的网络物理系统，如灵敏度和鲁棒性，以及在分布式计算的一致性条件，如线性化。虽然有一个广泛的机构的工作自动机为基础的表示跟踪属性，我们目前缺乏这样的表征hyperproperties。我们引入超自动机的EM超语言，这是语言的话集。本质上，超自动机允许在自动机上运行多个量化的单词。我们提出了一种特定类型的超自动机，称为非确定性有限超自动机（NFH），它接受常规超语言。我们证明了正则超语言表达有限迹的超性质的能力。然后，我们探讨了NFH的基本性质，并显示其封闭下的布尔运算。我们表明，虽然nonempty是不可判定的一般情况下，它是可判定的几个片段的NFH。我们进一步证明了有限集和NFH的正则语言的成员问题的可判定性，以及NFH的几个片段的包含问题。最后，我们介绍了学习算法的基础上的Angluin的L-星算法的片段NFH的量化是严格的普遍或严格存在的。
2020-02-23 cs.CL cs.FL
Canonical Representations of k-Safety Hyperproperties
超属性将跟踪属性的传统观点从跟踪集合提升到跟踪集合的集合，并提供了一种表达信息流策略的形式。对于迹属性，用于验证、监控和合成的算法通常基于将属性表示为ω-自动机。对于超性质，一个类似的，规范的自动机理论表示是，到目前为止，失踪。这对于算法的发展是一个严重的障碍，因为基本的构造，例如学习算法，不能被应用。在本文中，我们提出了一个典型的表示，广泛使用的一类正规k-安全超性质，其中包括重要的政策，如不干涉。我们证明了正则k-安全超性质S可以用一个有限自动机来表示，其中自动机接受的每个字都表示对S的违反。该表示提供了一个自动机理论的方法，定期k-安全超性质，并允许我们比较定期k-安全超性质，简化它们，并学习这样的超性质。我们研究了一般情况下和从HyperLTL中的公式构造正则k-安全超性质自动机的问题，并给出了不同平移的复杂性界。在确定性有限自动机L* 学习算法的基础上，提出了正则k-安全超性质的学习算法.
2020-12-29 cs.FL cs.LO
Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction
本文研究了实时的【形】系统的安全性验证与综合问题。我们介绍实时的【形】程序，这些程序由可以执行离散和实值变量赋值的指令组成。它们足够通用，可以捕获有趣的时间系统类，如时间自动机，秒表自动机，时间（d）Petri网和混合自动机。我们提出了一种使用轨迹抽象细化的半算法来解决实时的【形】程序的可达性验证问题和参数综合问题。所有提出的算法已经实施，我们已经进行了一系列的实验，比较我们的新方法的性能，以国家的最先进的工具，在经典的可达性，鲁棒性分析和参数合成定时系统。我们表明，我们的新方法提供了解决方案，这些问题是无法解决的，目前最先进的工具。
2020-07-21 cs.FL cs.LO cs.SY
Automata-less Monitoring via Trace-Checking (Extended Version)
Department of Mathematics, Computer Science and Physics University of Udine（乌迪内大学数学、计算机与物理系）
针对运行时验证中DFA监控器双指数爆炸问题，提出基于内蕴安全/共安全公式的迹检查监控方法，复杂度为多项式级，并明确了LTL和LTLf中识别这类公式的复杂度。
2025-11-14 cs.FL cs.LO
Combining Partial Specifications using Alternating Interface Automata
为了对真实世界的软件系统进行建模，建模范式应该支持某种形式的组合性。在接口理论和基于模型的输入和输出测试中，已经引入了合取算子：组合规范s1 $\wedge$ s2所允许的行为是部分模型s1和s2所允许的行为。手头的模型是非确定性接口自动机，但非确定性和连接之间的相互作用还没有得到很好的理解。另一方面，在交替自动机理论中，合取和非确定性是其核心内容。交替自动机没有被认为是在输入和输出的上下文中，使它们不太适合建模软件接口。在本文中，我们结合这两种建模范式定义交替接口自动机（AIA）。我们装备这些自动机与观察，跟踪为基础的语义，并定义测试人员，建立正确的黑盒接口相对于AIA规范。
2020-02-20 cs.FL
Efficient reduction of nondeterministic automata with application to language inclusion testing
本文提出高效缩减非确定性Büchi和有限词自动机规模的算法，通过剪枝、饱和及商化技术，并利用前瞻模拟近似迹包含，从而解决更大规模的语言包含等PSPACE完全问题，实验显示性能优于现有工具GOAL。
2019-02-12 cs.FL cs.LO
Asynchronous wreath product and cascade decompositions for concurrent behaviours
本文提出异步 wreath 积和级联分解等代数工具，用于分析 Mazurkiewicz 迹语言和异步自动机，推广 Krohn-Rhodes 定理，并应用于一阶逻辑可定义迹语言的表征。
2022-06-27 cs.FL
Relating Alternating Relations for Conformance and Refinement
对于具有输入和输出的状态转换系统，已经定义了各种关系来表示精化和一致性，例如基于模型的测试领域中的ioco和uioco，以及源自博弈论和形式化验证的交替模拟和交替跟踪包含。几篇论文比较了这些独立开发的关系，但这些比较做出了假设（例如，输入使能性），造成限制（例如，决定论-那么它们都一致），使用不同的模型（例如，接口自动机和Kripke结构），或者不处理静止的概念。在本文中，我们提出了集成的ioco/uioco理论的基于模型的测试和理论的交替细化，在域的非确定性，非输入启用接口自动机。一个长期的猜测是ioco和交替跟踪遏制一致。我们的主要结果是，这个猜想并不成立，但uioco符合交替跟踪包容的一个变种，图像有限接口自动机和明确的治疗静止。从ioco理论和交替细化之间的比较，我们得出结论，ioco和原来的关系的交替跟踪包含是太强的现实黑盒场景。本文提出了一个精化关系，它既能表示博弈论中的uioco，又能表示精化，而且更简单，具有更清晰的观察解释。
2019-09-30 cs.FL
CEDAR: Automata as Verifiable Interfaces for Language-Guided Embodied Action
University of Colorado Boulder（科罗拉多大学博尔德分校）
提出 CEDAR 框架，将具身智能体的自然语言指令转化为正则语言并表示为确定有限自动机，在 Minecraft 中可维持基线无法保留的时空约束并减少 LLM 查询，提供了实用的验证层。
2026-08-31 cs.AI cs.CL cs.FL
Active Learning of Abstract System Models from Traces using Model Checking [Extended]
我们提出了一种新的主动模型学习方法来生成抽象的系统实现，有限状态自动机（FSA），从执行轨迹。给定一个实现和一组可观察的系统变量，生成的自动机承认给定变量上的所有系统行为，并以保持实现的不变量的形式提供有用的见解。为了实现这一点，所提出的方法使用一个可插拔的模型学习组件，可以从一组给定的跟踪生成FSA。然后从正在构建的FSA中提取编码完整性假设的条件，并使用软件模型检验通过检查其真值来评估其完整性程度。这会生成新的轨迹，以表达任何缺失的行为。新的跟踪数据用于迭代地细化抽象，直到所有系统行为都被学习的抽象所接受。为了评估这种方法，我们逆向工程一组公开的Simulink Stateflow模型，从他们的C实现。
2021-12-11 cs.FL cs.LO
Conservative Hybrid Automata from Development Artifacts
验证在安全关键环境中运行的网络物理系统需要正式的系统模型。验证的有效性取决于模型的精度：模型中未捕获的可能行为可能导致正式验证，但不安全的系统。然而，手动构造是微妙的，容易出错，而自动构造不能扩展到大型复杂的系统。作为一种补救措施，本文设计了一种自动构建算法，利用包含在文物的开发过程中的信息：运行时监控规范和记录的测试痕迹。这些工件不会产生额外的成本，并提供足够的信息，以便构建过程可以很好地扩展到大型系统。该算法使用自上而下和自下而上的结构之间的混合方法，该方法允许证明结果保守，同时限制过度近似的水平。
2022-01-21 cs.FL
Efficient Runtime Verification of Real-Time Systems under Parametric Communication Delays
针对实时系统观测中存在参数化通信延迟导致传统在线监控不可靠的问题，提出基于zone的精确处理算法，在UPPAAL上实现并取得良好初步结果。
2025-07-29 cs.FL
Reactive Synthesis for DECLARE via symbolic automata
给定一个规范的线性时间的时间逻辑解释有限的痕迹（LTLf），反应性合成问题要求找到一个有限表示的，终止控制器的反应，以执行所需的系统规范的不可控的行动的环境。在本文中，我们研究，第一次，反应性的综合问题，DEQUE-一个片段的LTLf广泛用于在理论和实践中指定声明性的，基于约束的业务流程。我们提供三方面的贡献。首先，我们给出了一个朴素的，双指数时间综合算法。第二，我们展示了如何任意的DEPENE规范可以compensarily编码成一个等价的纯过去的LTLf，我们利用这一点来定义一个优化的，单指数时间算法DEPENE合成。第三，我们推导出一个符号版本的算法，通过引入一个新的翻译纯过去的时间公式符号确定性有限自动机。
2022-12-21 cs.FL cs.LO
On the Power of Automata Minimization in Reactive Synthesis
在人工智能应用中，时态逻辑经常被用来描述时态属性。最流行的语言是线性时态逻辑（Linear Temporal Logic，LTL）。最近，有限迹上的LTL，LTLf，已经在几种情况下进行了研究。为了对LTLf进行推理，通常将公式编译成确定性有限自动机（DFA），作为中间语义表示。此外，由于DFA具有规范表示的事实，可以应用有效的最小化算法来最大限度地减少DFA大小，从而有助于加速后续计算。在这里，我们提出了一个深入的调查两个经典的最小化算法，即Hopcroft和Brzozowski算法。更具体地说，我们展示了如何将这些算法应用于半符号（显式状态，符号转换函数）自动机表示。然后，我们比较这两种算法的上下文中的LTLf合成框架，从LTLf公式。虽然早期的研究比较两种算法从随机生成的自动机的结论是，没有算法占主导地位，我们的研究结果表明，从LTLf公式，Hopcroft的算法是最好的选择，在反应合成的背景下。更深入的分析解释了为什么Brzozowski算法的假定优势在实践中没有实现。
2021-09-17 cs.FL
Complete Compositional Syntax for Finite Transducers on Finite and Bi-Infinite Words
本文提出以有限状态非确定性传感器统一自动机理论、迁移系统与sofic子移位，并给出带可靠改写规则的组合图解语法，证明其等式理论完全性。
2025-02-10 cs.DM cs.FL cs.LO
Infinite Trace Objectives with Finite Trace Techniques: Translating LTL to LTLf+
本研究提出首个从LTL到LTLf+的线性转换方法，将LTL归一化为Manna-Pnueli层次的反应片段，保留LTLf+的优势且无渐近代价，可将LTLf+技术应用于更多AI问题。
2026-08-04 cs.AI cs.FL cs.LO
