SemML 2.0：合成 LTL 控制器
人工智能
2026-04-28 v1 形式语言与自动机理论
计算机科学中的逻辑
摘要
从线性时序逻辑（LTL）规范合成响应系统是经典问题，广泛应用于安全关键系统设计。这些系统通常表示为 Mealy 机或 AIGER 电路。我们提出了 SemML 的第二个版本，性能超过所有现有工具，无论是寻找解还是寻找解。除了实现经典的自动机论方法外，我们工具利用部分探索和机器学习引导高效获取解决方案，并通过大量经验法则和经典算法的改进来提取小型表示。我们在综合竞赛 SYNTCOMP 的数据集上评估了我们的工具，特别是与 Strix、LtlSynt 和 SemML 前一版本进行比较。我们表明，我们比其他工具解决了更多实例，速度也更快，同时保持了最佳的解决方案质量。
引用
@article{arxiv.2604.24102,
title = {SemML 2.0: Synthesizing Controllers for LTL},
author = {Jan Křetínský and Tobias Meggendorfer and Maximilian Prokop},
journal= {arXiv preprint arXiv:2604.24102},
year = {2026}
}