用机器学习提升自动机理论LTL合成效率，击败老牌工具Strix。
SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning
- 引入语义标签和机器学习构建搜索引导器，优化帕提游戏探索
- 在SYNTCOMP上解决更多实例，大样本下速度显著更快
- 首次证明机器学习辅助方法可超越顶尖传统工具
从线性时序逻辑（LTL）规范中合成反应式系统是经典问题，广泛应用于安全关键系统设计。我们提出工具SemML，赢得今年SYNTCOMP的LTL可实现性赛道冠军，终结了Strix多年垄断。尽管两者均基于自动机理论方法，但SemML依赖两项核心技术：(i) 语义标签——来自最新LTL到自动机转换的逻辑附加信息，用于装饰帕提游戏；(ii) 机器学习方法将该信息转化为在线探索帕提游戏的引导决策器（故名SemML）。本工具填补了先前使用此类引导器的空白，提供高效实现及额外算法优化。我们在SYNTCOMP全集与合成数据集上评估SemML，与Strix对比并分析优劣。结果表明，SemML在更大规模实例上显著更快，并解决更多问题，首次证实机器学习辅助方法可在真实LTL合成任务中超越当前最先进工具。
原文摘要 · Abstract (English)
Synthesizing a reactive system from specifications given in linear temporal logic (LTL) is a classical problem, finding its applications in safety-critical systems design. We present our tool SemML, which won this year's LTL realizability tracks of SYNTCOMP, after years of domination by Strix. While both tools are based on the automata-theoretic approach, ours relies heavily on (i) Semantic labelling, additional information of logical nature, coming from recent LTL-to-automata translations and decorating the resulting parity game, and (ii) Machine Learning approaches turning this information into a guidance oracle for on-the-fly exploration of the parity game (whence the name SemML). Our tool fills the missing gaps of previous suggestions to use such an oracle and provides an efficeint implementation with additional algorithmic improvements. We evaluate SemML both on the entire set of SYNTCOMP as well as a synthetic data set, compare it to Strix, and analyze the advantages and limitations. As SemML solves more instances on SYNTCOMP and does so significantly faster on larger instances, this demonstrates for the first time that machine-learning-aided approaches can out-perform state-of-the-art tools in real LTL synthesis.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。