基于转换的接受算法在ω-正则表达式合成中的应用

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

反应系统建模使用ω-正则语言，现有方法需将状态接受NBA转换为过渡接受NBA再合成，本文提出直接合成法，通过分解NBA为三元组处理过渡接受，证明正确性并分析复杂度，实验显示该方法减少后缀大小4.1倍和循环性1.5倍。

　　

摘要人工智能摘要

要查看此由人工智能生成的摘要，您必须具有高级访问权限。

了解更多登录

摘要

摘要

与环境保持持续交互的反应式系统通常使用$\omega$正则语言进行建模。这些语言通过无限长度的执行轨迹来描述系统行为，并表示为非确定性Büchi自动机（NBAs）或$\omega$正则表达式。现有的从NBAs合成表达式的方法仅处理基于状态的接受。这一限制迫使在合成之前将紧凑的基于转换的NBAs转换为更大的基于状态的NBAs。本文介绍了第一种直接从基于转换的NBAs合成$\omega$正则表达式的方法，从而消除了这种转换的需要。该方法通过将NBA分解为非确定性有限自动机的三元组来工作，同时包含了现有的基于对的分解方法以处理基于转换的接受。我们证明了我们的分解是正确的，从而确立了该方法的有效性和完整性。我们讨论了该方法的时间复杂度和描述复杂度。我们在185个线性时态逻辑公式上的实证评估支持了我们的假设：基于转换的合成将后缀大小减少了$4.1$（对于递归属性）和$1.5$（对于反应性属性）。我们还分析了决定基于转换的NBA何时会产生更紧凑表达式的结构因素，并将其发展为一个简单的标准，当应用该标准时，得到的表达式至少与直接基于状态的合成得到的表达式一样紧凑。

人工智能摘要

人工智能生成的摘要（实验性）

此摘要是使用自动化工具生成的，并非由文章作者编写或审核。它旨在帮助发现、帮助读者评估相关性，并协助来自相关研究领域的读者理解该工作。它旨在补充作者提供的摘要，后者仍然是论文的主要摘要。完整文章仍然是权威版本。点击此处了解更多。

点击此处对摘要的准确性、清晰度和实用性进行评论。这样做将有助于改进和未来生成的版本。

要查看此由人工智能生成的简单语言摘要，您必须具有高级访问权限。