Reasoning about Knowledge and Strategies under Hierarchical Information
两个不同的语义已被认为是知识的背景下，战略推理，这取决于球员是否知道对方的战略或没有。分布式合成的问题是已知的认知时间规范是不可判定的，后者的语义，已经在系统的层次信息。然而，对于其他的，不知情的语义，这个问题是决定这样的系统。在这项工作中，我们概括了这一结果，通过引入不完美信息的战略逻辑的认知扩展。知识算子的语义是不知情的，并捕获代理，可以改变观察力，当他们改变策略。我们解决了一类“层次实例”的模型检查问题，这提供了一个解决方案，一个巨大的类的战略问题与认知的时间规范层次系统，如分布式综合或合理的综合。
2018-09-03 cs.LO
Revisiting Parameter Synthesis for One-Counter Automata
研究了带参数的单计数器自动机的参数综合问题。单计数器自动机是将经典的有限状态自动机扩展为一个计数器，该计数器的值可以在非负整数范围内变化，并且可以测试为零。通过引入一组称为参数的整数值变量，可以进一步使适用于计数器的更新和测试参数化。这样的自动机的合成问题问是否存在一个参数的估值，使所有的无限运行的自动机满足一些欧米茄正则性质。Lechner证明了这个问题（的补充）可以被编码在具有可除性的Presburger算术的一个受限的交替片段中。在这项工作中（i），我们认为，所说的片段，称为AERPADPLUS，不幸的是不可判定的。然而，通过仔细重新编码的问题到一个可判定的限制AERPADPLUS，（ii）我们证明了合成问题是可判定的一般和N2 EXP的几个固定的Ω-经常性。最后，（iii）我们给出了一个多项式空间算法的特殊情况下的问题，参数只能用于测试，而不是更新，计数器。
2021-10-19 cs.FL cs.LO
Complexity of Verification and Synthesis of Threshold Automata
Technical University of Munich（慕尼黑工业大学）
本文研究了阈值自动机的验证与合成问题的复杂性，证明了多个核心问题的计算复杂度，并提出了一种基于Presburger公式的新算法。
2025-11-28 cs.DC cs.LO
Exploiting the Temporal Logic Hierarchy and the Non-Confluence Property for Efficient LTL Synthesis
从线性时序逻辑（LTL）规范合成反应系统的经典方法首先将给定的LTL公式转换为等价的omega-自动机，然后计算相应的omega-正则博弈的获胜策略。为此，所获得的欧米茄自动机必须（伪）确定，其中通常使用萨夫拉的确定过程的变体。在本文中，我们表明，这一确定步骤可以显着改善工具的实现取代萨夫拉的确定更简单的确定程序。特别地，我们利用（1）对应于由安全、活性、Buechi和co-Buechi自动机以及它们的布尔闭包组成的著名自动机层次的时态逻辑层次，（2）由LTL公式的某些平移产生的omega-自动机的非汇合性质，（3）Rabin-Scott和Miyano-Hayashi断点构造的确定过程的符号实现。特别是，我们提出了令人信服的实验结果，证明了我们的新的合成过程的实用性。
2010-06-08 cs.LO
Polynomial Synthesis of Asynchronous Automata
Zielonka定理表明，Mazurkiewicz迹的每一个规则集都可以实现为具有称为异步自动机的分布式控制结构的同步过程系统。本文给出了一个从正则Mazurkiewicz迹语言综合非确定异步自动机的多项式算法。这种新的结构是基于一种展开的方法，提高了Zielonka和Pighizzini的技术在状态数量方面的复杂性。
2005-06-27 cs.CC cs.LO
Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis
概率系统的模型检测问题主要依赖于将LTL转换为确定性Rabin自动机（DRW）。我们最近的Safraless翻译的LTL（F，G）片段产生较小的自动机相比，传统的方法。在这项工作中，而不是DRW，我们认为确定性自动机的接受条件作为广义拉宾对（DGRW）的析取。与DRW相比，LTL（F，G）公式到DGRW的Safraless翻译导致更小的自动机。我们提出了概率模型检测算法以及DGRW条件下的博弈求解。我们的新算法在理论界和实际评价方面都有所改进。我们比较PRISM与我们的新的翻译，并表明，新的翻译导致显着的改善。
2013-04-18 cs.FL cs.LO
Reactive Synthesis for DECLARE via symbolic automata
给定一个规范的线性时间的时间逻辑解释有限的痕迹（LTLf），反应性合成问题要求找到一个有限表示的，终止控制器的反应，以执行所需的系统规范的不可控的行动的环境。在本文中，我们研究，第一次，反应性的综合问题，DEQUE-一个片段的LTLf广泛用于在理论和实践中指定声明性的，基于约束的业务流程。我们提供三方面的贡献。首先，我们给出了一个朴素的，双指数时间综合算法。第二，我们展示了如何任意的DEPENE规范可以compensarily编码成一个等价的纯过去的LTLf，我们利用这一点来定义一个优化的，单指数时间算法DEPENE合成。第三，我们推导出一个符号版本的算法，通过引入一个新的翻译纯过去的时间公式符号确定性有限自动机。
2022-12-21 cs.FL cs.LO
Resource-Aware Automata and Games for Optimal Synthesis
我们考虑定量的奇偶自动机和奇偶游戏的概念，旨在模拟资源感知行为，并研究（内存满）策略展示接受运行，需要最小量的初始资源，分别为赢得一个游戏，最小的初始资源。我们还展示了这样的策略可以被简化为只包括两种类型的移动：前者旨在增加资源，后者旨在满足接受条件。
2019-09-17 cs.GT cs.LO
Incorporating Monitors in Reactive Synthesis without Paying the Price
时态合成试图构造满足给定声明式（LTL）公式的反应式程序。实践者发现只使用声明性规范是很有挑战性的，并且发现将建模与声明性规范结合起来的语言更有用。合成控制器还可能需要与预先存在的或手动构建的程序一起工作。在本文中，我们将探讨一种方法，结合合成的声明性规范在现有的行为模型作为一个监视器的存在下，没有理由的监视器的状态空间的好处。我们建议一个形式语言与自动机监视器作为非重复和重复触发器的LTL公式。我们使用具有内存的符号自动机作为触发器，从而产生比现有正则表达式触发器更严格的表达性和简洁的语言。我们给这种语言的合成过程中，推理的监视器状态空间是最小的。为了展示我们的方法的优势，我们将其应用于需要对任意长的事件序列进行计数和约束的规范，在那里我们也可以看到参数化的力量，在我们的方法中很容易处理。我们提供了一个工具来构造控制器（符号自动机的形式）为我们的语言。
2021-07-02 cs.LO
A Curry-Howard Approach to Church's Synthesis
本文通过 Curry-Howard 对应关系，引入直觉主义变体 SMSO 并借助自动机可实现性模型，为 Church 综合问题提供了可靠且完备的算法求解方法。
2019-12-06 cs.LO
Real-Time Model-Checking: Parameters everywhere
本文研究离散时间自动机上逻辑TCTL的模型检验和参数综合问题，其中参数在模型（时间自动机）和属性（时态公式）中都允许.我们的结果如下。在消极的一面，我们表明，模型检验问题的TCTL扩展参数是不可判定的离散时间自动机只有一个参数时钟。不可判定性结果需要逻辑上的等价性。在积极的一面，我们表明，模型检验和参数合成问题成为可判定的一个片段的逻辑是不允许的平等。我们的方法是基于自动机理论的原则和扩展我们的方法来表示时间自动机使用Presburger算法的运行持续时间。
2007-02-27 cs.LO
Automatic Synthesis of Switching Controllers for Linear Hybrid Automata
Università di Napoli “Federico II”（那不勒斯费德里科二世大学）
针对线性混合自动机，提出基于多面体抽象状态空间的符号不动点程序，自动生成满足安全目标的切换控制器，并证明每次迭代的终止性。
2011-08-04 cs.FL cs.LO cs.SY
The Extended HOA Format for Synthesis
我们提出了一个小的扩展河内欧米茄自动机格式定义反应合成问题。也就是说，我们添加了一个“可控制的AP”头项，指定原子命题的子集是可控的。我们描述了新格式的语义，并提出了一个输出格式的合成策略。最后，我们还评论了工具支持，旨在鼓励快速采用扩展的河内Omega-Automata格式进行合成。
2020-05-13 cs.FL cs.LO
DeepSynth: Automata Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning
University of Oxford（牛津大学）
本文提出了DeepSynth，这是一种有效训练深度强化学习（RL）代理的方法，当奖励是稀疏和非马尔可夫的，但同时朝着奖励的进展需要实现未知的高级目标序列。我们的方法采用了一种新的算法，紧凑的自动机的合成，自动发现这种顺序结构。我们从探索环境收集的跟踪数据中合成了一个人类可解释的自动机。然后用合成的自动机来丰富环境的状态空间，使得由深度RL生成的控制策略由在自动机中编码的发现的结构来指导。该方法能够同时处理高维、低层特征和未知稀疏非马尔可夫回报。我们在一系列实验中评估了DeepSynth的性能，其中包括Atari游戏Montezuma的复仇。与现有的方法相比，我们得到了减少两个数量级的策略合成所需的迭代次数，也是一个显着的可扩展性的改善。
2021-03-06 cs.AI cs.LG cs.LO
Parameter Synthesis Problems for one parametric clock Timed Automata
RISE, Southwest University（西南大学 RISE）；Department of Computer Science and Informatioin Systems, Birkbeck, University of London（伦敦大学伯贝克学院计算机科学与信息系统系）；LMAM & School of Mathematical Sciences, Peking University（北京大学数学科学学院 LMAM）；State Key Laboratory of Computer Science, Institute of Software, CAS（中国科学院软件研究所 计算机科学国家重点实验室）；CISS, CS, Aalborg University（奥尔堡大学计算机科学与工程系 CISS）
本文研究了一类参数时钟时序自动机的参数合成问题，通过线性表达式和参数多项式不等式约束，确定参数估值的可行区域以满足特定属性。
2018-09-15 cs.FL cs.LO cs.SY
On the Control of Asynchronous Automata
Ramadge和Wonham控制器综合问题的分布式版本的可判定性是一个具有挑战性的公开问题，其中对象和控制器都被建模为异步自动机，并且控制器具有因果记忆。存在三类对象，其具有因果记忆的正确控制器的存在已被证明是可判定的：当动作的依赖图是串并行时，当进程连接地通信时，以及当进程的依赖图是树时。设计了一类具有可判定控制器综合问题的可分解对策，给出了已有的三个可判定性结果的统一证明，并给出了可判定对策的新例子.
2017-08-04 cs.FL cs.LO
Synthesis of Temporal Causality
本研究推广时序因果性框架，提出首个针对ω-正则效应的完备原因合成算法，证明其原因具有ω-正则性，可通过原型工具实现并验证了实际性能。
2025-06-17 cs.LO
Supervisory Controller Synthesis for Non-terminating Processes is an Obliging Game
本文提出了一种新的算法来解决被建模为$ω$ -正则自动机的非终止过程的监督控制问题。这个问题的解决方案是由Thistle在1995年获得的，它使用了自动机的复杂操作。我们展示了一个新的解决方案，通过减少义务游戏，这反过来，可以减少到$ω$ -定期反应合成的问题。因此，我们的减少结果在一个符号算法的基础上操纵状态集使用的工具反应合成。
2021-08-26 cs.LO cs.SY eess.SY
Bounded Synthesis of Reactive Programs
大多数反应系统的综合算法都集中在有限状态机的构造上，而不是实际的程序。这通常会导致结构不良、不可读的代码。在本文中，我们提出了一个有界的合成方法，自动构造，从一个给定的规范在线性时间时序逻辑（LTL），一个程序在Madhusudan的简单的命令式语言的反应程序。我们开发和比较两个主要的方法减少的综合问题的布尔约束满足问题。第一个约简是基于有界合成到双向交替自动机的推广，第二个约简是基于约束系统中程序语法的直接编码。我们报告的初步经验与原型实现，这表明直接编码优于自动机的方法。
2018-07-24 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
Verification of Parametric Markov Automata under Time-bounded Reachability
Eindhoven University of Technology（埃因霍温理工大学）
针对参数化马尔可夫自动机（pMA），提出通过离散化为参数化马尔可夫决策过程（pMDP）并分析，解决时间有界可达性概率的合成问题，实现参数空间的满足/违反区域划分。
2026-06-23 cs.LO
The Church Synthesis Problem over Continuous Time
该研究将丘奇综合问题推广至非负实数连续时间域，发现连续时间域存在与标准离散自然数域截然不同的现象，拓展了该问题的研究范畴。
2025-07-22 cs.LO
Parameter Synthesis for Cardiac Cell Hybrid Models Using Delta-Decisions
系统生物学中的一个中心问题是确定参数值，使得生物模型满足某些行为约束（\eg，时间序列）。在本文中，我们专注于混合（连续/离散）模型的参数合成，因为许多生物系统可以拥有多个操作模式，在每个模式中具有特定的连续动态。这些生物系统自然地被建模为混合自动机，通常具有非线性连续动力学。然而，混合自动机是出了名的难以分析-即使是简单的可达性混合系统的线性微分动力学是一个不可判定的问题。在本文中，我们提出了一个参数综合框架的基础上$δ$ -完全决策过程，回避不可判定性。我们证明了我们的方法对两个高度非线性混合模型的心脏细胞动作电位。结果表明，我们的参数合成框架是方便和有效的，它使我们能够选择一个合适的模型来研究和确定与心脏疾病相关的关键参数范围。
2014-09-10 cs.CE cs.LO q-bio.QM
A Note on Fault Diagnosis Algorithms
在本文中，我们审查算法检查离散事件系统和时间自动机的可诊断性。我们指出，在这两种情况下的可诊断性问题减少到空性问题（定时）Büchi自动机。此外，它是已知的，检查是否离散事件系统是可诊断的，也可以减少到检查有界可诊断性。我们建立了一个类似的时间自动机的结果。我们还提供了一个综合的复杂性结果，为不同的故障诊断问题。
2010-04-16 cs.FL cs.LO
Control and Synthesis of Non-Interferent Timed Systems
ClearSy；IRCCyN laboratory, LUNAM Université, Ecole Centrale Nantes（南特大学、中央理工学院）；National ICT Australia（澳大利亚国家信息技术澳大利亚）
本文针对定时自动机模型，研究如何通过控制综合得到满足强非确定性非干扰（SNNI）及其基于（双）模拟的变体（CSNNI和BSNNI）的安全定时系统，并解决检查是否存在非干扰子系统以及计算最大非干扰子系统的问题。
2012-07-11 cs.FL cs.LO cs.SY
Deciding the synthesis problem for hybrid games through bisimulation
本文通过交替互模拟将初始化奇异混合博弈归约为时间博弈，并利用策略翻译引理，借助时间博弈工具为混合博弈合成获胜策略。
2024-09-30 cs.FL cs.LO
Synthesis of Sequential Extended Regular Expressions for Verification
综合技术采用可实现的线性时序逻辑规范，并产生实现规范的正确电路。生成的电路可以直接使用，也可以用作检查逻辑设计正确性的斜接。通常，这些技术生成非确定性有限状态自动机，其可以以可能的指数代价确定。最近的研究结果表明，使用确定性自动机的符号和有界模型检验的LTL安全性能的多个优点。在本文中，我们提出了一种技术与支持工具，采取一个顺序扩展的正则表达式规范Φ，和一个逻辑设计实现S，并生成一个时序电路C，表示为一个与反转图，检查是否S满足Φ。该技术将生成的电路C传递给有界模型检查器ABC，以验证正确性。我们用自由输入变量对Φ中的不确定性进行编码，得到了许多状态，它们与Φ的大小成斜接线性关系。我们的技术成功地生成了模型检查器的输入，而其他技术由于指数爆破而失败，并且在大多数情况下，ABC成功地找到了设计中的缺陷，否则无法检查，或者验证了设计。我们评估了我们的技术对几个工业基准，包括IBM仲裁器，负载平衡器，和交通灯系统，并比较我们的结果与NuSMV框架。我们的方法发现了缺陷，并且验证了NuSMV无法验证的系统。
2014-01-14 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
Resolving Nondeterminism with Randomness
IST Austria（奥地利科学技术研究所）；University of Warwick（华威大学）
本文定义并研究了通过结合记忆和随机性的策略在任意输入词上解决非确定性选择的ω-正则自动机类，包括对抗性可解和随机性可解两种设置，并分析了新自动机类在简洁性、表达力和计算复杂性之间的权衡。
2025-02-18 cs.FL cs.LO
Distributed synthesis for acyclic architectures
Université de Bordeaux（波尔多大学）；CNRS, Université de Bordeaux（法国国家科学研究中心，波尔多大学）
研究无环通信图下分布式系统的合成问题，证明了对所有omega-正则局部规范的可判定性，扩展了之前局部可达性规范的可判定性结果。
2014-07-16 cs.LO cs.SY eess.SY
