エレベータやロボットなどを制御するプログラムをシステム仕様から合成する研究が行われている。システム仕様は時間論理などの形式言語で記述され、この記述から制御プログラムを合成され、状態遷移図などの形式として出力される。また、制御プログラムの合成にはシステムの外部環境をモデル化して、システム仕様と外部環境モデルと合わせて制御プログラムを合成する場合もある。本論文では、外部環境が当初のモデルから変化した場合であっても、システム仕様に含まれる安全性だけは満たすような制御プログラムの合成を目指す。