実時間システムのパラメータ制約自動導出およびITSへの応用

スポンサーリンク

概要

論文の詳細を見る
本論文では、あるクラスの時間オートマトンモデルで記述された実時間システムが与えられた時相論理式で書かれた性質を満足するために必要十分な時間パラメータに関する制約を自動導出する手法[5]を道路交通に関する例題に適用し、その有効性を評価する。[5]で提案したモデルはAlurらが提案した時間オートマトンモデルと異なり、ある状態からある状態への到達可能であるためのパラメータに関する条件を遷移条件の論理積で表現できるという特徴を持つ。満たすべき性質は時相論理式の一種であるTCTLで記述する。TCTLによってある時間以内にある動作ができる状態に到達可能であるなどといった性質を記述できる。例題として、信号付き交差点を車がある時間以内に通過するための車の速度(実際には、車が道路のある領域を通過するのにかかる時間)と信号が変わるタイミングに関する制約を導出する。
一般社団法人情報処理学会の論文
2000-05-24

著者

関連論文

もっと見る

スポンサーリンク