[2N5-OS-17b] AIと制約プログラミング (2)

[2N5-OS-17b-04] 制約に基づくハイブリッドシステムモデリング言語HydLaの宣言的意味論の拡張

〇山田 悠之介¹、上田 和紀² (1. 早稲田大学大学院基幹理工学研究科情報理工・情報通信専攻、2. 早稲田大学理工学術院情報理工学科)

キーワード：制約プログラミング、ハイブリッドシステム、プログラム意味論、フレーム公理

ハイブリッドシステムは時間の経過に伴って変数が連続変化と離散変化を起こす動的システムである。ハイブリッドシステムのモデリング手法としてはハイブリッドオートマトンによるものが最もよく知られている。一方でハイブリッドシステムの宣言的でより簡潔な記述方法は未だにチャレンジングな問題である。
HydLaは制約ベースのハイブリッドシステムモデリング言語である。HydLaプログラムではシステムを宣言的に記述し、宣言的意味論によって得られる解集合でモデルを表現する。既存の意味論は簡潔かつ直感的であり、行儀の良いHydLaプログラムを考えるための十分な表現力を持っている。一方で、プログラム変換や操作的意味論との比較などのHydLaの意味論の応用を考える上ではより強力な意味論が必要となる。本論文では連続性に関するフレーム公理の表現について、既存の宣言的意味論を厳密化・拡張し、各改良点が必要であることを具体例を通して説明する。