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

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

反应系统通常通过ω-正则语言建模，常用非确定状态机（NBA）或ω-正则表达式表示。现有方法因仅处理状态接受模型，需将过渡式NBA转换为状态式NBA再合成，效率受限。本文提出首个直接从过渡式NBA生成ω-正则表达式的方法，消除转换步骤，并证明其正确性，分析时间复杂性和表达紧凑性。

　　

摘要AI 摘要

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

了解更多登录

摘要

摘要

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

AI 摘要

AI 生成的摘要（实验性）

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

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

要查看此由 AI 生成的纯文本摘要，您必须具有高级访问权限。