基于转换的ω正则表达式综合的接受方法

《Formal Aspects of Computing》：Transition?Based Acceptance for ω?Regular Expression Synthesis

　　

摘要AI总结

要查看此AI生成的总结，您需要拥有高级访问权限。

了解更多登录

摘要

摘要

那些需要与环境持续交互的反应式系统，通常用$\omega$正则语言来建模。这类语言通过无限长度的执行轨迹来描述系统行为，可表示为非确定性Büchi自动机或$\omega$正则表达式。目前从非确定性Büchi自动机生成表达式的方法仅支持基于状态的接受方式。这一限制使得在合成之前必须将结构紧凑的基于转换的非确定性Büchi自动机转换为规模更大的基于状态的自动机。本文首次提出了直接从基于转换的非确定性Büchi自动机生成$\omega$正则表达式的方法，从而无需进行此类转换。该方法通过将非确定性Büchi自动机分解为非确定性有限自动机的三元组来实现，同时整合了现有的基于二元组的分解方式以处理基于转换的接受逻辑。我们证明了这种分解的正确性，从而确保了方法的可靠性与完整性。此外，我们还分析了该方法的时间复杂度与描述复杂度。通过对185个线性时序逻辑公式的实证测试，我们的假设得到了验证：基于转换的合成方法可使后缀大小分别减少$4.1\times$和$1.5\times$，对应于递归性与反应性特征。我们还分析了决定基于转换的非确定性Büchi自动机何时能产生更紧凑表达式的结构因素，并将其转化为一个简单标准，应用该标准后得到的表达式至少与直接基于状态合成得到的表达式一样紧凑。

AI总结

AI生成的总结（实验性）

此总结是使用自动化工具生成的，未经文章作者撰写或审核。它旨在帮助读者发现相关内容、评估文章相关性，以及帮助来自相关研究领域的读者理解本文内容。它是对作者提供的摘要的补充，而作者提供的摘要仍是文章的核心总结。完整文章才是最具权威性的版本。点击此处了解更多。

点击此处，可以对此总结的准确性、清晰度及实用性发表意见。您的反馈将有助于进一步优化未来的生成版本。

要查看此AI生成的通俗语言总结，您需要拥有高级访问权限。