2024-03-29T09:52:19Zhttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_oaipmhoai:ipsj.ixsq.nii.ac.jp:000121932022-10-21T05:24:51Z00581:00690:00694
データ付時間オートマトンの双模倣等価性の記号的検証法Symbolic Verification of Bisimulation Equivalence for Timed Automata with Data Valuesjpn論文http://id.nii.ac.jp/1001/00012193/Journal Articlehttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_action_common_download&item_id=12193&item_no=1&attribute_id=1&file_no=1Copyright (c) 2000 by the Information Processing Society of Japan基礎理論大阪大学大学院基礎工学研究科情報数理系専攻北陸先端科学技術大学院大学情報科学研究科大阪大学大学院基礎工学研究科情報数理系専攻大阪大学大学院基礎工学研究科情報数理系専攻中田, 明夫服部, 哲東野, 輝夫谷口, 健一本論文では,時間制約と入出力データに関する条件判定が同時に記述できるオートマトンモデル,データ付時間オートマトンの双模倣等価性の記号的検証法を提案する.データ付時間オートマトンの各状態はいくつかの変数を持ち,その値が遷移条件を満足するような遷移を実行する.遷移は入出力遷移と時間遷移の2種類があり,入力遷移は入力値を変数に代入し,出力遷移は与えられた式の値を出力し,時間遷移は経過時間を変数に代入したのち次の状態へ遷移する.各状態は時間遷移しかできない休止状態と入出力遷移しかできない活動状態に分類され,休止状態からは活動状態へ,活動状態からは休止状態へ遷移する.提案する手法は,Hennessyら(1995)が提案した,入出力遷移のみを記述できる同種のモデルに対する双模倣等価性の記号的検証法の拡張であり,データ付時間オートマトンの任意の状態対に対して,それらが双模倣等価となるための変数に関する条件を自動導出する.In this paper, we propose a timed I/O automaton model and itsverification method of bisimulation equivalence.In a timed I/O automaton model, a set of variables is assigned to each state, andeach transition can be executed if its transition condition is satisfiedby 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 cansubstitute the input value into a variable. A time transition may have avariable, to which the amount of the delay fromthe execution time of the previous 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 executed.The proposed verification method is an extension of the method (Hennessy, et al., 1995).It derives the weakest condition for the variables to makegiven two states of timed I/O automata bisimilar.AN00116647情報処理学会論文誌419248724972000-09-151882-77642009-06-29