SemML 2.0：LTLのためのコントローラ合成

概要: 線形時相論理（LTL）で与えられた仕様から反応的システムを合成することは、古典的な問題であり、安全性が重要なシステム設計における応用が見出されています。これらのシステムは通常、Mealy機械またはAIGER回路のいずれかを用いて表現されます。本稿では、いずれの解を見つけるにおいても、最先端のすべてのツールに対して優れた性能を示すSemMLの第2版を提示します。我々のツールは、古典的なオートマトン理論に基づくアプローチを実装することに加えて、効率的に解を得るための部分探索と機械学習による誘導を利用し、さらに、それらの解の小さな表現を抽出するための古典的アルゴリズムに対する多数のヒューリスティックと改良も備えています。我々は、合成競技SYNTCOMPのデータセットにおいて、既存の最先端ツール（特にStrix、LtlSynt、ならびにSemMLの前バージョン）に対して本ツールを評価します。我々は、解の品質を最先端の水準に保ちながら、他のツールよりも有意に多くのインスタンスを解決し、かつはるかに高速に行えることを示します。