13:40 〜 14:00
[2E3-OS-13b-02] 差分制約を含んだ時間オートマトンモデルの LMNtal による状態空間構築
キーワード：LMNtal、リアルタイムシステム、時間オートマトン、状態遷移系、Difference Bound Matrices
システムの挙動に実時間制約をもつようなシステムをリアルタイムシステムといい, 時間オートマトンはリアルタイムシステムの代表的なモデリング手法の一つである. 通常, 時間は連続値をとることから, 検証を行うにあたっては状態空間の適切な抽象化を行い, 状態数の発散を抑える必要がある.
本研究の目的は, リアルタイムシステムを簡潔にモデリングすること, また, 適切に抽象化を行い状態数を削減した状態空間を構築することである. モデリングにあたっては, 多重集合の表現やプロセスの階層化が容易な言語 LMNtal を用い, 時間オートマトンモデルのフレームワークを考案した. 状態空間構築についても LMNtal を用いて実装し, 時間を制約式の積として管理することで状態数を大幅に削減することができた. また, 変数どうしの差分制約を含んだモデルを扱うため, 効率的な制約処理ができるデータ構造として知られる Difference Bound Matrices を LMNtal で実装した.
本研究の目的は, リアルタイムシステムを簡潔にモデリングすること, また, 適切に抽象化を行い状態数を削減した状態空間を構築することである. モデリングにあたっては, 多重集合の表現やプロセスの階層化が容易な言語 LMNtal を用い, 時間オートマトンモデルのフレームワークを考案した. 状態空間構築についても LMNtal を用いて実装し, 時間を制約式の積として管理することで状態数を大幅に削減することができた. また, 変数どうしの差分制約を含んだモデルを扱うため, 効率的な制約処理ができるデータ構造として知られる Difference Bound Matrices を LMNtal で実装した.
講演PDFパスワード認証
論文PDFの閲覧にはログインが必要です。参加登録者の方は「参加者用ログイン」画面からログインしてください。あるいは論文PDF閲覧用のパスワードを以下にご入力ください。