Model Checking Epistemic Halpern-Shoham Logic Extended with Regular Expressions
认知Halpern-Shoham逻辑（EHS）是一种时间-认知逻辑，它将Halpern-Shoham逻辑的区间算子与认知模态相结合。EHS的语义是基于解释系统，其标签功能定义在区间的端点上。我们表明，这个定义可以概括为允许标签功能的基础上，整个区间的正则表达式。我们证明，所有已知的EHS的积极成果，特别是吸引人的复杂性，其模型检验问题的一些片段，仍然持有其推广。我们还提出了新的逻辑EHSre操作标准Kripke结构，并具有表达能力相当于EHS与正则表达式。我们比较EHSre的表达能力与标准的时间逻辑。
2015-09-02 cs.LO
A Short Note on Infinite Union/Intersection of Omega Regular Languages
本文证明了Ω正则语言在无限并和交下不是封闭的。作为一种尝试，我们建议添加步骤变量和量词的时间逻辑，以提高底层逻辑的表达能力。我们还表明，这样做会导致不可判定的可满足性，即使是一个相当有限的片段的时间逻辑。
2016-03-17 cs.FL cs.LO
Energy mu-Calculus: Symbolic Fixed-Point Algorithms for omega-Regular Energy Games
$ω$-常规能量游戏，这是加权的两个玩家回合制游戏的定量目标，以保持能量水平非负，已被用于验证和合成的上下文中。模态$μ$-演算的逻辑，当应用于具有$ω$-正则获胜条件的博弈图时，允许以定点公式的形式定义用于计算获胜状态集的符号算法。在本文中，我们介绍了能量$μ$-演算，多值扩展的$μ$-演算，作为一个符号框架解决$ω$-经常能源游戏。能量$μ$-演算使现有的，众所周知的符号$μ$-演算算法的无缝重用$ω$-常规游戏，以解决其相应的能量增强的变种。我们定义的语法和语义的能量$μ$-演算的符号表示的游戏图，并展示了如何使用它来解决决策和最小信用问题的$ω$-定期能源游戏，有界和无界的能量水平的积累。
2020-10-18 cs.LO
Symbolic model checking of tense logics on rational Kripke models
本文引入了有理Kripke模型类，研究了基本时态逻辑Kt的符号模型检验及其在该类模型中的一些扩展。有理Kripke模型基于（通常是无限的）有理图，顶点由某些正则语言中的单词标记，转换由异步双头有限自动机（也称为有理转换器）识别。在理性Kripke模型中，每个原子命题都在一组规则的状态中求值。证明了Kt的每个公式在每个有理Kripke模型中都有一个有效的可计算正则扩张，从而证明了有理Kripke模型中Kt的局部模型检验和全局模型检验是可判定的.这些结果被提升到Kt的一些扩展。我们研究并部分确定了模型检验过程的复杂性。
2008-10-30 cs.LO
Omega-regular Verification and Control for Distributional Specifications in MDPs
本文首次提出基于分布性证书的自动化方法，在 PSPACE 内实现对 MDP 分布性 omega-正则规范的可靠且相对完备的验证与控制。
2025-07-06 cs.LO
A PAC Learning Algorithm for LTL and Omega-regular Objectives in MDPs
University of Colorado Boulder（科罗拉多大学博尔德分校）
本文针对 MDP 中的 omega-正则目标提出基于模型的 PAC 学习算法，引入 epsilon-复发时间度量策略收敛速度，并证明其样本复杂度为多项式级且经实验验证。
2024-02-21 cs.LG cs.LO
Proving termination with transition invariants of height omega
Podelski和Rybalchenko的终止定理指出，从任何初始状态终止的归约关系正是其传递闭包（仅限于可达状态）包含在某些良基关系的有限并中的归约关系。该定理的另一种陈述是，终止约化关系正是那些具有“反言有理的转变不变量”的关系。根据这个结果，同一作者和Byron Cook设计了一个算法来检查while-if程序终止的充分条件。该算法寻找一个析取的良好基础的过渡不变量，由良好基础的关系的高度Ω，如果它找到它，它推导出终止的while-if程序使用终止定理。这就提出了一个有趣的问题：当每个关系都有高度Ω时，具有析取良基转换不变量的归约关系的状态是什么？这个问题的答案可以导致一组while-if程序的终止算法可以证明是终止的表征。本文的目的是证明它们是高度为ω ^n的约化关系的集合，其中n <ω。此外，如果转移不变量中的所有关系都是本原递归的，且归约关系是本原递归映射对某个本原递归集的限制的图，则最终状态可由初始状态下的某个本原递归映射计算.作为一个推论，我们得出的一组功能，有至少一个实现Podelski Rybalchenko while-if语言与一个良好的基础析取过渡不变，其中每个关系的高度Ω，正是一组原始递归函数。
2014-07-17 cs.LO
Quantitative Model Checking of Linear-Time Properties Based on Generalized Possibility Measures
基于可能性测度的线性时间特性的模型检验在以前的工作（Y。Li和L. Li，模型检验基于可能性度量的线性时间特性，IEEE Transactions on Fuzzy Systems，21（5）（2013），842-854）。然而，在以前的工作中考虑的线性时间性质是经典的和定性的，系统的可能性信息没有考虑在所有。本文将研究基于广义可能性测度的模糊线性时间性质的定量模型检验。使用可能性信息来描述系统的模型以及系统需要遵守的属性，以识别模型/属性中的不确定性。系统采用{ \sl广义可能性Kripke结构}（GPKS，简称）建模，其性质用模糊线性时间性质描述.具体地，研究了GPKS系统的可达性、总是可达性、约束可达性、重复可达性和持续性的模糊线性时间性质。介绍了GPKS中的模糊正则安全性质和模糊$ω-$正则性质，深入研究了模糊有限自动机对模糊正则安全性质和模糊$ω-$正则性质的验证.证明了有限GPKS中模糊正则安全性和模糊$ω-$正则性的验证可以转化为本文所介绍的产品GPKS中（总是）可达性和重复可达性（持久性）的验证.文中给出了几个算例来说明本文所提出的方法。
2016-01-25 cs.LO
Synthesis of Temporal Causality
本研究推广时序因果性框架，提出首个针对ω-正则效应的完备原因合成算法，证明其原因具有ω-正则性，可通过原型工具实现并验证了实际性能。
2025-06-17 cs.LO
A decidable class of (nominal) omega-regular languages over an infinite alphabet
我们定义了一类在无限个字母表上有无限个词的语言，以及相应的自动机。用于识别的自动机是确定性Muller自动机的一个推广，以设置名义集。值得注意的是，所获得的语言是由它们最终的周期性片段决定的，就像经典的情况一样。在补、并、交下的封闭性，以及空性和等价性的可判定性都被推广所保持。这是通过使用有限表示（否则无限状态）定义类的自动机。
2013-10-15 cs.FL cs.LO
Realizing Omega-regular Hyperproperties
研究了超逻辑HyperQPTL，它结合了迹关系和$ω$ -正则性的概念.我们证明了HyperQPTL是非常有表现力的，它可以表达诸如不确定性，有界等待授权，认知属性，特别是任何$ω$ -正则属性等属性。这些属性在以前研究过的超逻辑（如HyperLTL）中无法表达。与此同时，我们认为，HyperQPTL的表现力是最佳的，在某种意义上，一个更有表现力的逻辑$ω$ -正则超属性将有一个不可判定的模型检验问题。我们进一步研究了HyperQPTL的可实现性问题。我们证明了可实现性对于包含像不确定性这样的属性的HyperQPTL片段是可判定的。但是，与可满足性问题相比，命题量化确实使超逻辑的可实现性问题更难。更具体地说，具有泛存在命题量词交替后跟单个迹量词的HyperQPTL公式片段通常是不可判定的，即使片段到HyperLTL的投影具有可判定的可实现性问题。最后，我们在原型工具BoSy中实现了HyperQPTL的有界综合问题。使用带有HyperQPTL规范的BoSy，我们已经能够合成几个资源仲裁器。非线性时间超逻辑的综合问题仍然是一个未解决的问题。例如，还不知道如何从分支时间超逻辑（如HyperCTL $^*$）中给出的规范合成系统。
2021-01-18 cs.LO
Regular Model Checking Revisited (Technical Report)
在这方面的贡献，我们重温定期模型检验，一个强大的框架，已成功地应用于验证的无限状态系统，特别是参数化系统（并发系统与任意数量的进程）。我们提供了一个重新制定的定期模型检验与长度保持传感器在存在的二阶理论在自动结构。我们认为，这是一个自然的配方，使我们能够利用强大的综合技术，已被广泛研究的软件验证社区。更确切地说，在这个公式中，一阶部分表示所需正确性属性的验证条件（我们有完整的求解器），而存在量化的二阶变量表示要合成的关系。我们表明，许多有趣的正确性可以用这种方式制定，例如安全，活性，双相似性，和游戏。更重要的是，我们表明，这种新的配方允许新的有趣的基准（和旧的定期模型检验基准，以前被认为是困难的），特别是在参数化系统验证领域，要解决。
2021-11-21 cs.FL cs.LO
Approximate Automata for Omega-Regular Languages
无限词上的自动机，也被称为欧米伽自动机，在反应系统的验证和综合中起着关键作用。欧米茄自动机的谱由两个特征定义：接受条件（例如Büchi或宇称）和决定论（例如，确定性或非确定性）的自动机。这些特性在自动机理论的应用中起着至关重要的作用。例如，某些验收条件可以通过专用工具和算法比其他条件更有效地处理。此外，一些应用程序，如合成和概率模型检验，要求属性表示为某种类型的确定性欧米茄自动机。然而，属性并不总是由具有期望的接受条件和确定性的自动机表示。在本文中，我们研究的问题，逼近线性时间性质的自动机在一个给定的类。我们的近似是基于保留的语言，以用户定义的精度，在有限的套索表示的无限的执行，保留的大小。我们研究了不同类型的近似自动机的状态复杂性，并提供了不同的自动机类内的近似结构，例如，近似一个给定的自动机的一个更简单的接受条件。
2020-12-29 cs.FL cs.LO
Omega-Regular Decision Processes
University of Twente（特文特大学）；University of Colorado Boulder（科罗拉多大学博尔德分校）；University of Liverpool（利物浦大学）
该研究提出omega-正则决策过程（ODPs），将非马尔可夫决策的约束从过去正则性质扩展为未来omega-正则前瞻，未满足承诺则收益为最劣值，通过归约为有限MDP的字典序优化学习实现折扣奖励目标下的优化，实验验证了归约的有效性。
2023-12-14 cs.LG cs.LO
On the Complexity of Verifying Regular Properties on Flat Counter Systems
在计数器系统验证的近似方法中，其中之一是模型检验其平坦展开。不幸的是，除了可达性查询或过去的LTL模型检查问题的复杂性表征，这种业务模型并不总是很好地研究。在本文中，我们描述的复杂性的模型检测问题的平面计数器系统的规约语言，包括一阶逻辑，线性μ演算，无限自动机，和相关的形式主义。我们的研究结果跨越不同的复杂性类（主要是从PTime到PSpace），它们适用于计数器值的算术约束系统允许的语言。就证明技术而言，我们提供了一种集中于主要问题的统一方法。
2013-04-23 cs.LO
Model Checking Regular Language Constraints
即使是最快的SMT求解器在处理来自真实程序的正则表达式时也会遇到性能问题。由于这些性能问题通常来自问题表示（例如，非确定性有限自动机得到确定和正则表达式得到展开），我们重新审视布尔有限自动机，它允许直接和自然的表示任何正则语言的布尔组合。将IC3模型检验算法应用于布尔有限自动机，不仅可以有效地回答空性和普适性问题，而且通过扩展，可以判定多变量串成员问题的可满足性。我们证明了所产生的系统的有效性，一些流行的基准和正则表达式。
2017-08-30 cs.FL cs.LO cs.SC
Typestate Checking and Regular Graph Constraints
我们引入了正则图约束，并探讨其可判定性。规则图约束的动机是1）在存在链接的数据结构的情况下改变对象类型的类型检查，2）形状分析技术，以及3）在树和网格上的类似约束的泛化。我们定义了一个称为堆的图子类，作为程序在执行过程中构造的数据结构的抽象。证明了堆类上正则图约束蕴涵的有效性是不可判定的。我们表现出不可判定性表现出一定的“对应图”的存在和不存在的同态有限数量的固定图的特征。正则图约束蕴涵的不可判定性意味着，当这些属性用任何规约语言表达时，都没有算法来验证过程前提条件是否满足，或者不变量是否保持不变，至少与正则图约束一样具有表达性。
2004-08-05 cs.LO cs.PL
Algorithms for Omega-Regular Games with Imperfect Information
我们研究了基于观察的策略，两个球员回合制游戏的图与欧米茄定期目标。基于观察的策略依赖于关于戏剧历史的不完全信息，即过去的观察序列。这样的游戏发生在一个控制器的合成中，该控制器看不到植物的私有状态。我们的主要结果是双重的。首先，我们给出了一个不动点算法，用于计算一组状态，从该状态中，玩家可以用确定性的基于观察的策略来赢得任何ω-正则目标。不动点是在状态集的反链格中计算的。该算法具有目标导向和避免在博弈图上构造显式子集的优点。其次，我们给出了一个算法，用于计算一个球员可以赢得概率为1的随机观察为基础的战略Buechi目标的状态集。这个集合很有趣，因为在没有完美信息的情况下，随机策略比确定性策略更强大。我们证明了我们的算法是最佳的匹配下界。
2007-11-02 cs.GT cs.LO
Qualitative Analysis of Partially-observable Markov Decision Processes
我们研究了部分可观测马尔可夫决策过程（POMDPs）与欧米茄定期目标的观察为基础的战略。基于观察的策略依赖于关于游戏历史的部分信息，即过去的观察序列。我们考虑的定性分析问题：给定一个POMDP与一个欧米伽正则目标，是否有一个基于观察的策略，以达到目标的概率约1（几乎肯定获胜），或与积极的概率（积极获胜）。我们的主要结果是双重的。首先，我们提出了一个完整的图片的计算复杂性的定性分析POMDP的奇偶性目标（一个规范形式来表达ω-经常目标）及其子类。我们的贡献在于建立了几个在文献中不为人知的上限和下限。其次，我们提出了最佳的界限（匹配的上限和下限）的内存所需的纯随机观察为基础的策略，POMDP的奇偶校验目标及其子类的定性分析。
2010-06-09 cs.LO
Kofola 1.0: A Modular Approach to ω-Regular Complementation and Inclusion Checking (Technical Report)
Brno University of Technology（布尔诺理工大学）；Aalborg University（奥尔堡大学）；Key Lab. of System Software (Chinese Academy of Sciences), ISCAS（中国科学院系统软件重点实验室）；Slovak University of Technology in Bratislava（布拉迪斯拉发斯洛伐克科技大学）
Kofola 1.0 提出了一种高效的 Büchi 自动机补集与包含检查工具，基于模块化补集框架，结合新启发式方法，实验证明其在实际应用中性能优越。
2026-06-29 cs.FL cs.LO
Omega-Regular Objectives in Model-Free Reinforcement Learning
University of Liverpool（利物浦大学）；University of Colorado Boulder（科罗拉多大学博尔德分校）
我们提供了第一个解决方案，无模型强化学习的ω-正则目标的马尔可夫决策过程（MDP）。我们提出了一个建设性的减少从几乎肯定满足ω-正则目标的几乎肯定的可达性问题，并将这种技术推广到学习如何控制一个未知的模型，使满足目标的机会最大化。我们的技术的一个关键特征是将ω-正则性质编译成极限确定性Buechi自动机而不是传统的Rabin自动机;这种选择回避了破坏以前建议的困难。我们的方法使我们能够应用无模型，现成的强化学习算法来计算最佳策略的MDP的观察。我们提出了一个实验评估我们的技术对基准学习问题。
2018-09-26 cs.LG cs.LO stat.ML
Model-Checking of Ordered Multi-Pushdown Automata
我们解决了有序多下推自动机的验证问题：下推自动机的多栈扩展，具有对栈转换的约束，使得弹出只能在第一个非空栈上执行。首先，我们证明了有序多下推自动机的空问题是在2 ETIME。然后，我们证明了，对于一个有序的多下推自动机，一个正则配置集的所有前身的集合是一个有效的可构造正则集。我们利用这一结果来解决全球模型检验，其中包括在计算一个有序的多下推自动机，满足给定的w-正则性质（可表示在线性时间的时间逻辑或线性时间μ演算）的所有配置的集合。作为一个直接的后果，我们得到了一个2 ETIME上界的有序多下推自动机的w-正则性质的模型检验问题（匹配其下限）。
2012-09-19 cs.FL cs.LO
Reward Shaping for Reinforcement Learning with Omega-Regular Objectives
Queen’s University Belfast（贝尔法斯特女王大学）；Institute of Software, CAS（中国科学院软件研究所）；University of Colorado Boulder（科罗拉多大学博尔德分校）；University of Liverpool（利物浦大学）
最近，已经成功地利用良好的MDP自动机（Büchi自动机与非确定性的限制形式）的无模型强化学习，一类自动机，包括良好的游戏自动机和最广泛的一类限制确定性自动机。使用这些Büchi自动机的基础是，Büchi条件，对于良好的MDP自动机，可以转化为可达性。这种翻译的缺点是，平均而言，奖励很晚才获得，这需要在学习过程中长时间的插曲。我们设计了一种新的奖励塑造方法来克服这个问题。我们表明，由此产生的模型是等价于一个有偏见的折扣，简化和改善以前的工作在这个方向上的折扣收益目标。
2020-01-16 cs.LG cs.LO
A proof theory of (omega-)context-free languages, via non-wellfounded proofs
本文研究带不动点的正则表达式的证明理论，将其视为(omega-)上下文无关文法，通过引入最小和最大不动点扩展超序列系统，并利用证明论与博弈论技术证明其非良基证明的可靠性与完备性。
2024-04-24 cs.LO math.LO
Regular Model Checking Upside-Down: An Invariant-Based Approach
本文提出一种从上方逼近可达配置集合的常规模型检测补充方法，利用归纳不变量的交集构造正则自动机，并分析其复杂度与所需子句数。
2025-01-13 cs.DC cs.LO
Quantitative Verification of Omega-regular Properties in Probabilistic Programming
East China Normal University, China（华东师范大学）；Nanyang Technological University, Singapore（南洋理工大学）
本文提出时间后验推断框架，用于在概率编程中定量验证omega-正则性质，通过分解Rabin条件并构建随机屏障证书，实现对概率行为的高效推断。
2025-12-25 cs.FL cs.LG cs.LO
Supermartingale Certificates for Quantitative Omega-regular Verification and Control
本文提出首个用于定量ω正则性质的超鞅证书（LDBSM），并给出自动化合成算法，实验表明能解决先前方法无法处理的随机系统验证与控制任务。
2025-05-24 cs.LO cs.SY eess.SY
A proof theory of right-linear (omega-)grammars via cyclic proofs
本文提出右线性代数理论及循环证明系统 CRLA，证明其对正则语言可靠完备，并扩展到最大不动点系统 νCRLA 以刻画 ω-正则语言。
2024-01-24 cs.FL cs.LO math.LO
Revelations: A Decidable Class of POMDPs with Omega-Regular Objectives
CNRS（法国国家科学研究中心）；University of Antwerp（安特卫普大学）；Flanders Make（法兰德斯制造研究院）
针对POMDP中omega正则目标的可判定性问题，提出启示机制限制信息损失，将弱启示和强启示两类POMDP的可判定情形归结为有限信念支撑MDP，从而给出精确算法。
2024-12-16 cs.AI cs.LO cs.SY
Reduction of Register Pushdown Systems with Freshness Property to Pushdown Systems in LTL Model Checking
下推系统（PDS）是递归程序的一种抽象模型，下推系统的模型检验方法已得到研究。寄存器PDS（RPDS）是由寄存器扩展的PDS，以有限的方式处理来自无限域的数据值。一个线性时序逻辑（LTL）模型检验方法已被提出的RPDS与定期估值，但该方法要求用于表示一个定期估值的寄存器自动机（RA）是向后确定的。本文提出了另一种方法来解决同样的问题，其中的模型检验问题的RPDS归结为PDS的问题，通过构造一个PDS互模拟等价于一个给定的RPDS。所提出的方法的结构比以前的模型检验方法更简单，不需要RA确定性或后向确定性，互模拟等价性清楚地保证了这种减少的正确性。另一方面，所提出的方法要求每个RPDS（和RA）具有新鲜度属性，其中每当RPDS用未存储在任何寄存器或栈顶中的数据值更新寄存器时，该值应该是新鲜的。本文还表明，这种模型检验问题的定期评估定义的一般RA是不可判定的，因此新鲜度约束是必要的，在所提出的方法。
2022-03-22 cs.FL cs.LO
On the Complexity of Model Checking for Syntactically Maximal Fragments of the Interval Temporal Logic HS with Regular Expressions
本文研究了Halpern和Shoham的区间时序逻辑HS的模型检验问题。在过去的几年里，间隔时态逻辑MC作为传统（基于点）时态逻辑MC的可行替代方案越来越受到关注，传统时态逻辑MC可以被恢复为特殊情况。大多数结果都是在同质性假设下得到的，即约束一个命题字母在一个区间上成立当且仅当它在每个分量状态上成立。最近，Lomuscio和Michaliszyn提出了一种放松这种假设的方法，利用正则表达式来定义命题字母在其组成状态方面的行为。当同质性假设，MC的确切复杂性是一个困难的公开问题，充分HS和它的两个句法最大片段AA'BB' E '和AA' EB 'E'。在本文中，我们提供了一个渐近最优的约束下，这两个片段的复杂性更有表现力的语义变体的基础上，正则表达式的MC问题是AEXP_pol-完成，其中AEXP_pol表示的复杂性类的问题，由指数时间有界的交替图灵机，使一个多项式有界的交替。
2017-09-07 cs.CC cs.LO
Forward Analysis and Model Checking for Trace Bounded WSTS
我们研究了良结构变迁系统（WSTS）的一个子类，即Ginsburg和Spanier（trans. AMS 1964）意义下的有界完全确定性系统，我们认为它为Finkel和Goubault-Larrecq（Logic. Meth. Comput. Sci. 2012年）。事实上，我们证明，不同于其他条件考虑以前终止的前向分析，有界性是可判定的。有界性被证明是一个有价值的限制WSTS验证，因为我们表明，它进一步允许决定所有的$ω$ -经常属性的无限的痕迹的系统。
2016-03-04 cs.LO
Regular Model Checking Approach to Knowledge Reasoning over Parameterized Systems (technical report)
我们提出了一个通用的框架，建模和验证的认识属性参数化的多智能体系统，通过真实的公告进行通信。在我们的框架中，代理的数量或某些资源的数量被参数化（即先验未知），相应的验证问题询问给定的认知属性是否为真，而不管参数的实例化。例如，在一个泥泞的儿童拼图中，人们可以问每个孩子是否最终都会发现他是否泥泞，而不管孩子的数量。我们的框架是定期模型检验（RMC）为基础的，其中同步有限状态自动机（相当于一元二阶逻辑的话）被用来指定系统。我们提出了一个公共声明逻辑的扩展作为规约语言。特别感兴趣的是增加了所谓的迭代公共公告运营商，这是至关重要的推理知识参数化系统。虽然运营商的模型检验问题不可判定的，我们表明，这成为一个适当的“消失关系”时，可判定的。此外，我们展示了如何Angluin的L* 算法学习有限自动机可以应用到找到一个消失的关系，这是保证终止，如果它是正规的。我们已经实现了该算法，并将其应用于这样的例子，如泥泞的儿童拼图，俄罗斯卡问题，大数挑战。
2021-03-08 cs.FL cs.LO cs.MA
Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints
Technische Universität München（慕尼黑工业大学）；Université libre de Bruxelles（布鲁塞尔自由大学）
我们形式化的问题，最大化的平均支付值的高概率，同时满足奇偶性目标的马尔可夫决策过程（MDP）未知的概率转移函数和未知的奖励函数。假设支持的未知的过渡函数和最小的转移概率的下限是已知的，我们表明，在MDP组成的一个单一的端组件，两个组合的保证奇偶校验和平均回报的目标可以实现取决于有多少内存的人愿意使用。(i)对于所有的$ε$和$γ$，我们可以构造一个在线学习的有限记忆策略，该策略几乎肯定满足奇偶性目标，并且以至少$1 - γ$的概率实现$ε$ -最优平均收益。(ii)或者，对于所有的$ε$和$γ$，存在一个在线学习的无限记忆策略，它肯定满足奇偶性目标，并以至少$1 - γ$的概率实现$ε$ -最优平均收益。我们将上述结果推广到由一个以上的终端组件在一个自然的方式MDP。最后，我们表明，上述保证是紧的，即有MDP的更强的组合的保证不能确保。
2018-08-23 cs.AI cs.LO
Simple strategies for Banach-Mazur games and fairly correct systems
在2006年，Varacca和Völzer证明了在有限图上，omega-正则大集与概率为1的omega-正则集重合，通过使用相关的Banach-Mazur博弈中位置策略的存在性。受这一结果的启发，我们试图理解概率为1的集合与各种简单策略概念之间的关系（包括Grädel和Lessenich最近的一篇论文中介绍的概念）。然后，我们介绍了一个概括的经典巴拿赫-马祖尔游戏，特别是，概率版本，其目标是将集合的概率为1（作为经典巴拿赫-马祖尔游戏将大型集）。当获胜集是开集的可数交时，我们得到了这些博弈的一个决定性结果。
2013-07-17 cs.LO
Tree Regular Model Checking for Lattice-Based Automata
树规则模型检验（TRMC）是分析无限状态系统的一系列技术的名称，其中状态由项表示，状态集由树自动机（TA）表示。TRMC的核心问题是判断一组坏状态是否可达。计算表示可达状态集合（的过近似）的TA的问题是不可判定的，但是存在基于树换能器的完成或迭代的有效解决方案。不幸的是，TRMC框架无法有效地捕获系统的复杂结构及其某些功能。作为示例，对于JAVA程序，项的结构主要用于捕获系统的状态的结构。相反，Java程序的整数必须用Peano数编码，这意味着任何代数运算都可能由数千个重写规则的应用程序表示。在本文中，我们提出了格树自动机（LTA），树自动机的扩展版本，其叶子配备了格。LTA允许我们表示可能无限的解释术语集。这些术语能够以有效的方式表示复杂的域和相关操作。我们还将经典的布尔运算扩展到LTA。最后，作为一个主要的贡献，我们引入了一个新的基于完成的算法计算可能无限的可达解释条款在有限的时间。
2012-03-07 cs.FL cs.LO
Stochastic Omega-Regular Verification and Control with Supermartingales
本文首次提出Streett超鞅证书，用于随机动态系统的ω-正则规范验证与控制，算法可靠完备，并优化为SMT求解，原型实验验证有效。
2024-05-27 cs.LO cs.SY eess.SY
Three Applications to Rational Relations of the High Undecidability of the Infinite Post Correspondence Problem in a Regular omega-Language
Harel在[Har 86]中指出，“人们可以定义$Σ_1^1$ -著名的Post Correspondence Problem的完全版本”。我们首先给出了这个结果的一个完整的证明，表明在一个正规的$ω$ -语言的无限后对应问题是$Σ_1^1$ -完全的，因此位于算术层次之外，高度不可判定。我们从这个结果推断，它是$Π_1^1$ -完全的，以确定是否两个给定的无穷有理关系是不相交的。然后证明了有限状态Büchi变换器实现的$ω$ -有理函数的两个判定问题之间存在着惊人的差距。事实上Prieur证明在[Pri 01，Pri 02]，这是决定是否一个给定的$ω$ -有理函数是连续的，而我们在这里表明，它是$Σ_1^1$ -完全确定是否一个给定的$ω$ -有理函数至少有一个点的连续性。其次证明了判定给定$ω$ -有理函数的连续集是否是$ω$ -正则的是$Π_1^1$ -完全的。这给出了[CFS 08]中证明为不可判定的两个问题的精确复杂度。
2011-07-29 cs.CC cs.LO math.LO
Wadge degrees of $Δ^0_2$ omega-powers
该研究针对不同的Borel差分层类，构造出对应ω幂为该类完全集的正则语言，刻画了$\Delta^0_2$ ω幂的Wadge度相关性质。
2024-07-15 cs.LO math.GN math.LO
RNN Generalization to Omega-Regular Languages
Imperial College London, UK（伦敦帝国学院）
本研究首次探究RNN对LTL导出的ω-正则语言的泛化能力，通过训练RNN复现Büchi自动机行为并测试分布外长序列，证实其在多数复杂任务上可实现高精度泛化，为神经符号验证提供了可行性支撑。
2025-09-02 cs.FL cs.LG cs.LO
Characterizing Omega-Regularity through Finite-Memory Determinacy of Games on Infinite Graphs
本文通过无限图博弈的有限记忆决定性刻画了ω-正则目标，证明双方玩家在色度有限记忆下最优时目标必为ω-正则，并提供了一对二玩家提升及折扣和目标的实例。
2023-01-13 cs.FL cs.GT cs.LO
Model-checking parametric lock-sharing systems against regular constraints
本文研究参数化锁共享系统在强公平性下的无限行为验证问题，证明其在嵌套锁使用下可判定且为 Exptime 完全，并在 spawn 参数有界时对固定秩奇偶自动机性质给出 Ptime 算法。
2023-07-10 cs.DC cs.FL cs.LO
Certificates and Witnesses for Multi-objective ω-regular Queries in Markov Decision Processes
针对马尔可夫决策过程中多目标ω-正则查询，提出独立可验证的证书与证据，扩展改进现有证书推导MILPs找最小见证子系统，特例下用无歧义Büchi自动机获单指数空间算法，实现并验证技术有效性。
2025-08-25 cs.LO
There Exist some Omega-Powers of Any Borel Rank
有限语言的Ω幂是以V^Ω形式存在的无限词的语言（Ω语言），其中V是有限字母表X上的有限语言。它们非常自然地出现在正则或上下文无关的omega语言的特征中。由于有限字母表X上的无限词的集合可以配备通常的Cantor拓扑，有限语言的Ω幂的拓扑复杂性问题自然出现，并由Niwinski（1990），Simonnet（1992）和Staiger（1997）提出。最近证明了：对任意整数n > 0，存在若干上下文无关语言的Ω幂，它们是Pi^0_n-完备Borel集;存在上下文无关语言L，使得L^Ω是解析的而不是Borel集;存在有限语言V，使得V^Ω是无限秩的Borel集。但它仍然是未知的可能是无限的波莱尔列欧米伽权力。我们在这里填补了这个空白，证明了下面这个非常令人惊讶的结果，它表明omega-幂表现出很大的拓扑复杂性：对于每个非零可数序数alpha，存在一些Sigma^0_alpha-完全omega-幂，和一些Pi^0_alpha-完全omega-幂。
2007-06-25 cs.CC cs.LO math.LO
HornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses(Technical Report)
HornStr 是首个将正则模型检验的不变式合成转化为字符串上的约束 Horn 子句问题的求解器，支持 L* 和基于 SAT 的自动机学习，并自动验证 MU 谜题，生成超 30000 个新基准。
2025-05-23 cs.FL cs.LO
Multi-Objective Model Checking of Markov Decision Processes
研究并给出了马尔可夫决策过程多目标模型检验问题的有效算法。给定MDP，M，以及给定多个线性时间（ω-正则或LTL）性质φ i，以及概率ri ε[0，1]，i=1，.，k，我们问是否存在控制器的策略σ，使得对于所有i，由σ控制的M的轨迹满足φ i的概率至少为ri。我们提供了一个算法，决定是否存在这样的策略，如果是这样产生它，并运行在时间多项式中的MDP的大小。这种策略可能需要同时使用随机化和内存。我们还考虑了更一般的多目标ω-正则查询，我们激励与应用的假设保证组合推理的概率系统。注意，在不同属性之间可以存在折衷：以高概率满足属性φ 1可能需要以低概率满足φ 2。将其视为多目标优化问题，我们需要关于“权衡曲线”或帕累托曲线的信息，以最大化不同属性的概率。我们证明了在MDP的大小下，可以计算关于时间多项式中的一组ω-正则性质的近似Pareto曲线。我们的定量上限使用LP方法。我们还研究了定性的多目标模型检验问题，我们表明，这些可以通过纯粹的图论方法进行分析，即使策略可能仍然需要随机化和内存。
2008-11-11 cs.CC cs.GT cs.LO
Learning to Prove Safety over Parameterised Concurrent Systems (Full Version)
我们重新审视了经典的问题，证明安全的参数化并发系统，即，用有限（符号）方法表示的有限状态并发系统的无限族。这样的无限族的一个例子是一个用餐哲学家协议，具有任意数量的n个进程（n是定义无限族的参数）。常规模型检验是一种用于参数化并发系统建模的通用框架，其中无限组的配置（分别为：transitions）由正则集（resp.常规换能器）。虽然在常规的模型检验框架中验证安全属性通常是不可判定的，但是在过去的15年中已经开发了许多复杂的半算法，可以在许多实际情况中成功地证明安全性。在本文中，我们提出了一个简单的解决方案，利用Angluin的经典L* 算法（及其变体）来合成正则归纳不变量。我们提供了一个终止保证时，从一组给定的初始配置可达的配置集是定期的。我们已经测试了L* 算法的标准（以及新的）的例子，在定期的模型检验，包括用餐哲学家协议，用餐密码协议，和几个互斥协议（如面包店，伯恩斯，Szymanski，和德国）。我们的实验表明，尽管我们的解决方案的简单性，它可以执行至少以及现有的半算法。
2017-10-03 cs.FL cs.LO cs.PL
Natural Colors of Infinite Words
虽然有限自动机有最小的DFA作为一个简单和自然的范式，确定性欧米茄自动机目前没有任何类似的。其中一个原因是，欧米茄-正则语言的范式必须谈论的不仅仅是接受-例如，要有奇偶校验语言的范式，它应该将每个无限的单词与这种语言的某种自然颜色联系起来。这就提出了一个问题：是否存在一个概念，比如一个无限单词的自然颜色（对于一种给定的语言），如果存在，它是如何与自动机联系起来的。我们定义的自然颜色的一个字纯粹的基础上的欧米茄-正则语言，并显示这种自然的颜色可以追溯到任何确定性的奇偶自动机后，两个廉价和简单的自动机转换。由此产生的流线型自动机不一定接受每个具有自然颜色的单词，但它有一个“共同运行”，这就像一个运行，但可以一次移动到语言等价状态，其颜色是自然颜色，不存在具有更高颜色的共同运行。流线型自动机为每个颜色c定义了一个适合游戏的co-Büchi自动机，该自动机识别出其自然颜色w.r.t.所表示的语言至少是C。这为每个$ω$ -正则语言提供了一个规范表示，因为适合游戏的co-Büchi自动机对每个co-Büchi语言都有一个规范的最小（并且容易获得）表示。
2022-07-22 cs.FL cs.LO
A Theory of Hanoi Omega-Automata and Games
Université libre de Bruxelles（布鲁塞尔自由大学）；University of Antwerp（安特卫普大学）
本文研究了HOA编码自动机与游戏的理论复杂性，证明非空问题为NP完全，语言包含问题在多数条件下为PSPACE完全，Emerson-Lei接受条件为EXPSPACE完全，并形式化了HOG游戏。
2026-04-27 cs.FL cs.LO
The memory of $ω$-regular and BC($Σ_2^0$) objectives
University of Kaiserslautern-Landau（凯泽斯劳滕-兰道大学）；CNRS, Laboratoire d’Informatique et des Systèmes (LIS)（法国国家科学研究中心，信息系统实验室）
研究双人零和无限博弈中目标的记忆，针对$\omega$-正则和BC($\Sigma_2^0$)目标，证明了记忆可判定性，给出了记忆有界自动机类，并推导出记忆计算复杂度及并集记忆上界。
2026-06-03 cs.FL cs.LO
