arXiv:2501.17496v2 通告类型: 替换 摘要：从线性时序逻辑（LTL）规范中合成反应系统是一个经典问题，其应用范围涵盖了安全关键系统的设计。我们介绍了我们的工具SemML，该工具在今年SYNTCOMP的LTL实现轨道中获胜，而在之前的几年中，Strix一直占据主导地位。虽然这两种工具都基于自动机理论的方法，但我们的工具依赖于（i）语义标签，这种逻辑性质的附加信息来源于最近的LTL到自动机的翻译，并装饰了生成的帕里游戏；以及（ii）机器学习方法，将其转换为一种引导或acles，用于即兴探索帕里游戏（因此命名为SemML）。我们的工具填补了之前关于使用这种或acles的建议中的缺失空白，并提供了一个高效的实现，还包括额外的算法改进。我们分别在SYNTCOMP的整个数据集和一个合成数据集上评估了SemML，将其与Strix进行了比较，并分析了其优势和限制。由于SemML在SYNTCOMP中解决了更多的实例，并且在处理更大实例时显著更快，这表明机器学习辅助的方法首次在实际LTL合成中可超越最先进的工具。