Symbolic Optimal Reachability in Weighted Timed Automata
加权时间自动机在2000年初被定义用于建模实时系统中的资源消耗或分配问题。在加权时间自动机中，最优可达性是可判定的，并提出了一种符号前向算法来解决这一问题。该算法使用所谓的定价区域，即具有成本函数的标准区域的扩展。为了确保终止，该算法要求时钟有界。对于未定价的时间自动机，已经做了很多工作来开发适合于时间自动机的前向探索的合理抽象，确保在不限制时钟的情况下终止模型检查算法。在本文中，我们利用最近的发展抽象的时间自动机，并提出了一个算法，允许符号分析的所有加权时间自动机，而不需要有界的时钟。
2016-02-01 cs.LO
The Complexity of Satisfiability Checking for Symbolic Finite Automata
本文研究符号有限自动机的可满足性问题，通过将其分解为输入字符理论与接受单词索引的单子二阶理论，获得了该自动机类及其线性算术约束扩展的紧计算复杂度界限。
2023-06-30 cs.LO
Complementing Büchi Automata with Ranker (Technical Report)
我们提出了一个补充Büchi自动机（BA）的工具Ranker。Ranker建立在我们之前对基于秩的BA互补的优化基础上，并使用许多算法进一步推动它们，以产生更小的自动机。此外，它还包含了对专门构造的新颖优化，以补充（i）固有的弱自动机和（ii）半确定性自动机，所有这些都在一个强大的工具中提供。这些优化显著提高了Ranker的可用性，正如对真实世界基准的广泛实验评估所示，在大多数情况下，Ranker产生的补充比其他最先进的工具要少。
2022-06-04 cs.FL cs.LO
Symbolic Simulation-Checking of Dense-Time Systems
直观地说，一个（实现）自动机被一个（规范）自动机模拟，如果实现自动机的每个外部可观察的转换也可以由规范自动机完成。在这项工作中，我们提出了一个符号算法的时间自动机的模拟检查。我们首先提出了一个模拟检查程序，操作状态空间，表示与凸多面体，时间自动机。然后，我们提出的技术来表示这些中间结果凸多面体的区域，并使该过程的算法。然后，我们讨论如何在实现自动机中处理芝诺状态。最后，我们完成了算法的实现，并在实验中报告了我们的算法的性能。
2006-10-13 cs.LO cs.SE
Sky Is Not the Limit: Tighter Rank Bounds for Elevator Automata in Büchi Automata Complementation (Technical Report)
我们提出了几种方法来减轻Büchi自动机（BA）基于秩的互补中组合爆炸的主要原因之一：不必要的状态秩上限。首先，我们确定电梯自动机，这是一个大类的BA（广义半确定性BA），经常发生在实践中，其中行列的状态是有界的强连接组件的结构。电梯自动机的边界也可以扩展到包含电梯自动机作为子结构的一般BA。其次，我们介绍了两种技术，用于细化边界的BA状态的行列使用数据流分析的自动机。我们实现了技术作为BA互补工具的扩展，并表明它们确实大大修剪了生成的状态空间，获得了显着更好的结果，并在大量基准测试中优于其他最先进的工具。
2022-01-27 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
Symbolic Representation of Algorithmic Game Semantics
在本文中，我们重新审视了二阶递归自由的理想化算法与无限数据类型的游戏语义的正则语言表示。通过使用符号值，而不是具体的，我们推广的标准概念的正规语言和自动机表示相应的符号表示。通过这种方式，具有无限数据类型的项（例如整数）可以表示为有限符号自动机，尽管标准自动机的解释是无限的。此外，游戏语义模型的状态空间的显着减少。这使得能够有效地验证术语，这通过几个示例来说明。
2012-10-09 cs.FL cs.GT cs.LO
Reducing (to) the Ranks: Efficient Rank-based Büchi Automata Complementation (Technical Report)
本文对基于秩的Büchi自动机的补充方法进行了几种优化。我们从Schewe的理论上最优的建设，并制定了一套技术修剪其状态空间，是关键，以获得小补充自动机在实践中。特别是，这些约简（除了一个）具有保留（至少一些）所谓的超紧运行的性质，这些运行的排名尽可能紧。我们对一个大型基准的评估表明，优化确实显着帮助基于秩的方法，并在大量的情况下，所获得的补充是最小的，从大量的国家的最先进的工具产生的Büchi互补。
2021-07-21 cs.FL cs.LO
Succinct Determinisation of Counting Automata via Sphere Construction (Technical Report)
本文提出了一种确定计数自动机的有效算法，有界计数器扩展的有限自动机。该算法避免了将计数器展开为控制状态，这与朴素的方法不同，因此产生了更小的确定性自动机。我们还开发了一个简化和更快的版本的一般算法的子类所谓的一元CA（MCA），即，在字符类上使用计数循环的CA，这在实践中很常见。我们的主要动机是（除了在逻辑的验证和决策过程中的应用）确定性（M）CA在模式匹配正则表达式中的应用计数，这是非常常见的，例如，网络流量处理和日志分析。我们已经根据这些应用领域的实际基准对我们的算法进行了评估，并得出结论，与简单的方法相比，我们的算法不太容易爆炸，产生的自动机可以小几个数量级，并且整体速度更快。
2019-10-04 cs.FL cs.LO
Control-Flow Residual Analysis for Symbolic Automata
在系统的完全静态分析由于系统大小而无法按比例放大的情况下，动态监视已越来越多地用于确保系统正确性。然而，缺点是运行时开销，这是由附加的监控代码所引起的。为了解决这个问题，在文献中已经提出了各种方法来使用静态分析以减少监视开销。在本文中，我们概括了现有的工作，使用控制流静态分析，以优化指定为自动机的属性，并证明了类似的分析可以应用于更有表现力的符号自动机-使减少监测仪器的系统，也监测逻辑。我们还提出了实证证据，这种方法的有效性，通过分析的影响，在金融交易系统中的监控管理费用。
2017-08-24 cs.LO cs.SE
Verifying Quantum Circuits with Level-Synchronized Tree Automata (Technical Report)
本文提出基于层级同步树自动机的量子电路符号验证方法，将门操作复杂度降至至多二次方，并支持参数化验证，实验表明其可处理规模远超现有工具的问题。
2024-10-24 cs.FL cs.LO
Complementation of Emerson-Lei Automata (Technical Report)
本文提出了基于秩的 Büchi 自动机求补方法修改的 Emerson-Lei 自动机子类求补新构造，包括针对 Inf 接受条件布尔组合的专门构造和广义 Rabin 自动机求补技术，部分类别的上限比现有技术好指数倍。
2024-10-15 cs.FL cs.LO
Approximated Symbolic Computations over Hybrid Automata
University of Trieste（的里雅斯特大学）；University of Udine（乌迪内大学）
本文提出一种基于近似语义的混合自动机框架，整合了上界和下界逼近技术，用于处理噪声、不完全信息和有限精度问题，改进了传统混合自动机的分析方法。
2013-08-24 cs.FL cs.LO cs.SY
On Complementation of Nondeterministic Finite Automata without Full Determinization (Technical Report)
本文研究避免完全确定化的NFA求补替代方法，基于逆幂集构造及两种利用NFA常见结构的新颖构造，实验证明这些方法在多数情况下能生成显著更小的补集。
2025-07-14 cs.FL cs.LO
Z3-Noodler: An Automata-based String Solver (Technical Report)
Z3-Noodler是一个基于自动机的字符串求解器，通过稳定化算法求解带正则约束的单词方程，在众多基准上超越现有求解器，并与其他求解器互补，适合作为求解器组合的候选。
2023-10-17 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
Complementing Emerson-Lei Elevator Automata (Technical Report)
Brno University of Technology（布尔诺理工大学）；Key Laboratory of System Software (Chinese Academy of Sciences), ISCAS（中国科学院系统软件重点实验室）；Slovak University of Technology in Bratislava（布拉迪斯拉发斯洛伐克工业大学）
本文提出 Emerson-Lei 电梯自动机，推广了 Büchi 电梯自动机到更丰富的接受条件，并给出一种补全算法，其渐近复杂度显著优于已知最佳算法，实验表明比 Spot 工具更高效。
2026-06-26 cs.FL cs.LO
A Practical Specification Language for Automatic Quantum Program Verification (Technical Report)
Institute of Information Science, Academia Sinica（中央研究院資訊科学研究所）；Graduate Institute of Electronics Engineering, National Taiwan University（国立台湾大学电子工程学研究所）；Faculty of Information Technology, Brno University of Technology（布尔诺理工大学信息技术学院）
本文提出了一种扩展的集合基规范语言和转换算法，通过控制自动机构造和量子位重排，实现线性复杂度的量子程序自动验证。
2026-05-07 cs.FL cs.LO
Simulations in Rank-Based Büchi Automata Complementation (Technical Report)
Büchi自动机的互补是程序可终止性分析中的一项重要技术。对最佳互补结构的长期探索随着Schewe的工作而达到高潮，他提出了一种最坏情况下的基于最佳秩的程序，该程序生成的互补大小与$(0.76n)^n$的理论下限相匹配，并对$O(n^2)$的多项式因子取模。虽然是最坏情况下的最优，但该过程在许多情况下会产生不必要的大自动机。在本文中，我们提出了几种方法，如何使用直接和延迟的模拟关系，以减少规模的自动机得到的基于秩的互补过程。我们的技术是基于（i）忽略宏状态，不能用于接受一个字的补充或（ii）饱和的宏状态与模拟较小的状态，以减少其总数。我们的实验表明，我们的技术确实可以大大减少互补输出的大小。
2019-10-04 cs.FL cs.LO
The Delay-Insensitivity, the Hazard-Freedom, the Semi-Modularity and the Technical Condition of Good Running of the Discrete Time Asynchronous Automata
本文研究了异步自动机的一些重要性质：延迟不敏感性、冒险自由性、半模块性和良好运行的技术条件。时间是离散的。
2001-10-31 cs.LO
Inferring Symbolic Automata
本文研究了符号有限状态自动机（SFA）在查询学习和极限识别范式下的可学习性，通过提出必要与充分条件，首次得出了负面与正面结果，并重新审视了不同SFA形式下的过程复杂性。
2023-04-19 cs.FL cs.LO
Automata Terms in a Lazy WSkS Decision Procedure (Technical Report)
我们提出了一个懒惰的决策过程的逻辑WSkS。它建立了一个基于术语的符号表示的状态空间的树自动机（TA）构造的经典WSkS决策过程。经典的决策过程通过自底向上的遍历将符号表示转换为TA，然后测试其语言非空性，这对应于公式的可满足性。另一方面，我们从顶部开始评估表示，动态构建状态空间，并利用机会修剪掉与语言空虚测试无关的状态空间部分。为了做到这一点，我们需要将我们前面的逻辑线性片段（所谓的WS1S）过程中使用的语言项（表示语言派生）的概念扩展为自动机项。我们实现了我们的决策过程，并确定了我们的原型实现明显快于Mona工具中实现的经典过程的公式类。
2019-05-21 cs.FL cs.LO
On the Sets of Real Numbers Recognized by Finite Automata in Multiple Bases
本文研究了有限自动机识别位置符号编码的实数集的表达能力。我们考虑Muller自动机以及弱确定性自动机的限制类，在实际应用中用作符号集表示。在以前的工作中，已经建立了弱确定性自动机在两个不共享同一组素因子的基础上可识别的数字集合正是那些在实数和整数的一阶加法理论中可定义的数字。这一结果扩展了Cobham定理，该定理描述了可由多个基中的有限自动机识别的整数集合。在这篇文章中，我们首先将这个结果推广到乘法独立基，这使得它更接近于Cobham定理的原始陈述。然后，我们研究了Muller自动机在两个基上可识别的实数集。我们用一个反例表明，在这种情况下，科巴姆定理并不推广到乘法独立的基础。最后，我们证明了Muller自动机在两个基上可识别的实数集，如果它们不具有相同的素因子集，那么它们就是在实数和整数的一阶加法理论中可定义的实数集.因此，这些集合也可以被弱确定性自动机识别。这一结果导致了一个精确的特征集的实数是可识别的多个基地，并提供了一个理论上的理由使用弱自动机作为符号表示集。
2010-02-24 cs.FL cs.LO
Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic
我们介绍堆自动机，一个形式主义的符号堆碎片的分离逻辑与用户定义的归纳谓词的鲁棒性自动推理。可满足性、可达性和非循环性等鲁棒性属性对于基于分离逻辑的自动程序分析和验证中的各种推理任务都很重要。以前，这样的性质已经出现在分离逻辑文献的许多地方，但没有被系统地研究。在本文中，我们开发了一个基于堆自动机的算法框架，使我们能够以统一的方式获得广泛的鲁棒性的渐近最优决策程序。我们实现了我们的框架的原型，并取得了可喜的成果，所有上述的鲁棒性。此外，我们证明了堆自动机的适用性超出了鲁棒性。我们应用我们的算法框架的模型检验和蕴涵问题的符号堆分离逻辑。
2016-10-22 cs.LO
Modular Mix-and-Match Complementation of Büchi Automata (Technical Report)
不确定Büchi自动机（BA）的可补性是自动机理论中的一个重要问题，在形式化验证中有着广泛的应用，如程序的终止性分析、模型检验以及某些逻辑的判定过程等。我们建立在最近的工作的想法BA确定李等。并提出了一个新的模块化算法BA互补。我们的算法允许结合几个BA互补程序在一起，一个程序的一个子集的BA的强连接组件（SCC）。以这种方式，可以利用特定SCC的结构（例如当它们固有地弱或确定性时）并使用更有效的专用算法，而不管整个BA的结构如何。我们给出了一个一般的框架，部分互补程序可以插入，它的实例化与几个算法。一般来说，该框架可以产生具有Emerson-Lei接受条件的补集，该补集通常可以更紧凑。使用该算法，我们能够建立一个指数更好的新的上限$O(4n)$补充最近推出的电梯自动机类。我们实现了该算法的原型，并进行了一系列全面的实验上的一个大的基准测试，表明我们的框架补充以及最先进的，它可以作为未来的高效BA互补和包含检查算法的基础。
2023-01-05 cs.FL cs.LO
Towards Efficient Matching of Regexes with Backreferences using Register Set Automata (Technical Report)
Brno University of Technology（布尔诺理工大学）；Aalborg University（奥尔堡大学）
本文提出寄存器集自动机（RSA）以提升带有回溯的正则表达式匹配效率，通过转换正则表达式为RSA并分析其时间复杂度，证明了RSA在处理带捕获组和回溯的正则表达式时的高效性。
2026-04-15 cs.FL cs.LO
Model-Free Reinforcement Learning for Symbolic Automata-encoded Objectives
University of Southern California（南加州大学）；AIT Austrian Institute of Technology GmbH（奥地利技术研究院有限公司）
针对强化学习依赖状态奖励易致策略不满足任务目标或不安全的问题，提出用符号自动机编码目标，定义非稀疏势能奖励提升收敛性，且能保证策略满足规范。
2022-02-24 cs.AI cs.LO cs.RO
Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection (Technical Report)
本文研究了硬件加速的网络入侵检测系统（NIDS）中的非确定自动机的近似约简问题。我们定义了一个错误的距离，从原来的一个减少自动机的数据包被错误分类的减少自动机的概率（wrt的概率分布的数据包在网络流量）。我们使用这个概念来设计一个近似的减少过程，实现了很大的规模减少（远远超出了国家的最先进的语言保留技术）与控制和小的错误。我们已经实现了我们的方法，并评估了从Snort，一个流行的NIDS的用例。我们的研究结果提供了实验证据表明，该方法在实践中可以是非常有效的，使NIDS跟随网络速度的快速增长。
2018-02-21 cs.FL cs.LO cs.NI
An Automata-based Framework for Verification and Bug Hunting in Quantum Circuits (Technical Report)
本文提出一种基于树自动机的量子电路验证与Bug搜寻新范式，通过代数表示量子态并实现量子门语义，在大型电路验证和Bug捕获上展现出高度可扩展性，且建立了量子程序验证与自动机理论的联系。
2023-11-23 cs.FL cs.LO
Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic (Technical Report)
本文利用自动机与算术公式间的细粒度对偶，将位向量自动机与代数推理结合，提出以公式导数构造自动机状态并大规模优化的量化线性整数算术求解方法，原型性能媲美甚至超过前沿 SMT 求解器。
2024-05-18 cs.LO
String Solving with Stabilization and Transducers (Technical Report)
Faculty of Information Technology, Brno University of Technology（布尔诺理工大学信息技术学院）；The Technical Faculty of IT and Design, Aalborg University（奥尔堡大学IT与设计技术学院）
本文提出了一种基于自动机的高效方法，用于求解字符串约束，通过稳定化方法改进了Z3-Noodler求解器，以支持由有限状态转录机表示的关系约束。该方法通过减少昂贵的连接消除需求，提高了长度约束的处理效率，并提出了有效的启发式方法，显著提升了求解性能。
2026-05-18 cs.FL cs.LO
Weakly acyclic diagrams: A data structure for infinite-state symbolic verification
针对OBDDs无法处理无限状态系统的局限，提出弱无环图（WADs）这一OBDDs泛化结构，保留其算法优势并支持无限语言表示，可用于多种无限状态系统的符号模型检测。
2025-02-17 cs.DS cs.LO
ATL*AS: An Automata-Theoretic Approach and Tool for the Verification of Strategic Abilities in Multi-Agent Systems
本文提出面向无限迹与有限迹语义的 ATL* 符号化模型检测算法，并在 ATL*AS 工具中实现，实验证明其在可扩展性和效率上优于现有方法。
2025-10-21 cs.LO cs.MA
Decision Procedures for Sequence Theories (Technical Report)
本文研究序列理论的可判定性，证明基于布尔代数字母表和参数自动机可保持可判定性，并开发了序列求解器 SeCo 以验证其有效性。
2023-07-31 cs.LO
Compositional Liveness-Preserving Conformance Testing of Timed I/O Automata -- Technical Report
I/O一致性测试理论（例如，ioco）关注的是正式定义实现的可观察输出行为何时符合规范允许的行为。因此，人们提出了几种ioco的实时扩展，通常称为tioco，进一步考虑了动作之间允许的延迟。在本文中，我们提出了一个改进版的tioco，称为实时ioco（ltioco），解决现有定义的各种弱点。在这里，一个合理的适应静止（即，任何输出的可观察到的不存在）到实时行为的转换必须小心进行：因此，LTIOCO将允许发生的安全输出与强制在特定时间段内发生的实况输出区分开，从而引起静止的两个不同方面。此外，tioco经常被定义在时间I/O标记转换系统（TIOLTS），时间I/O自动机（TIOA）的语义模型，这是无限分支，因此不可行的实际测试工具。相反，我们扩展了理论的区域图，使有限的语义模型TIOA的ltioco测试。最后，我们调查ltioco的组合性与平行组成，包括适当的治疗沉默的过渡。
2019-09-10 cs.FL cs.LO cs.SE
Model Checking Flat Freeze LTL on One-Counter Automata
本文解决了单计数器自动机上平坦冻结线性时序逻辑模型检测的可判定性开放问题，通过归约到带参数化相等性测试的可达性问题并转化为Presburger算术证明其可判定。
2018-12-06 cs.FL cs.LO
Unbounded-Thread Reachability via Symbolic Execution and Loop Acceleration (Technical Report)
我们提出了一种方法，以参数化的可达性通信有限状态线程，制定了一个可满足性问题的分析。除了无限数量的线程之外，基于SAT/SMT的可达性方法的主要挑战是线程执行的程序中存在无限循环。在本文中，我们展示了如何简单的循环可以加速近似Presburger算术约束。这些约束是通过符号执行获得的，如果给定的程序状态是可达的，则这些约束是可满足的。我们总结循环嵌套在其他循环使用递归关系从内部循环的加速。该摘要抽象了循环迭代参数，因此可能过于近似。我们的符号方法的一个优点是，建立Presburger公式的过程可以在任何算术运算之前立即揭示它们的不可满足性。我们证明了这种技术的力量，证明和反驳的安全特性的无限线程程序和其他无限状态转换系统。
2015-05-11 cs.LO
Parameterized Verification of Quantum Circuits (Technical Report)
Uppsala University（乌普萨拉大学）；Mälardalen University（马拉尔登大学）；Brno University of Technology（布尔诺理工大学）；Aalborg University（奥尔堡大学）；National Taipei University of Technology（台北科技大学）
本文提出了一种自动框架用于验证参数化量子电路的输入输出正确性与等价性，采用同步加权树自动机模型并提供决策算法，通过实验展示了框架的高效性与表达力。
2025-12-02 cs.FL cs.LO
Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games
自从Calude，Jain，Khoussainov，Li和Stephan（2017）的突破性结果以来，已经提出了几种不同的技术来设计用于解决奇偶游戏的准多项式算法：游戏摘要，进度测量和注册游戏。我们认为，所有这些技术都可以被视为实例的分离方法来解决平价游戏，其中一个关键的技术组成部分是构建（显式或隐式）的自动机，分离语言的文字编码播放（决定性地）赢得了两个球员。我们的主要技术成果是一个准多项式下界的大小，这样的分离自动机，几乎匹配目前最好的上限。这就形成了一个障碍，所有现有的方法必须克服正在进行的寻求多项式时间算法解决奇偶博弈。我们引入和研究的关键和基本概念是泛序树。技术亮点是泛有序树的大小的准多项式下界和证明每个分离安全自动机有一个泛树隐藏在其状态空间。
2018-11-02 cs.CC cs.FL cs.GT
Time-Darts: A Data Structure for Verification of Closed Timed Automata
符号数据结构在模型检验时系统中的应用已成为一个重要的研究课题，在一些成熟的验证工具中，差分边界矩阵（DBMs）仍然是首选的数据结构。相比之下，离散化提供了一个简单的选择，所有的操作都具有线性时间复杂度的时钟数，但有效的封闭系统的一大类。不幸的是，细粒度的离散化会导致状态空间爆炸。我们引入了一种新的数据结构，称为时间箭头的符号表示的状态空间的时间自动机。与完全离散化相比，单个时间镖允许表示任意大的状态集合，但是时间镖上的操作的时间复杂度在时钟数量上保持线性。我们证明了建议的可达性算法的正确性，并进行了几个实验，以比较性能的时间飞镖和完全离散化。主要结论是，在我们所有的实验中，时间镖方法优于完全离散化，它的规模显着更好的模型与较大的常数。
2012-11-27 cs.DS cs.LO
Verification of Timed Automata Using Rewrite Rules and Strategies
ELAN是一种强大的语言和环境，用于指定和原型化演绎系统，该语言基于由策略控制的重写规则。时间自动机是一类反应式系统的连续实时模型，有效的模型检测算法已经被设计出来。在本文中，我们表明，这些算法可以很容易地在ELAN系统的原型。本文认为，通过这个例子，重写依赖于规则和策略的系统是一个很好的框架，原型，研究和测试，而有效的符号模型检测算法，即算法，涉及组合的图形探索规则，演绎规则，约束求解技术和决策过程。
2009-07-17 cs.LO
Zone-based verification of timed automata: extrapolations, simulations and what next?
时间自动机是由Rajeev Schmidt和David Dill在90年代初提出的。在过去的几十年里，时间自动机已经成为事实上的模型，用于验证实时系统。时间自动机的算法是基于使用区域作为符号表示的状态空间的遍历。由于状态空间是无限的，终止依赖于产生可达状态的有限表示的有限抽象。获得有限抽象的第一个解决方案是基于区域的外推，并已在行业实力工具Uppaal中实现。在过去的十年中，出现了一种基于区域之间模拟的不同方法，并已在完全开源的工具中实现。这种基于模拟的方法已经为时间自动机的可达性和活性带来了新的有效算法，并且还扩展到更丰富的模型，如加权时间自动机和具有对角约束和更新的时间自动机。在这篇文章中，我们调查的外推和模拟技术，并讨论了未来的一些开放的挑战。
2022-07-15 cs.LO
A Symbolic Algorithm for the Case-Split Rule in Solving Word Constraints with Extensions (Technical Report)
案例分割是当前字符串约束理论决策过程中的一个核心证明规则。它的使用是字符串约束求解中状态空间爆炸的主要原因，因为它是在证明树中创建分支的唯一规则。此外，显式处理的情况下分裂规则可能会导致重新计算相同的任务在多个分支的证明树。在本文中，我们提出了一个符号算法，显着减少这样的冗余。特别是，我们将字符串约束编码为正则语言，并将证明规则编码为理性转换器。这允许我们在证明树中只执行一次类似的步骤，从而缓解状态空间爆炸。我们还扩展了编码，以处理字符串约束，长度约束和常规约束的任意布尔组合。在我们的实验结果中，我们验证了我们的技术在许多其他最先进的求解器无法提供答案的实际情况下有效;我们的Python原型实现解决了超过50%的其他工具无法解决的字符串约束。
2023-03-02 cs.LO
Coalgebraic Automata Theory: Basic Results
我们将自动机理论中的一些中心结果推广到余代数的抽象层次，从而奠定了在无限对象上操作的自动机的普遍理论的基础。设F是任何保持弱拉回的集合函子。我们证明了F-余代数的可识别语言类在取联合、交集和投影下是封闭的。我们还证明了，如果一个非确定性的F-自动机接受一些余代数，它接受一个有限的自动机的大小。我们的主要技术成果涉及一个明确的建设，将一个给定的交替F-自动机到一个等价的不确定性，其大小是指数约束的大小的原始自动机。
2008-11-21 cs.LO
An Automaton Learning Approach to Solving Safety Games over Infinite Graphs
University of California at Los Angeles（加州大学洛杉矶分校）；University of Pennsylvania（宾夕法尼亚大学）
我们提出了一种方法来构建有限状态反应控制器的系统，其相互作用与他们的对抗性的环境建模的无限持续时间的两个玩家游戏（可能）无限的图形。所提出的方法的目标是安全游戏无限多个国家或与这样一个大量的国家，这将是不切实际的-如果不是不可能的-传统的合成技术，工作在整个状态空间。我们诉诸于构建有限状态控制器，这样的系统，通过自动机学习方法，利用符号表示的基础游戏，是基于有限自动机。在整个学习过程中，学习者保持对获胜区域的近似（表示为有限自动机），并使用教师提供的不同类型的反例对其进行细化，直到可以导出令人满意的控制器（如果存在）。我们提出了一个符号表示的安全游戏（灵感来自定期模型检验），提出实现的学习者和教师，并评估其性能的例子，在动态环境中的机器人运动规划的动机。
2016-01-07 cs.FL cs.LG cs.LO
Symbolic Models for Stochastic Switched Systems: A Discretization and a Discretization-Free Approach
Technische Universität München（慕尼黑工业大学）；University of Oxford（牛津大学）；Université de Grenoble（格勒诺布尔大学）
本文提出两种符号抽象技术，用于随机切换系统的稳定性分析与控制器合成，通过构造近似等价的符号模型来满足逻辑规范要求。
2014-07-10 cs.LO cs.SY eess.SY
Supervisory Controller Synthesis for Non-terminating Processes is an Obliging Game
本文提出了一种新的算法来解决被建模为$ω$ -正则自动机的非终止过程的监督控制问题。这个问题的解决方案是由Thistle在1995年获得的，它使用了自动机的复杂操作。我们展示了一个新的解决方案，通过减少义务游戏，这反过来，可以减少到$ω$ -定期反应合成的问题。因此，我们的减少结果在一个符号算法的基础上操纵状态集使用的工具反应合成。
2021-08-26 cs.LO cs.SY eess.SY
