Proceedings Sixth International Symposium on Games, Automata, Logics and Formal Verification
本卷包含第六届国际游戏、自动机、逻辑和形式化验证研讨会（GandALF 2015）的会议记录。研讨会于2015年9月21日和22日在意大利热那亚举行。专题讨论会的会议记录载有三次应邀演讲的摘要和13篇论文，这些论文是经过仔细评估后被接受在会议上介绍的。被接受的论文的主题包括算法博弈论，自动机理论，形式化验证，模态和时序逻辑。
2015-09-23 cs.FL cs.LO
FO-definable transformations of infinite strings
有限弦的正则变换和非周期变换理论最近引起了人们的极大兴趣。这些类可以使用逻辑（一元二阶逻辑和一阶逻辑）、双向机（常规双向和非周期性双向转换器）和单向寄存器机（常规流式字符串和非周期性流式字符串转换器）等效地定义。已知这些类在顺序组合和常规（无星）选择等操作下是封闭的;并且功能等价和类型检查等问题对于这些类是可判定的。另一方面，对于无限弦，这些结果只在$ω$ -正则变换下才被发现：Alfred、Filiot和Trivedi研究了无限弦的变换，并引入了流弦变换在$ω$ -弦上的扩展，并证明了它们捕获了无限弦的一元二阶可定义变换。在本文中，我们扩展他们的工作，以恢复一阶逻辑可定义的变换，非周期性的双向传感器和非周期性的流串传感器之间的无限字符串连接。
2016-07-17 cs.FL cs.LO
Multi-weighted Automata and MSO Logic
加权自动机是一种非确定性自动机，其中的转换都带有权值。它们可以模拟系统的定量方面，如成本或能耗。运行的值可以被计算为例如转变权重的最大值、极限平均值或折扣总和。在多重加权自动机中，转换带有多个权重，并且可以模拟例如奖励和成本之间的比率，或者在二级资源上的某个上限约束下的主要资源的使用效率。在这里，我们介绍了一个一般模型的多加权自动机以及多加权MSO逻辑。在我们的主要结果中，我们表明，这种多加权MSO逻辑和多加权自动机是表示等价的有限和无限的话。翻译过程是有效的，导致我们的多加权MSO逻辑的可判定性结果。
2015-06-19 cs.FL cs.LO
Automata Theory Meets Barrier Certificates: Temporal Logic Verification of Nonlinear Systems
我们认为时间逻辑验证（可能是非线性的）动态系统在连续的状态空间。我们的方法结合了基于自动机的验证和所谓的屏障证书的使用。基于自动机的验证允许将验证任务分解为连续状态空间上的有限的简单约束集合。反过来，这些约束的满足可以（可能是保守的）通过适当构造的屏障证书来证明。因此，我们的方法，再加上基于优化的搜索屏障证书，允许计算验证的动态系统对时间逻辑属性，同时避免显式抽象的动力学通常在文献中做。
2014-03-14 cs.FL cs.LO
Proceedings Seventeenth International Symposium on Games, Automata, Logics, and Formal Verification
本文是关于GandALF 2026研讨会论文集的介绍，该会议于2026年在丹麦奥尔堡举行，旨在汇集博弈、自动机、逻辑与形式化验证领域的研究者，促进理论与应用的交叉融合。
2026-10-08 cs.FL cs.LO
Effective Characterizations of Simple Fragments of Temporal Logic Using Carton--Michel Automata
我们提出了一个框架，获得有效的未来时序逻辑（LTL）的简单片段与自然数的时域特征。该框架是基于一种形式的强明确的自动机，也被称为预言自动机或完全明确的Büchi自动机，并在本文中被称为Carton-Michel自动机。这些自动机具有很强的结构特性，特别是，它们以一种自然的方式将无限词的正则语言的“有限分数”与其“无穷分数”分离。在我们的框架内，我们提供了几个自然片段的时序逻辑，其中，在某些情况下，没有有效的表征已经知道以前的特征，并给出其计算复杂性的下限和上限。
2013-06-20 cs.FL cs.LO
Automata and temporal logic over arbitrary linear time
线性时序逻辑是为了推理反应系统而引入的。它通常被认为是关于无限的话，指定长期运行的系统的行为。我们可以考虑线性时间的更一般的模型，使用由任意线性排序索引的词。我们调查的时间逻辑和自动机之间的联系，线性排序，介绍了Bruyère和纸箱。我们提供了一个双指数过程，从任何LTL公式计算直到，因为，和Stavi连接词的自动机，决定该公式是否对输入字。特别地，由于这些自动机的空性问题是可判定的，这种变换给出了逻辑可满足性的判定过程。
2011-01-10 cs.FL cs.LO
Feasible Automata for Two-Variable Logic with Successor on Data Words
我们介绍了一个自动机模型的数据字，这是在每个位置进行一个符号从一个有限的字母表和一个值从一个无界的数据域的话。该模型是（语义）的数据自动机，介绍了Bojanczyk，等的限制。在2006年，它被称为弱数据自动机。它的表达能力比数据自动机差，而表达能力又是寄存器自动机无法比拟的。弱数据自动机的表达能力与后继为+1且数据值相等\sim，EMSO 2（+1，\sim）的存在一元二阶逻辑完全对应。它遵循从以前的工作，大卫，等。等人在2010年提出了弱数据自动机的非空性问题可以在2-NEXPTIME中判定。此外，我们还研究了数据ω-串上的弱Büchi自动机。它们可以用EMSO 2（+1，\sim）的扩展来刻画，其中存在量词用于无限集合.最后，通过对弱数据自动机的非空性问题进行非确定性多项式时间约简，得到了其非空性问题的复杂性界。
2011-10-06 cs.FL cs.LO
Weighted Automata and Logics for Infinite Nested Words
Nested words由Alfred和Madhusudan引入，用于捕获具有线性和层次顺序的结构，例如XML文档，而不会丢失有价值的闭包属性。此外，Büchi和Madhusudan为有限和无限嵌套词引入了自动机和等价逻辑，从而将Büchi定理扩展到嵌套词。最近，在定量系统中的权重的平均和折扣计算发现了很大的兴趣。在这里，我们将介绍和研究加权自动机模型和加权MSO逻辑无限嵌套的话。作为权重结构，我们考虑赋值幺半群，它包含权重的平均和折扣计算以及经典的半环。我们表明，在适当的假设下，两个分别。我们的加权逻辑的三个片段可以相互转换。此外，我们表明，逻辑片段具有相同的表达能力加权嵌套词自动机。
2015-06-23 cs.FL cs.LO
Proceedings Ninth International Symposium on Games, Automata, Logics, and Formal Verification
本卷包含第九届游戏，自动机，逻辑和形式化验证国际研讨会（GandALF 2018）的会议记录。研讨会于2018年9月26日至28日在德国萨尔布吕肯举行。Gandalf研讨会是由一群意大利计算机科学家建立的，他们对数学逻辑、自动机理论、博弈论及其在复杂系统规范、设计和验证中的应用感兴趣。它的目的是提供一个论坛，让来自不同地区，可能有不同背景的人可以进行富有成效的互动。Gandalf具有真正的国际精神，这一点可以从项目和指导委员会的组成以及提交论文的国家分布中得到证明。
2018-09-07 cs.FL cs.LO
Higher-Order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties
本文研究一类非常一般的无限秩树的逻辑性质，即由高阶递归方案生成的无限秩树。我们考虑，对于一元二阶逻辑和模态μ演算，三个主要问题：模型检查，逻辑反射（又名全局模型检查，要求公式成立的元素集的有限描述）和选择（要求，如果存在的话，要求具有二阶自由变量的MSO公式成立的元素集的有限描述）。对于每一个问题，我们都提供了有效的解决方案。这是由于高阶递归方案和可折叠下推自动机之间的已知连接，并在以前的工作有关奇偶校验游戏上的过渡图的可折叠下推自动机。
2021-03-02 cs.FL cs.LO
Set Automata and Limits of Decidability of Two-Variable Logic on Data Words
Tata Institute of Fundamental Research（塔塔基础研究所）；Indian Institute of Technology Goa（印度理工学院果阿分校）
研究扩展数据词双变量逻辑以包含guarded regular二元谓词，定义了idempotent monoids的决定性条件，并引入set automata形式化，证明其与ordered quasi-normal set automata的等价性。
2026-05-09 cs.FL cs.LO
Logic and Languages of Higher-Dimensional Automata
本文从逻辑角度研究有限高维自动机，证明其语言与MSO可定义的有限有界宽度带接口区间偏序集在序扩张下相互对应，并由此得出该类集合的序扩张仍保持MSO可定义性。
2024-03-28 cs.FL cs.LO
Register Automata with Extrema Constraints, and an Application to Two-Variable Logic
本文提出带极值约束的寄存器自动机模型，证明其空性问题可判定，并应用于二变量逻辑，在树序和线性序存在时证明其可数可满足性及可满足性问题可判定。
2022-03-21 cs.FL cs.LO
Minimisation in Logical Form
Stone-type对偶为研究逻辑系统的性质提供了一个强有力的数学框架。他们最近已经卓有成效地探索在理解最小化的各种类型的自动机。在Bezhanishvili等人（2012）中，一个余代数范畴和一个代数范畴之间的对偶等价被用来解释极小化。代数语义是对偶的余代数语义，其中逻辑等价与迹等价一致。余代数的极大子代数对应于代数的极小子代数。例子包括部分可观测的确定性有限自动机，线性加权自动机被视为有限维向量空间上的余代数，以及信念自动机，它们是紧致豪斯多夫空间上的余代数。在Bonchi et al.（2014）中，Brzozowski对确定性有限自动机的双反转最小化算法进行了分类描述，并通过可达性和可观察性之间的对偶解释了其正确性。这项工作包括概括Brzozowski的算法摩尔和加权自动机交换半环。在本文中，我们提出了一个一般的分类框架内，这种最小化算法可以理解。目标是提供一个基于二元性的统一视角。我们的框架包括一个堆栈的三个相互关联的adjections-base对偶adjunction，可以提升到一个对偶adjunction之间的coalgebras和代数，也到一个对偶adjunction之间的自动机。该方法提供了对可达性和可观察性的抽象理解。我们说明了一系列具体的例子，包括确定性Kripke框架，加权自动机，拓扑自动机（信念自动机），和交替自动机的一般框架。
2020-05-23 cs.FL cs.LO
Weighted Automata and Monadic Second Order Logic
设S是交换半环。M. Droste和P.Gastin在2005年引入了加权一元二阶逻辑WMSOL，其权在S。他们使用WMSOL的语法片段RMSOL来表征加权自动机可识别的词函数（幂级数），其中量词的语义既用作算术运算，又在布尔情况下用作量化。早在2001年，B. Courcelle、J.Makowsky和U. Rotics已经引入了一种形式主义，用于在Monadic二阶逻辑中定义的图参数，这里称为MSOLEVAL，其值在环R中。它们的框架可以很容易地适应于半环S。这种形式主义清楚地将逻辑部分与算术部分分开，并且也适用于词函数。本文给出了两个证明：值在S中的RMSOL和MSOLEVAL对词具有相同的表达能力。一个证明直接表明，MSOLEVAL捕获的功能可识别的加权自动机。另一个证明展示了如何将形式主义从一个转换成另一个。
2013-07-17 cs.FL cs.LO
Proceedings 12th International Symposium on Games, Automata, Logics, and Formal Verification
本卷包含第12届国际游戏，自动机，逻辑和形式化验证研讨会（GandALF 2021）的会议记录。Gandalf 2021研讨会的目的是汇集来自学术界和工业界的研究人员，他们积极参与游戏，自动机，逻辑和形式化验证领域的工作。其想法是涵盖从理论到应用的广泛主题，并促进相互交流。
2021-09-16 cs.FL cs.GT cs.LO
Proceedings of the 13th International Symposium on Games, Automata, Logics and Formal Verification
本卷包含第13届国际游戏，自动机，逻辑和形式化验证研讨会（GandALF 2022）的会议记录。Gandalf 2022研讨会的目的是汇集来自学术界和工业界的研究人员，他们积极参与游戏，自动机，逻辑和形式化验证领域的工作。其想法是涵盖从理论到应用的广泛主题，并促进相互交流。
2022-09-19 cs.FL cs.GT cs.LO
On the Translation of Automata to Linear Temporal Logic
虽然将未来的线性时态逻辑（LTL）转换为无限词上的自动机的复杂性是众所周知的，但将自动机转换回LTL所涉及的大小增加却不是。特别是，没有已知的基本限制的复杂性，翻译确定性$ω$ -定期自动机LTL。我们的第一个贡献包括严格的界限LTL在一元字母表：交替，非确定性和确定性自动机可以完全指数，二次和线性更简洁，分别比任何等价的LTL公式。我们的主要贡献包括翻译一般计数器免费确定性$ω$ -定期自动机到LTL公式的双指数时间嵌套深度和三重指数长度，使用中间Krohn-Rhodes级联分解的自动机。据我们所知，这是这个翻译的第一个基本界限。此外，我们的翻译保留了自动机的接受条件，在这个意义上，它把一个循环，弱，Büchi，coBüchi或穆勒自动机到一个公式，属于匹配类的句法未来层次。特别地，它可以用于将识别安全语言的LTL公式转换为属于LTL的安全片段的公式（在有限和无限字上）。
2022-05-08 cs.FL cs.LO
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
Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification
本卷包含第七届国际游戏、自动机、逻辑和形式化验证研讨会（GandALF 2016）的会议记录。研讨会于2016年9月14日至16日在意大利卡塔尼亚举行。研讨会的会议记录包括3个特邀演讲的摘要和21篇论文全文，这些论文是经过仔细评估后被接受在会议上发表的。被接受的论文的主题涵盖算法博弈论，自动机理论，综合，形式化验证，动态，模态和时态逻辑。
2016-09-13 cs.FL cs.GT cs.LO
Proceedings of the Fourteenth International Symposium on Games, Automata, Logics, and Formal Verification
该论文集汇集GandALF 2023关于博弈、自动机、逻辑与形式验证的研究，旨在连接学界与业界并推动理论及应用的交叉融合。
2023-09-29 cs.CC cs.FL cs.LO
Proceedings Fifth International Symposium on Games, Automata, Logics and Formal Verification
本卷包含第五届国际游戏、自动机、逻辑和形式化验证研讨会（GandALF 2014）的会议记录。研讨会于2014年9月10日至12日在意大利维罗纳举行。专题讨论会的会议记录载有三次应邀演讲的摘要和19篇论文，这些论文是经过仔细评估后被接受在会议上发表的。被接受的论文的主题范围很广，包括算法和行为博弈论，博弈语义学，形式语言和自动机理论，模态和时序逻辑，软件验证，混合系统。
2014-08-24 cs.FL cs.GT cs.LO
Teaching LTL and ω-automata with Spot
EPITA Research Laboratory（EPITA研究实验室）
研究如何利用Spot库教授线性时态逻辑和ω自动机，核心方法是借助其可视化能力与Python接口，主要贡献是为相关教学提供了有吸引力的平台。
2026-07-08 cs.FL cs.LO
Proceedings Fourth International Symposium on Games, Automata, Logics and Formal Verification
本卷包含第四届国际游戏、自动机、逻辑和形式化验证研讨会（GandALF 2013）的会议记录。研讨会于2013年8月29日至31日在意大利Borca di Cadore举行。专题讨论会的会议记录载有三次应邀演讲的摘要和17篇论文，这些论文是经过仔细评估后被接受在会议上发表的。被接受的论文的主题范围很广，包括算法和行为博弈论，博弈语义学，形式语言和自动机理论，模态和时序逻辑，软件验证，混合系统。
2013-07-16 cs.FL cs.GT cs.LO
Distributed Automata and Logic
分布式自动机是在有限有向图上运行的有限状态机。作为同步分布式算法，它们使用它们的输入图作为一个网络，在这个网络中，相同的处理器可能进行无限次的同步轮通信。对于这些自动机的局部变体，其中轮数由常数限定，Hella等人（2012，2015）已经根据基本模态逻辑建立了逻辑表征。在这篇论文中，我们为两个更具表现力的分布式自动机类提供了类似的逻辑刻画。第一类扩展了具有全局接受条件的局部自动机，并能够在不确定性和并行计算之间交替。我们证明了它等价于图上的一元二阶逻辑。通过限制转换是不确定性或确定性的，我们也得到了两个严格较弱的变体，空性问题是可判定的。我们的第二个类的异步算法的标准概念转移到非局部分布式自动机的设置。由此产生的机器被证明是等价于一个小片段的最小不动点逻辑，更具体地说，到一个受限制的变种的模态μ演算，允许最少的不动点，但禁止最大的不动点。利用与逻辑的连接，我们还证明了这些异步自动机的表达能力是独立的消息是否可以丢失。
2018-05-16 cs.DC cs.FL cs.LO
Proceedings Fifteenth International Symposium on Games, Automata, Logics, and Formal Verification
本卷是2024年6月在冰岛雷克雅未克举办的第十五届GandALF研讨会论文集，该会汇聚游戏、自动机等领域产学研研究者，覆盖理论到应用主题以促进跨领域融合。
2024-10-29 cs.CC cs.FL cs.LO
A Tableau Construction for Finite Linear-Time Temporal Logic
本文描述了一种将有限命题线性时间时态逻辑（Finite LTL）中的公式转换成有限状态自动机的方法，该自动机的语言是给定公式的模型。有限LTL与传统LTL的不同之处在于，公式是关于有限而不是无限的状态序列来解释的;这一事实意味着传统的有限状态自动机，而不是像Büchi和其他人开发的ω-自动机，足以识别这样的公式的模型。所考虑的方法是基于众所周知的表格建设技术开发的LTL，我们在这里适应有限LTL的设置。所得到的自动机可用作模型检验、可满足性测试和模型综合的基础。
2020-06-22 cs.FL cs.LO
A Pattern Logic for Automata with Outputs
我们引入了一个逻辑来表达自动机的结构特性与字符串输入，并可能在一些幺半群的输出。在这个逻辑中，讨论输出值的谓词集是参数的，我们提供了模型检查问题可判定的谓词的充分条件。然后，我们考虑三个特定的自动机模型（有限自动机，传感器和自动机加权整数-求和自动机-），并实例化的通用逻辑为他们每个人。我们给紧的复杂性结果的三个逻辑和模型检测问题，这取决于公式是否是固定的。我们研究我们的逻辑的表达能力，通过表达经典的结构模式，例如有限的模糊性和多项式模糊性的情况下，有限自动机，可确定性和有限值的情况下，传感器和求和自动机的特点。因此，我们的复杂性的结果，我们直接得到这些经典性质可以决定在PTIME。
2018-10-08 cs.FL
Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment
线性时序逻辑的某些应用需要将逻辑公式转化为确定性的欧米伽自动机。目前有两个翻译器产生确定性自动机：ltl 2dstar适用于整个LTL和Rabinizer适用于LTL（F，G），这是LTL片段只使用模态F和G。我们提出了一个新的翻译确定性拉宾自动机通过交替自动机和确定性转换为基础的广义拉宾自动机。我们的翻译适用于严格大于LTL（F，G）的片段。实验结果表明，我们的算法可以产生显着更小的自动机相比，Rabinizer和ltl 2dstar，特别是对于更复杂的LTL公式。
2013-11-06 cs.FL cs.LO
Logics Meet 2-Way 1-Clock Alternating Timed Automata
本文研究了单时钟交替时间自动机（1-ATA）的扩展，即双向单时钟交替时间自动机（2-Way 1-ATA）。我们证明了具有重置自由循环的2-Way 1-ATA的子类（2-Way 1-ATA-rfl）在表达上等价于用保护度量量词（GQMSO）扩展的MSO[<]。2路1-ATA-rfl（以及因此GQMSO）的空性检查问题通常是不可判定的。我们提出了一个“非准时性”的限制，称为非邻接，2路1-ATA-rfl，也为GQMSO，其中的空（分别满足性）检查成为可判定的。非相邻2路1-ATA是第一类具有交替和2路性的时间自动机，其空性检查是可判定的（并且也具有初等复杂性）。我们还表明，2路1-ATA-rfl，即使与非相邻的限制，可以表达属性是不可识别的使用1-ATA。
2022-02-26 cs.FL cs.LO
Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification
本卷包含第11届游戏，自动机，逻辑和形式化验证国际研讨会（GandALF 2020）的会议记录。研讨会于2020年9月21日至22日以完全在线的方式举行。Gandalf研讨会是由一群意大利计算机科学家建立的，他们对数学逻辑、自动机理论、博弈论及其在复杂系统规范、设计和验证中的应用感兴趣。它的目的是提供一个论坛，让来自不同地区，可能有不同背景的人可以进行富有成效的互动。Gandalf具有真正的国际精神，这一点可以从项目和指导委员会的组成以及提交论文的国家分布中得到证明。
2020-09-20 cs.FL cs.GT cs.LO
Proceedings Tenth International Symposium on Games, Automata, Logics, and Formal Verification
本卷包含第十届游戏，自动机，逻辑和形式化验证国际研讨会（GandALF 2019）的会议记录。研讨会于2010年9月2日至3日在法国波尔多举行。Gandalf研讨会是由一群意大利计算机科学家建立的，他们对数学逻辑、自动机理论、博弈论及其在复杂系统规范、设计和验证中的应用感兴趣。它的目的是提供一个论坛，让来自不同地区，可能有不同背景的人可以进行富有成效的互动。Gandalf具有真正的国际精神，这一点可以从项目和指导委员会的组成以及提交论文的国家分布中得到证明。
2019-09-12 cs.FL cs.GT cs.LO
Proceedings Eighth International Symposium on Games, Automata, Logics and Formal Verification
本卷包含第八届游戏、自动机、逻辑和形式化验证国际研讨会（GandALF 2017）的会议记录。研讨会于2017年9月20日至22日在意大利罗马举行。Gandalf研讨会是由一群意大利计算机科学家建立的，他们对数学逻辑、自动机理论、博弈论及其在复杂系统规范、设计和验证中的应用感兴趣。它的目的是提供一个论坛，让来自不同地区，可能有不同背景的人可以进行富有成效的互动。Gandalf具有真正的国际精神，这一点可以从项目和指导委员会的组成以及提交论文的国家分布中得到证明。
2017-09-06 cs.FL cs.GT cs.LO
Proceedings First Symposium on Games, Automata, Logic, and Formal Verification
本卷包含了第一次研讨会上的“游戏，自动机，逻辑，和形式化验证（GandALF）"，在米诺里（阿马尔菲海岸），意大利，2010年6月17日至18日举行的会议记录。研讨会由一些对博弈论、数理逻辑、自动机理论及其在复杂系统的规范、设计和验证中的应用感兴趣的意大利计算机科学家推动。它涵盖了大量的研究课题，从理论方面到具体应用。它的目的是提供一个论坛，让来自不同地区的人，可能有不同的背景，可以成功地互动。该活动的高水平国际形象由节目委员会的组成和最终节目见证。
2010-06-09 cs.FL cs.GT cs.LO
An Alternating Automaton for First-Order Linear Temporal Logic--Tech Report
本文给出了LTL-FO $^+$性质的自动机表示。LTL-FO $^+$是LTL的一个扩展，它包含了对有界变量的一阶量化，从而大大提高了语言的表达能力。这种形式主义的自动机表示允许更容易地编写和理解属性，以及执行操作，如否定或空检查。LTL-FO $^+$公式的自动机表示具有有限的大小，而不管量化变量的域以及在属性的大小中是线性的状态的数量。
2016-10-22 cs.FL cs.LO
Weight Assignment Logic
我们介绍了一个权重分配逻辑推理的数量语言的无限的话。该逻辑是经典MSO逻辑的扩展，并且允许描述具有多个权重参数的系统的定量性质，例如，回报与成本的比率我们表明，这种逻辑是表达等价于明确的加权Büchi自动机。我们还考虑了扩展的重量分配逻辑，这是表示等价于不确定性加权Büchi自动机。
2015-08-25 cs.FL cs.LO
An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata
在80年代中期，Lichelman，Pnueli和Zuck证明了一个经典定理，说明Past LTL的每个公式（带有过去算子的LTL的扩展）都等价于$\bigwedge_{i=1}^n \mathbf{G}\mathbf{F} φ_i \vee \mathbf{F}\mathbf{G} ψ_i$形式的公式，其中$φ_i$和$ψ_i$只包含过去算子。几年后，Chang、Manna和Pnueli在这个结果的基础上导出了LTL的类似范式。这两个规范化过程都有一个非初等的最坏情况爆破，并遵循从公式到无计数器自动机到无星正则表达式再回到公式的相关路径。我们在这两点上都有所改进。我们提出了一个直接的和纯粹的语法规范化程序LTL产生一个范式，相当于一个由张，曼纳，和Pnueli，只有一个单一的指数爆破。作为一个应用，我们推导出一个简单的算法，将LTL转换成确定性的拉宾自动机。该算法规范化的公式，将其转换成一个特殊的非常弱的交替自动机，并适用于一个简单的determinisation程序，有效的只有这些特殊的自动机。
2020-05-01 cs.FL cs.LO
A translation of weighted LTL formulas to weighted Büchi automata over ω-valuation monoids
本文在乘积$ω$ -赋值幺半群上引入了一个满足特定性质的加权LTL。我们还引入了带$\varepsilon$ -转移的加权广义Büchi自动机，以及在积$ω$ -赋值幺半群上带$\varepsilon$ -转移的加权Büchi自动机，并证明了这两个模型在表达上是等价的，也等价于文献中已经引入的加权Büchi自动机.我们证明了我们的逻辑的一个句法片段的每个公式可以有效地转化为一个加权的广义Büchi自动机与$\varepsilon$ -转移。对于满足特定性质的广义乘积$ω$ -赋值幺半群，我们定义了加权LTL，带$\varepsilon$ -变迁的加权广义Büchi自动机，带$\varepsilon$ -变迁的加权Büchi自动机，并证明了广义乘积$ω$ -赋值幺半群的上述结果.本文给出了一个带限制的语法片断的加权LTL公式到带$\varepsilon$ -转移的加权广义Büchi自动机的转化。
2022-01-02 cs.FL cs.LO
Reachability relations of timed pushdown automata
时间下推自动机（TPDA）是一种将递归与时间约束逻辑相结合的表达形式。我们证明了TPDA的可达性关系可以用线性算术表示，这是一种丰富的逻辑，推广了Presburger算术和有理算术。的主要技术成分是一个新的量词消去结果的时钟约束（用于简化TPDA转换的语法），使用时钟差关系来表达的分数时钟值的可达性关系，和应用帕里克定理重建的积分时钟值。
2020-12-30 cs.FL cs.LO
Automata-Based Software Model Checking of Hyperproperties
我们开发了时态流逻辑（TSL）和超时态流逻辑（HyperTSL）模理论的模型检验算法。TSL扩展了线性时序逻辑（LTL）的存储单元，功能和谓词，使其成为一个方便的和表达的逻辑推理软件和其他系统的无限数据域。HyperTSL进一步将TSL扩展到hyperproperties的规范-与多个系统执行相关的属性。因此，HyperTSL可以在软件系统中表达信息流策略，如不干涉。我们用理论扩充了HyperTSL，得到了HyperTSL（T），并建立在LTL软件验证的方法上，得到了TSL和HyperTSL（T）的模型检验算法。这导致了一个合理但不一定完整的算法，用于HyperTSL（T）的forall*exists* 片段中包含的规范。我们的方法构成了第一个软件模型检验算法的时间hyperproperties与量词交替，不依赖于有限状态的抽象。
2023-03-26 cs.FL cs.LO
First-Order vs. Second-Order Encodings for LTLf-to-Automata Translation
将有限迹上的线性时序逻辑（LTL）公式转换为符号确定有限自动机（DFA），不仅在LTL公式综合中起着重要作用，而且在安全LTL公式综合中也起着重要作用。翻译是通过使用MONA，一个强大的工具，符号，BDD为基础，从逻辑规范的DFA建设。最近的工作使用LTLf公式的一阶编码将LTLf转换为一阶逻辑（FOL），然后将其馈送到MONA以获得符号DFA。这种编码表现良好，但其他编码尚未研究。具体来说，具有明显更简单的量化结构的二阶编码是否能优于一阶编码的自然问题仍然是开放的。在本文中，我们解决这一挑战，并研究二阶编码LTLf公式。我们首先介绍了一个特定的MSO编码，捕捉LTLf的语义在一个自然的方式，并证明其正确性。然后，我们探索的是一个紧凑的MSO编码，它受益于自动机理论的最小化，从而提出了一个可能的实际优势。为此，我们提出了一个形式化的符号DFA在二阶逻辑，从而开发了一个新的BDD和MSO之间的连接。然后，我们通过经验评估表明，一阶编码的性能优于二阶编码。结论是在LTLf到自动机的转换中，一阶编码比二阶编码更好。
2019-01-18 cs.FL cs.LO
Rarefied Thue-Morse Sums Via Automata Theory and Logic
令$t(n)$表示$n$的基$2$表示中的$1$比特的数目，取模$2$。我们展示了如何证明经典的猜想利奥莫泽，在稀薄的总和$\sum_{0\leq i<n} (-1)^{t(3i)}$，使用自动机理论和逻辑的工具。同样的技巧可以用来证明类似和的结果。
2023-02-22 cs.FL math.NT
A Nivat Theorem for Weighted Timed Automata and Weighted Relative Distance Logic
加权时间自动机（WTA）对实时系统的定量方面进行建模，如内存、电力或财务资源的持续消耗。它们接受量化的定时语言，其中每个定时单词都映射到一个值，例如，一个真实的数字本文证明了WTA的Nivat定理，即可识别的定量时间语言正是那些可以从可识别的布尔时间语言中通过几个简单的运算得到的语言。我们还介绍了加权相对距离逻辑的Wilke开发的扩展，我们表明，我们的加权相对距离逻辑和WTA是同样的表达。这个结果的证明可以从我们的Nivat定理和Wilke相对距离逻辑定理中得到。由于我们的Nivat定理的证明是构造性的，从逻辑到自动机的转换过程也是构造性的。这导致加权相对距离逻辑的可判定性结果。
2015-06-19 cs.FL
Games on Graphs: From Logic and Automata to Algorithms
本书系统梳理图上无限持续博弈，从自动机与逻辑起源讲到程序验证、综合及优化、强化学习等跨领域应用。
2025-07-29 cs.FL cs.GT cs.LO
An Automaton-based Characterisation of First-Order Logic over Infinite Trees
本文研究无穷树上的一阶逻辑，通过引入两类犹豫树自动机精确捕获 polcCTLp 和 cCTL*[f] 的表达能力，提供自动机理论刻画并导出范式，揭示 FO 仅表达安全或共安全属性。
2025-09-17 cs.FL cs.LO
Weak Mso with the Unbounding Quantifier
本文引入了一类新的无限词语言，称之为极大正则语言，它是对$ω$ -正则语言类的扩充.这个类有两个等价的描述：自动机（一种确定性计数器自动机）和逻辑（带有边界量词的弱一元二阶逻辑）。给出了逻辑和自动机之间的有效转换。
2009-02-06 cs.FL cs.LO
The Role of Logic and Automata in Understanding Transformers
Max-Planck Institute for Software Systems, Kaiserslautern, Germany University of Kaiserslautern-Landau, Kaiserslautern, Germany Institute for Mathematical
本文综述逻辑、自动机及电路复杂性在分析 Transformer 表达能力方面的作用，并指出其与验证交叉领域的开放问题。
2025-09-28 cs.CL cs.FL cs.LG
Efficient Automata-based Planning and Control under Spatio-Temporal Logic Specifications
时空逻辑在控制中的使用是出于对动态系统施加复杂的空间和时间行为并相应地控制这些系统的需要。合成正确的设计控制律是一项具有挑战性的任务，导致计算要求高的方法。我们认为有效的自动机为基础的规划连续时间系统下的信号间隔时序逻辑规范，表达片段的信号时序逻辑。规划是基于最近的结果，自动机为基础的验证度量区间时序逻辑。获得接受满足度量间隔时间逻辑规范的所有布尔信号的定时信号转换器，该度量间隔时间逻辑规范是从手头的信号间隔时间逻辑规范中提取的。该传感器被修改，以考虑信号间隔时间逻辑规范的空间特性，表征满足该规范的所有实值信号。使用基于逻辑的反馈控制法，如我们在早期的作品中提出的，然后，我们提供了一个抽象的系统，在一个合适的方式，与修改后的定时信号传感器对齐。这允许避免通常通过在系统的抽象和规范之间形成产品自动机而引起的状态空间爆炸。
2020-03-24 cs.FL
Probabilistic Disjunctive Normal Forms in Temporal Logic and Automata Theory
V.A. Trapeznikov Institute of Control Sciences of Russian Academy of Sciences（俄罗斯科学院控制科学瓦·阿·特拉佩兹尼科夫研究所）
本文提出概率析取范式用于表示和推理不确定性，结合代数证据组合与概率分布，实现逻辑、数值方法和连续概率的融合。
2026-03-11 cs.FL cs.LO math.PR
Alternation Is Strict For Higher-Order Modal Fixpoint Logic
研究了交替奇偶Krivine自动机（APKA）的表达能力，APKA为高阶模态不动点逻辑（HFL）提供了操作语义。APKA由普通的奇偶自动机扩展的变化Krivine抽象机。我们表明，APKA的优先级的数量和奇偶性形成了一个适当的层次结构的表达能力，在模态μ演算。这也导致了HFL上严格的交替层次结构。证明遵循Arnold（1999）的编码运行到树和随后使用的Banach不动点定理。
2016-09-14 cs.FL cs.LO
Asynchronous Distributed Automata: A Characterization of the Modal Mu-Fragment
我们建立了一类异步分布式自动机和一个小片段的最小不动点逻辑之间的等价性，当限制到有限有向图。更具体地说，我们考虑的逻辑是模态$μ$的片段（的变体）-允许最少固定点但禁止最大固定点的演算。相应的自动机模型使用相同的有限状态机网络，这些有限状态机以异步方式进行通信，并且其状态图必须是非循环的，除了自循环。利用与逻辑的连接，我们还证明了这些机器的表达能力是独立的消息是否可以丢失。
2017-03-06 cs.DC cs.FL cs.LO
An automaton over data words that captures EMSO logic
我们开发了一个通用的框架，其执行系统的规范和实施的话，或偏序，在一个无限的字母表。作为一个模型的实现，我们引入类寄存器自动机，一个单向自动机模型的话多个数据值。我们的模型结合了寄存器自动机和类记忆自动机。它有自然的解释。特别是，它捕获通信自动机与无限数量的进程，其语义可以被描述为一组（动态）消息序列图。在规范方面，我们提供了一个局部存在一元二阶逻辑，不对变量的数量施加任何限制。我们研究的可实现性问题，并表明，从逻辑的每一个公式可以有效地，并在小学的时间，翻译成一个等价的类寄存器自动机。
2011-06-10 cs.FL
Distributed Graph Automata and Verification of Distributed Algorithms
结合分布式算法和交替自动机的思想，我们引入了一类新的有限图自动机，精确识别一元二阶逻辑中可定义的有限图语言。通过限制转换是不确定性或确定性的，我们也得到了两个严格较弱的变种，我们的自动机的空性问题是可判定的。作为一个应用程序，我们建议如何合适的图自动机可能是有用的分布式算法的形式化验证，使用弗洛伊德-霍尔逻辑。
2014-09-28 cs.DC cs.FL cs.LO
