10日間大学時代の気分に戻ってLTLで仕様を書いてみた - cloverrose's blog会社のイベントで1週間何しててもいい期間があったので、大学時代に研究していた形式手法の1分野であるLTL仕様からオートマトン合成の分野に触れていました。 タイムライン 以前使っていたAcacia+というツールがリンク切れになっていたことに驚く LTLからオートマトン合成のコンペティションが2014年から開催されており使いやすく高性能なLTL合成ツールの発展に貢献していた TLSFという生のLTLをラップした仕様形式がベンチマークの共通形式として普及していた。入出力のシグナルとオプションがLTLとセットで管理できる。 Strixというツールが2019年のコンペで1位になっていたのでOnlineでもページで遊んでみる Strixが良さそうなのでDockerfile作ってインストールして触ってみる Strixの内部でowlというLTLパースとωオートマトン変換をやるJavaライブラリ使っていて、
