Abstract
信号時相論理（Signal Temporal Logic; STL）はサイバーフィジカルシステムに対する、時間制約のある安全性重視のタスクを指定するために広く用いられていますが、非専門のユーザがSTLの式を直接記述するのは困難です。自然言語（NL）は便利なインタフェースを提供しますが、その内在する構造的曖昧性のために、STLへの一対一の翻訳は信頼できません。本論文では、NLのタスク記述をSTLの候補式へ変換するための、 extit{曖昧性を保持する}手法を提案します。要点は、構文解析段階で単一の解釈を無理に押し付けるのではなく、複数のもっともらしい構文解析を保持することです。これを実現するために、Combinatory Categorial Grammar（CCG）に基づく3段階のパイプラインを開発します。すなわち、曖昧性を保持するn-best構文解析、STL向けのテンプレートベース意味合成、そしてスコア集約による正準化です。提案手法は、もっともらしさ（plausibility）のスコアを付与した重複排除済みのSTL候補集合を出力し、曖昧な指示に対する複数の可能な形式的解釈を明示的に表現します。既存の、1-bestのNLから論理への翻訳手法とは対照的に、本アプローチはアタッチメント（結合）とスコープの曖昧性を保持することを目的としています。代表的なタスク記述に関するケーススタディでは、本手法が、真に曖昧な入力に対しては複数のSTL候補を生成し、一方で曖昧でない、または正準化されて同等な導出は単一のSTL式へと畳み込むことを示します。
