文献

J-GLOBAL ID：201302279557715443   整理番号：13A0291606

自律最大プラス線形系の抽象化および検証

Abstraction and Verification of Autonomous Max-Plus-Linear Systems

著者 (3件)： ADZKIYA Dieky (Delft Univ. Technol., NLD) ,  DE SCHUTTER Bart (Delft Univ. Technol., NLD) ,  ABATE Alessandro (Delft Univ. Technol., NLD)
資料名： Proceedings of the American Control Conference  (Proceedings of the American Control Conference)
巻： 2012 Vol.1  ページ： 721-726  発行年： 2012年 
JST資料番号： B0982A  ISSN： 0743-1619  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 最大+線形(MPL)系は,内在する離散事象のタイミングを特性化する連続状態空間による離散事象モデルである。本論文では,自律MPLモデルの有限状態抽象化に基づく新しいアプローチを,様相論理における仕様としての一般動的特性の表現において,モデルチェックによるこの特性の形式的検証において調べた。抽象化手順に関して,有限状態標識付過渡システム(LTS)を生成する新しい技術を提示した。LTSの頂点を,MPLの状態空間の有限分割により得,2つのLTS状態間の関係を,オリジナルのMPLモデルの軌道が対応する分割領域間で遷移できるかをチェックすることにより定義した。LTSモデルの標識を,オリジナルモデルの2変数に対する事象のタイミング間の差を特性化するか,あるいはMPLモデルの連続事象間の時間差を表現するかにより定義した。事例研究において抽象化手順の計算性能のベンチマークを検査した。

シソーラス用語： *線形系 ,  抽象 ,  離散系 ,  *様相論理 ,  モデル検査 ,  検証 ,  *標識法 ,  分割 ,  現象
準シソーラス用語： 形式的検証 ,  事象 ,  自律 ,  *状態空間 ,  抽象化

分類 (1件)： システム・制御理論一般  (IA02010H)

タイトルに関連する用語 (4件)： 自律 ,  線形系 ,  抽象化 ,  検証