時間制約と入出力データに関する条件判定が同時に記述できるオートマトンモデルとその双模倣等価性検証法

• Item type: Symposium(1)
• 公開日: 1999-12-01
• タイトル: 時間制約と入出力データに関する条件判定が同時に記述できるオートマトンモデルとその双模倣等価性検証法
• タイトル / 言語: en
• タイトル: Timed Automata with Data Values and their Verification of Bisimulation Equivalence
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_5794
• 資源タイプ: conference paper
• 著者所属: 広島市立大学情報科学部情報数理学科
• 著者所属: 奈良先端科学技術大学院大学情報科学研究科
• 著者所属: 大阪大学大学院基礎工学研究科情報数理系専攻
• 著者所属: 大阪大学大学院基礎工学研究科情報数理系専攻
• 著者所属(英): en
• 著者所属(英): Dept. of Compuer Science，Faculty of Information Sciences，Hiroshima City University
• 著者所属(英): en
• 著者所属(英): Graduate School of Information Science，Nara Institute of Science and Technology
• 著者所属(英): en
• 著者所属(英): Dept. of Informatics and Mathematical Science，Graduate School of Engineering Science，Osaka University
• 著者所属(英): en
• 著者所属(英): Dept. of Informatics and Mathematical Science，Graduate School of Engineering Science，Osaka University
• 著者名: 中田, 明夫; 服部, 哲; 東野, 輝夫; 谷口, 健一
• 著者名(英): Akio, Nakata; Satoshi, Hattori; Teruo, Higashino; Kenichi, Taniguchi
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本論文では，時間制約と入出力データに関する条件判定が同時に記述できるオートマトンモデル，データ付時間オートマトンの双模倣等価性の記号的検証法を提案する.データ付時間オートマトンの各状態はいくつかの変数を持ち，その値が遷移条件を満足するような遷移を実行する.選移は入出力選移と時間選移の2種類があり，入力遷移は入力値を変数に代入し，出力遷移は与えられた式の値を出力し，時間遷移は経過時間を変数に代入したのち次の状態へ遷移する.各状態は時間遷移しかできない休止状態と入出力遷移しかできない活動状態に分類され，休止状態からは活動状態へ，活動状態からは休止状態へ遷移する.提案する手法は，文献[3]で提案された，入出力選移のみを記述できる同種のモデルに対する双模倣等価性の記号的検証法の拡張であり，データ付時間オートマトンの任意の状態対に対して，それらが双模倣等価となるための変数に関する条件を自動導出する.
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: In this paper，we propose a timed I/O automaton model and its verification method of bisimulation equivalence. In a timed I/O automaton model，a set of variables is assigned to each state，and each transition can be executed if its transition condition is satisfied by the current values of the variables. There are two kinds of transition，one is an I/O transition and the other is a time transition. An input transition can substitute the input value into a variable. A time transition may have a variable，to which the amount of the delay from the execution time of the privious I/O action is assigned. All states are divided into either idle states or active states. In an idle state，only a time transition can be executed，whereas in an active state，some I/O transitions can be execued. The proposed verification method is an extension of Ref. [3]. It derives the weakest condition for the variables to make given two states of timed I/O automata bisimilar.
• 書誌情報: マルチメディア通信と分散処理ワークショップ論文集; 巻 1999, 号 18, p. 37-42, 発行日 1999-12-01
• 出版者 / 言語: ja
• 出版者: 情報処理学会