核心发现
方法论
本文提出一种基于状态分解的直接合成方法，从转移基NBAs中生成ω正则表达式。该方法将NBA拆分为〈起始状态，接受状态〉对的NFAs三元组，分别合成正则表达式后再组合成完整表达式。通过定义Lij, all、Lij, rej和Lij, acc三类语言，确保表达式与NBA识别的语言一致。算法利用状态消除技术，从NFAs中提取正则表达式，避免了传统的状态转换，减少了表达式复杂度。论文证明了该方法的正确性（声称和完备性），并分析了时间复杂度（O(|Q|^5)）和表达式的描述复杂度。
关键结果
- 实验证明，从转移基NBAs合成的ω正则表达式比从状态基NBAs得到的更紧凑，平均缩减超过50%的反波兰记法节点数。特别是在义务、反应性、安全和递归型LTL公式中，紧凑性提升更明显，递归型公式平均缩减达52%。此外，使用转移基NBAs能处理更多的LTL公式，验证了方法的实用性和扩展性。
研究意义
该研究突破了传统从状态基NBAs合成ω正则表达式的局限，提供了更高效、更紧凑的表达方式，极大改善了模型合成和验证的复杂度。对形式验证、模型检测和反应式系统设计具有重要推动作用，特别是在工业规模的复杂系统中，表达式紧凑性直接影响验证效率和可读性。
技术贡献
技术创新在于提出一种直接从转移基NBAs合成ω正则表达式的算法，避免中间状态转换，提升表达式紧凑性和生成效率。结合Lij系列语言定义，确保合成的表达式与原语言等价。算法的正确性由声称和完备性证明支撑，复杂度分析为后续优化提供理论基础。此方法拓宽了模型合成的工具箱，为复杂系统的自动化验证提供新途径。
新颖性
本研究首次提出直接从转移基NBAs合成ω正则表达式的方法，避免了传统的状态转换步骤，显著提升表达式的紧凑性和算法效率。与现有的基于状态的合成方法相比，创新在于利用转移结构的天然优势，结合三类语言的定义，实现更简洁的表达式生成。这一创新为自动化模型合成提供了新的理论和实践基础。
局限性
- 该方法在处理极大规模NBA时，仍存在时间复杂度较高的问题（O(|Q|^5)），对计算资源要求较高。算法依赖于NFAs的状态消除，可能在某些复杂结构中导致表达式膨胀。此外，当前未考虑表达式的简化优化，未来需结合简化策略进一步提升表达式的可读性和简洁性。
未来方向
未来将探索优化算法的时间复杂度，结合表达式简化技术，提升大规模系统的适应性。同时，将研究该方法在不同类型的逻辑公式（如CTL、μ-演算）中的扩展可能性，推动自动化模型合成的广泛应用。还计划结合机器学习技术，自动识别最优拆分策略，进一步提升合成效率和表达式紧凑性。
AI 总览摘要
在反应式系统建模与验证领域，ω-正则语言提供了描述无限行为的强大工具。传统方法多依赖状态基NBAs，合成ω正则表达式时常导致表达式臃肿，影响验证效率。本文提出一种创新算法，直接从转移基NBAs中合成ω正则表达式，避免中间状态转换，显著提升表达式紧凑性。该方法通过定义三类语言（Lij, all、Lij, rej、Lij, acc）确保合成表达式与原始语言等价，并利用状态消除技术实现高效合成。实验证明，转移基NBAs生成的表达式平均比状态基NBAs紧凑超过50%，在义务、反应性和递归型LTL公式中表现尤为优异。这一突破不仅提升了模型验证的效率，也为复杂系统的自动化合成提供了新工具。未来，研究将聚焦算法优化与表达式简化，推动该技术在工业界的广泛应用。该方法的提出，为自动化验证和模型合成开辟了新的路径，具有深远的理论和实践意义。
深度分析
研究背景
反应式系统的行为通常由无限长的执行轨迹描述，ω-正则语言成为表达此类行为的核心工具。早期研究主要依赖状态基NBAs（如Safra构造和Rabin自动机）和正则表达式的转换技术，但这些方法在表达式复杂度和算法效率方面存在瓶颈。近年来，转移基NBAs因其结构天然、算法自然，逐渐成为研究热点。尽管如此，现有合成方法多依赖状态转换，导致表达式冗长，难以应用于大规模系统。理解和改进这一过程，成为形式验证的关键挑战。
核心问题
传统合成ω正则表达式的方法多基于状态转换，将转移基NBAs转化为状态基NBAs，过程复杂且可能引入指数级的状态膨胀，导致表达式不紧凑，验证效率低下。如何直接利用转移结构，保持表达式的简洁性和算法的高效性，成为亟待解决的问题。此问题关系到模型检测的可扩展性和自动化程度，尤其在工业应用中，表达式的紧凑性直接影响验证的可行性。
核心创新
本研究的创新点在于提出一种基于三类语言（Lij, all、Lij, rej、Lij, acc）的直接合成方法，避免了中间状态转换。通过定义NFAs对应的三类语言，结合状态消除技术，能在保持语言等价的前提下，生成更紧凑的ω正则表达式。此方法不仅简化了合成流程，还提升了表达式的紧凑性和算法效率。其理论基础由声称和完备性证明支撑，为未来的模型合成提供了新思路。
方法详解
- �� 将转移基NBA拆分为〈起始状态，接受状态〉对的NFAs三元组。• 定义Lij, all、Lij, rej和Lij, acc三类语言，描述不同转移条件下的轨迹。• 利用状态消除算法，从NFAs中提取正则表达式。• 通过公式将三类语言合成完整的ω正则表达式，确保与原NBA识别的语言一致。• 证明表达式的正确性（声称和完备性），分析时间复杂度（O(|Q|^5)）和表达式的描述复杂度。• 实验验证表达式紧凑性提升，特别在特定LTL模式中表现优异。
实验设计
采用Spot工具生成的转移基和状态基NBAs，基于工业和模式数据集。指标包括反波兰记法节点数、时间长度和星阶，比较两种方法的表达式紧凑性。设定120秒超时限制，未简化和简化两组实验，验证算法在不同场景下的表现。结果显示，转移基NBAs合成的表达式平均缩减超过50%，在递归、义务和反应性公式中效果尤为明显。实验还分析了不同公式类型的表现差异，验证了方法的实用性。
结果分析
实验证明，直接从转移基NBAs合成的ω正则表达式在反波兰记法节点数上平均比状态基NBAs少50%以上。递归、义务和反应性公式的缩减比例超过52%，显著优于传统方法。表达式的紧凑性提升，极大改善了模型验证的可读性和效率。多场景下，方法表现稳定，验证了其广泛适用性和优越性，为工业应用提供了强有力的技术支持。
应用场景
该方法适用于自动化模型验证、反应式系统设计、软件行为分析等场景。只需提供LTL公式，即可快速生成紧凑的ω正则表达式，辅助验证工程师进行模型检测和系统分析。其优势在于提升验证效率、降低表达式复杂度，适合大规模系统的自动化处理。未来还可结合工具链，推广到工业级验证平台，推动智能系统的可靠性提升。
局限与展望
当前算法在极大规模NBA下仍面临高时间复杂度（O(|Q|^5)），计算资源消耗较大。表达式未经过充分简化，可能影响可读性和后续处理。未来需结合表达式优化和简化策略，提升算法的扩展性和实用性。同时，尚未充分考虑不同逻辑扩展（如CTL、μ-演算）对算法的适应性，仍需深入研究。
通俗解读 非专业人士也能看懂
想象你在一家工厂里，工厂每天都要生产各种产品。每个工艺流程都很复杂，有很多步骤和不同的路径。现在，工厂想用一种简单的说明书，告诉工人们怎么快速完成所有流程。传统的方法就像是把每个步骤都写在一张大表里，太长太复杂，不方便记忆。本文提出的方法，就像是用一套简洁的符号和规则，直接描述所有可能的路径，省去了繁琐的中间步骤。这样，工人们可以更快理解流程，也能更容易发现问题。这个新方法让整个工厂的操作变得更高效、更清晰，就像用简洁的说明书让工人们更好地工作一样。
简单解释 像给14岁少年讲一样
想象你在玩一个超级复杂的游戏，每次你要告诉朋友你赢了还是输了，通常要写一长串的故事。可是，如果你能用一句话总结，比如“我赢了，因为我收集了所有宝藏”，是不是就简单多了？这篇论文就像是发明了一种神奇的“总结方法”，可以用一句话把复杂的游戏过程描述清楚。以前，人们总是把游戏的每一步都写下来，太长太难懂。而这个新方法直接从游戏的“规则”出发，用一种特别的符号，把所有可能的玩法都压缩成一句话。这样，不仅节省了时间，还能让别人一眼看出你赢的秘诀。就像用简洁的语言讲故事，让所有人都听得懂一样，这个方法让复杂的系统变得简单明了。
原文摘要
A popular method for modelling reactive systems is to use $ω$-regular languages. These languages can be represented as nondeterministic Büchi automata (NBAs) or $ω$-regular expressions. Existing methods synthesise expressions from state-based NBAs. Synthesis from transition-based NBAs is traditionally done by transforming transition-based NBAs into state-based NBAs. This transformation, however, can increase the complexity of the synthesised expressions. This paper proposes a novel method for directly synthesising $ω$-regular expressions from transition-based NBAs. We prove that the method is sound and complete. Our empirical results show that the $ω$-regular expressions synthesised from transition-based NBAs are more compact than those synthesised from state-based NBAs. This is particularly the case for NBAs computed from obligation, reactivity, safety and recurrence-type LTL formulas, reporting in the latter case an average reduction of over 50%. We also show that our method successfully synthesises $ω$-regular expressions from more LTL formulas when using a transition-based instead of a state-based NBA.