データ付時間オートマトンの双模倣等価性の記号的検証法

• Item type: SIG Technical Reports(1)
• 公開日: 1998-06-03
• タイトル: データ付時間オートマトンの双模倣等価性の記号的検証法
• タイトル / 言語: en
• タイトル: Symbolic Verification of Bisimulation Equivalence for Timed Automata with Data Values
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 大阪大学大学院基礎工学研究科情報数理系
• 著者所属: 大阪大学大学院基礎工学研究科情報数理系
• 著者所属: 広島市立大学情報科学部ソフトウェア工学講座
• 著者所属: 大阪大学大学院基礎工学研究科情報数理系
• 著者所属: 大阪大学大学院基礎工学研究科情報数理系
• 著者所属(英): en
• 著者所属(英): Dept. Information and Computer Sciences, Faculty of Engineering Science, Osaka University
• 著者所属(英): en
• 著者所属(英): Dept. Information and Computer Sciences, Faculty of Engineering Science, Osaka University
• 著者所属(英): en
• 著者所属(英): Dept. of Computer Science, Faculty of Information Sciences, Hiroshima City University
• 著者所属(英): en
• 著者所属(英): Dept. Information and Computer Sciences, Faculty of Engineering Science, Osaka University
• 著者所属(英): en
• 著者所属(英): Dept. Information and Computer Sciences, Faculty of Engineering Science, Osaka University
• 著者名: 新田, 直子; 山口, 弘純; 中田, 明夫; 東野, 輝夫; 谷口, 健一
• 著者名(英): Naoko, Nitsuta; Hirozumi, Yamaguchi; Akio, Nakata; Teruo, Higashino; Kenichi, Taniguchi
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本稿ではM.Hennessyらが提案したデータ付きプロセスの双模倣等価性の記号的検証法と，我々が提案した時間プロセスの双模倣等価性の記号的検証法を組み合わせて，データと時間に関する制約を両方記述できるような一つのプロセスモデル（データ付時間オートマトンと呼ぶ）上での双模倣等価性の記号的検証法を提案する．データ付時間オートマトンの双模倣等価性を検証する際に，動作に入出力値などのデータや時間に関する制約が付けられていると，意味モデル上では無限個の遷移を生成してしまう．そこで遷移先が同じであるような動作群を一つの遷移にまとめ，もとの無限グラフを有限グラフに変換して検証する．双模倣等価性t〓^buは，プール式bを満たすようなデータ値や時間値の組に対してのみ，状態tとuは双模倣等価であることを表す．本研究では与えられた2つの状態tとuに対してt〓^buを満たすような最も弱いプール式mgb(t u)を求めるアルゴリズムを示す．本手法の適用例として，マルチメディア通信用多重化プロトコルの遷移条件の変更に際して非時間的双模倣等価性が保たれるかどうかを検証した．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: In this paper, we propose a symbolic verification method to verify bisimulation equivalence of two timed automata with data values by combining M. Hennessy's method to verify bisimulation equivalence of two data-passing processes and proposed method to verify bisimulation equivalence of two timed processes. We use the timed automata with data values to describe data-passing timed processes. In general, it costs infinitely to verify bisimulation equivalence of two timed automata with data values, if the range of data values and/or time domain is infinite. Therefore, we classify the infinite number of transitions from a state into the finite number of groups, each of which moves the same state. We use t 〓^b u to express that t is bisimulation equivalent to u for any interpretation which satisfies b. In this paper, we propose an algorithm which obtains the weakest condition mgb(t,u) such that t〓^<mgb(t,u)> u holds for a given state-pair t and u. Using the proposed method, we can verify timed and untimed bisimulation equivalence for timed automata with data values. A practical example is also given.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10116224
• 書誌情報: 情報処理学会研究報告マルチメディア通信と分散処理（DPS）; 巻 1998, 号 55(1998-DPS-089), p. 19-24, 発行日 1998-06-03
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会