Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages
并发Kleene代数（CKA）是一种研究具有并发行为的程序的数学形式。与Kleene代数以前的扩展一样，描述自由模型对于发展理论基础和潜在应用至关重要。对于CKA来说，这几年来一直是一个悬而未决的问题，本文朝着答案迈出了重要的一步。我们提出了一个新的自动机模型和Kleene定理，涉及到一个宽松的版本的CKA串并行pomset语言，这是一个自然的候选人的自由模型。与以前的工作有两个实质性的区别：从表达式到自动机，我们使用Brzozowski衍生物，这使得直接建设的自动机;从自动机到表达式，我们提供了一个句法表征的自动机，表示有效的CKA行为。
2017-10-22 cs.FL cs.LO
Interpreted Higher-Dimensional Automata for Concurrent Discrete-Event Control
SAMOVAR, Télécom SudParis, Institut Polytechnique de Paris（巴黎理工学院）；Université Paris-Saclay, ENS Paris-Saclay, LURPA（巴黎萨克雷大学）
本文提出利用高维自动机框架将解释性Petri网转换为闭环控制器，并识别隐藏的模糊或矛盾规范。通过虚拟环境验证了方法的可行性。
2026-03-23 cs.FL
Reachability Analysis of Reversal-bounded Automata on Series-Parallel Graphs
字符串上的有限状态自动机的扩展，如多头自动机或多计数器自动机，已成功地用于编码许多无限状态非正则验证问题。在本文中，我们考虑一个推广的自动机理论的无限状态验证从字符串标记串并行图。我们定义了一个模型的非确定性，2路，并发自动机工作串并行图和通信通过共享寄存器的节点上的图形。我们考虑以下验证问题：给定一个系列的串并行图描述的上下文无关的图转换系统（GTS），并在串并行图的并发自动机，是一些图所产生的GTS接受的自动机？一般的问题是不可判定的已经（单向）多头自动机字符串。我们表明，一个有界的版本，其中自动机使固定数量的反转沿图，并使用固定数量的共享寄存器是可判定的，即使有没有约束的GTS生成的串并行图的大小。我们的可判定性结果是基于建立上下文切换的数量是有界的，并对有界并发自动机的计算进行编码，以将空性问题减少到下推自动机的空性问题。
2015-09-24 cs.FL
Bisimulations and Logics for Higher-Dimensional Automata
Norwegian University of Science and Technology（挪威科技大学）；University of Warsaw（华沙大学）；EPITA Research Lab（EPITA研究实验室）
本文提出Ipomset模态逻辑，用于刻画HDAs中的路径双向模拟，并定义单元双向模拟及其与标准双向模拟的关系。
2024-11-11 cs.FL cs.LO
On Series-Parallel Pomset Languages: Rationality, Context-Freeness and Automata
并发Kleene代数（CKA）是研究并发程序的一种形式化方法.像以前的Kleene代数扩展一样，开发指称和操作视角之间的对应关系对于基础和应用都很重要。本文采取了重要的一步，这样的对应关系，通过精确的双Kleene代数（BKA），CKA的一个片段，一种新型的自动机，pomset自动机（PAs）。我们表明，PA可以实现BKA语义的串并行的理性表达式，一类PA可以被翻译回这些表达式。我们还讨论了一般PA的上下文无关的pomset文法的行为，因此，普遍性，等价性和串并行合理性的一般PA是不可判定的。
2018-12-14 cs.FL
Leafy Automata for Higher-Order Concurrency
有限理想化并发算法（Finitary Idealized Concurrent Algol，FICA）是一种结合了函数式、命令式和并发计算的原型程序设计语言。存在一个完全抽象的FICA博弈模型，原则上可以用来证明FICA程序的等价性和安全性。不幸的是，这些问题对于整个语言来说都是不可判定的，并且只知道非常基本的可判定子语言。我们提出叶自动机作为一个专门的自动机理论的形式主义表示游戏语义的FICA。自动机使用具有树结构无限字母表。我们表明，游戏语义的任何FICA长期可以表示的痕迹，一个树叶自动机。相反，任何叶子自动机的迹都可以用FICA项表示。由于与FICA的密切匹配，我们认为叶自动机作为一个很有前途的起点，寻找可判定的语言子类，更一般地说，提供了一个新的视角高阶并发计算模型。此外，我们确定了一个片段的FICA，是适合验证翻译成一个特定的类叶自动机。使用后一类的局部性，其中级别之间的通信是有限的，每隔一级有界的，我们表明，他们的空虚问题是可判定的减少到Petri网的可达性。
2021-01-21 cs.FL cs.PL
On the topology of concurrent systems
本文证明了高维自动机作为并发系统的组合拓扑模型，对于每个非空连通多面体，都存在一个共享变量系统，其状态空间的高维自动机模型具有该多面体的同伦类型。
2024-04-25 cs.FL cs.LO math.AT
Non-Sequential Theory of Distributed Systems
这些课堂讲稿涵盖了并发和分布式系统的建模和验证的基本自动机理论概念和逻辑形式。这些概念中的许多自然地扩展了经典的自动机和逻辑，这些概念为建模顺序系统提供了一个框架。另一方面，分布式系统结合了几个（有限或递归）过程，因此将被建模为（分别为有限或下推）自动机的集合。分布式系统的一个关键参数是进程之间允许的交互类型。在这堂课中，我们将重点讨论消息传递范式。通常，分布式系统中的通信在事件之间创建复杂的依赖关系，当使用顺序的操作语义时，这些依赖关系被隐藏。这里采取的方法是基于忠实地保留并发事件的依赖关系。也就是说，系统的执行被建模为偏序或图，而不是事件序列。
2021-10-17 cs.FL cs.LO
Asynchronous wreath product and cascade decompositions for concurrent behaviours
本文提出异步 wreath 积和级联分解等代数工具，用于分析 Mazurkiewicz 迹语言和异步自动机，推广 Krohn-Rhodes 定理，并应用于一阶逻辑可定义迹语言的表征。
2022-06-27 cs.FL
Saturating automata for game semantics
提出基于无穷字母表的饱和自动机模型，将FICA有限片段翻译为该自动机以有效建模高阶并发，保证饱和性质且对范式项实现多项式时间内的线性规模构造。
2023-11-18 cs.FL cs.PL
Better Automata through Process Algebra
本文展示了如何使用结构操作语义（SOS）的风格推广的进程代数社区可以导致一个更简洁和有用的建设有限自动机从正则表达式。这样的构造已经知道了几十年，并且形成了Kleene定理的一个方向的证明的基础。新的建设的目的是，一方面，向学生展示如何小自动机可以构建，而不需要空的过渡，另一方面，以显示如何建设方法承认关闭证明正则语言相对于其他运营商以及。这些结果，虽然在理论上并不令人惊讶，但指出了过程代数研究的额外影响：除了提供对并发计算性质的基本见解之外，它还为自动机理论中的旧的，众所周知的结构提供了新的见解。
2020-02-18 cs.FL
Order-2 bygone-state opacity of labeled finite-state automata
School of Mathematics and Statistics（数学与统计学院）；Xi’an Jiaotong University（西安交通大学）
提出二阶过往状态不透明性概念，描述一个代理无法确定另一代理能否根据当前及过去观测唯一确定自动机状态，并通过并发组合和经典观察器在双指数时间内验证该性质。
2026-06-26 cs.CC cs.FL
Forkable Regular Expressions
我们认为forkable正则表达式，丰富了正则表达式的fork操作符，建立一个正式的基础，静态和动态分析的并发程序的通信行为。我们定义了一个新的组合语义forkable表达式，建立其基本属性，并定义衍生工具，为他们的自动机的生成，匹配，和语言的包容性测试的基础。可分叉表达式可能会产生非正则语言，在一般情况下，但我们确定的表达式，保证有限的自动机建设通过衍生物的充分条件。
2015-12-08 cs.FL cs.LO cs.PL
Label Cuts in Layered Automata: Short Explanations for the Regular Constraint
Southern University of Science and Technology（南方科技大学）；Guangdong Police College（广东警官学院）
本文研究 Regular 约束的 LCG 解释，证明值删除解释等价于分层 DFA 的标签 s-t 割，确立最小权重解释的 NP 完全性，提出包含最小解释的多项式算法和精确动态规划，实验表明最小标签割显著缩短解释并高效运行。
2026-10-02 cs.FL
The homology graph of a higher dimensional automaton
高维自动机，即标记预立方集，模型并发系统。我们引入了HDA的同调图，它是一个有向图，其节点是HDA的同调类。我们证明了同胚抽象下的同调图是不变的，即在弱态射同胚。
2013-07-30 cs.FL math.AT
Verification of $K$- and Infinite-Step Strong/Weak Anonymity Using Concurrent Compositions
Macau University of Science and Technology（澳门科技大学）；Xi’an Jiaotong University（西安交通大学）；Tianjin University of Science and Technology（天津科技大学）
本文针对非确定性有限状态自动机建模的部分可观测离散事件系统，定义四种新型K步及无限步匿名性，利用并发组合技术给出其充要条件与复杂度分析，并计算K步强、弱匿名性的K值上界。
2026-09-02 cs.CR cs.FL
[Draft] High-order estimation-based properties and high-order observers for labeled finite-state automata
本文提出了一种基于高阶估计性质的框架，通过高阶观察器验证标记有限状态自动机的属性。
2025-12-31 cs.FL
Structural Invariants for Parametric Verification of Systems with Almost Linear Architectures
我们认为并发系统组成的一个有限的，但数量未知的组件，这是一个给定的有限状态自动机的复制实例。组件通过执行交互进行通信，交互是一组组件的同时原子状态变化。我们指定交互的类型（例如\广播）和拓扑（即\体系结构）（例如，流水线，环）通过一个可判定的交互逻辑，这是嵌入在经典的弱顺序演算的一个继任者（WS1S）。证明这种系统的安全属性，如死锁自由或互斥的正确性，需要推断归纳不变量，包含可达状态集，避免不安全状态。我们的方法直接从描述相互作用的公式中合成这样的不变量，而不需要昂贵的定点迭代。我们应用我们的技术来验证几个教科书的例子，如用餐的哲学家，互斥协议和并发系统的抢占和优先级。
2019-02-07 cs.FL
A counterexample to Thiagarajan's conjecture on regular event structures
我们提供了一个反例Thiagarajan（1996年和2002年）的猜想，规则的事件结构完全对应的事件结构作为有限1-安全Petri网的展开。同样的反例被用来反驳Badouel，Darondeau，and Raoult（1999）的一个密切相关的猜想，即具有有界$\natural$ -团的正则事件结构的域是有限迹自动机可识别的。事件结构、跟踪自动机和Petri网是并发理论的基本模型。这些结构作为组合和几何对象存在着很好的解释。也就是说，从图论的角度来看，素事件结构的域正好对应于中值图;从几何的角度来看，这些域与CAT（0）立方体复形是双射的。这两个假设成立的必要条件是正则事件结构的域（具有有界$\natural$ -团）允许正则nice标签。为了反驳这些假设，我们描述了一个规则的事件域（有界$\natural$ -团），不承认一个定期的好标签。我们的反例来自怀斯（Wise，1996年和2007年）的一个例子，一个非正曲的平方复形，它的泛覆盖是一个CAT（0）平方复形，包含一个具有非周期镶嵌的特定平面。我们证明了Thiagarajan猜想的其他反例来自Kari和Papasoglu（1999）和Lukkarila（2009）的非周期4路确定性瓦片集。在积极的一面，使用Agol（2013）和Haglund and Wise（2008，2012）从几何群论的突破性结果，我们证明了Thiag…
2018-01-18 cs.DM cs.FL math.CO
