イベント間の時間制約を論理式で記述できるラベル付き遷移システムとその双模倣等価性検証
スポンサーリンク
概要
- 論文の詳細を見る
時間制約が指定された通信プロセスに対する双模倣等価性の判定は,時間性に起因する状態爆発により一般には困難である.時間性に関しては,文献[4,2,1]などに状態爆発を回避する等価性判定法の提案がある. しかし,それらの提案ではいずれも時間制約としては限られたクラスの記述しか出来ない.一方,最近,データ受渡しを記述できるプロセスモデルに関して,データの具体的な値を考えずに値が満たす条件式を用いて等価性を判定する方法が[3]で提案された.この手法は, (1)判定コストがデータの領域や具体値に依存しない,(2)データに依存する動作の遷移条件を記述する言語として任意の決定可能な論理式の体系を採ってよい,という利点をもつ.時間性を考慮したプロセスの等価性判定にも同様の利点を持った判定法があることが望ましい.本稿では,時間制約が記述可能な一つのプロセスモデルを提案し,そのモデルで記述されたプロセスに対して,上記のような手法によって状態爆発を回避して双模倣等価性を判定する方法を提案する.まず,時間制約を記述するモデルとして,交替性Timed Symbolic Labelled Transition System(以下交替性TSLTSと略す)を導入する.交替性TSLTSの各状態は幾つかのパラメータ変数(例えばx, y)を持ち,各遷移には,例えば,x+5秒間からy秒間待つ,待った時間がy-3秒以内なら動作αを実行し,さもなければ動作bを実行する,などといった条件を変数を用いて記述できる.提案する方法では,文献[3]と同様のアルゴリズムによって,交替性TSLTSモデルで記述されたプロセスの2状態に対して,それらを時間的双模倣等価にするような最弱の条件式(most general boolean,以下mgb[3]と呼ぶ)を求める.
- 一般社団法人情報処理学会の論文
- 1996-09-04
著者
-
東野 輝夫
大阪大学 大学院情報科学研究科
-
谷口 健一
大阪大学 基礎工学部
-
東野 輝夫
大阪大学大学院情報科学研究科|独立行政法人科学技術振興機構 Crest
-
中田 明夫
大阪大学 基礎工学部 情報工学科
関連論文
- 災害現場でセンシングされた生体情報を集約する無線センサーネットワークの構成法(モバイルコンピューティング、モバイルアプリケーション、ユビキタス通信、モバイルマルチメディア通信)
- ネットワークオンチップにおける回路面積と配線コストを考慮したチップ内通信構造最適化の一手法(コンピュータシステムの設計・検証及び一般,デザインガイア2007-VLSI設計の新しい大地を考える研究会)
- アドホック通信に基づく行先経路の道路情報取得プロトコルの開発(セッション2,ITS情報処理・一般)
- アドホック通信に基づく行先経路の道路情報取得プロトコルの開発(セッション2)(ITS情報処理・一般)
- 詳細度の異なるモデルを用いた無線シミュレーションの高速化手法の提案(Work in Progress,ワイヤレス環境でのアプリケーション品質,P2P/アドホックネットワーク,画像符号化,ストリーム技術,信頼性,一般)
- 無線メッシュネットワークにおけるWDSクラスタ分割アルゴリズムの改善(無線ネットワーク)
- 災害医療支援ネットワークのための軽傷者用負傷者端末(システム設計,物理設計及び一般)
- 位置情報に基づくTDMプロトコルの提案(セッション1)
- 車車間通信を利用した信号機制御手法の提案
- 車車間通信を用いた危険車両の検出手法の提案(車車間通信技術,次世代社会基盤をもたらす高度交通システムとモバイル通信システム)
- メッセージフェリーと車車間通信を併用した渋滞情報収集システムの情報伝播効率の改善(車車間通信技術,次世代社会基盤をもたらす高度交通システムとモバイル通信システム)
- データ付時間オートマトンの双模倣等価性の記号的検証法
- MANETを用いた災害時における被災者の位置情報収集・追跡システムの提案(交通における計測・一般(電気系3学会ITS合同研究会))
- MANETを用いた災害時における被災者の位置情報収集・追跡システムの提案(交通における計測, 一般(電気系3学会ITS合同研究会))
- 1J-4 センサーネットワークの設計開発を支援するシミュレーション融合型テストベットの検討(情報爆発時代における情報提示・センサネット・P2P,一般セッション,「情報爆発」時代に向けた新しいIT基盤技術)
- アプリケーション層マルチキャストミドルウェアの実装とPlanetLab上での評価(セッション4 : オーバレイネットワーク)
- 無線メッシュネットワークのアクセスポイント間通信での優先度順リンク動作方式(トラヒックエンジニアリング,一般,トラヒック,NW評価,性能,リソース管理・制御,トラヒックエンジニアリング,NW信頼性・レジリエンシ,一般)
- 先行経路上の道路情報取得用アドホック通信プロトコルの開発(ITS)
- 目的地選択の公平性と指定されたノード密度分布を実現する移動モデルの提案(学生特別セッション,移動通信ワークショップ)
- チップ内ネットワークの性能要求検証および最適化のための一手法(ネットワーク,通信)
- 即時通信を行うハードウェアのサイクル精度動作記述モジュール群に対するモデル検査の一手法(FPGAとその応用及び一般)
- 即時通信を行うハードウェアのサイクル精度動作記述モジュール群に対するモデル検査の一手法
- 部品のコスト・性能を考慮したリアルタイム組込みシステムの一設計法(VLSI設計技術とCAD)
- 外部入力値のみを保持できる整数変数をもつFSMに対する記号モデル検査法(ソフトウェア工学)
- 実時間通信システムに対する高信頼ハードウェア合成手法の提案(VLSIの設計/検証/テスト及び一般論理合成及び高位合成)
- 実時間通信システムに対する高信頼ハードウェア合成手法の提案(VLSIの設計/検証/テスト及び一般 論理合成及び高位合成)(デザインガイア2003 -VLSI設計の新しい大地を考える研究会-)
- 並行周期EFSM群でモデル化されたQoSルータの高信頼性設計の一手法
- 並行周期EFSMに対するパラメトリックモデル検査手法(LAシンポジウム(計算機科学基礎理論ワークショップ)論文小特集)
- 並行周期EFSMに対するパラメトリックモデル検査およびパラメタ条件簡約高速化の一手法
- 遷移の選択が状態訪問回数で決まる有限状態機械対からなる通信系に対する生存性の検証
- 通信プロトコルのLOTOS仕様から並行EFSM群への変換の一手法
- 遷移の選択が状態訪問回数に依存する有限状態機械対からなる通信系に対する生存性検証システム
- 無線センサーネットワークを利用した電子トリアージシステムの実現(モバイル/放送融合アプリケーション,モバイルコンテンツ,モバイル映像配信,一般)
- 無線センサーネットワークを利用した電子トリアージシステムの実現(学生特別セッション,モバイル/放送融合アプリケーション,モバイルコンテンツ,モバイル映像配信,一般)
- 傷病者の自動監視を実現する電子トリアージシステム(モバイル P2P,ユビキタスネットワーク,アドホックネットワーク,センサネットワーク,一般)
- NGNを活用したセキュア通信提供サービスの提案
- ノード群の相対位置関係に基づく位置推定アルゴリズムの評価手法
- 移動無線端末の位置情報と通信情報を用いた災害現場地図の自動生成
- 断続的に移動する無線端末群の位置推定
- 災害時救急救命支援に向けた電子トリアージシステムの設計開発
- 遭遇端末の位置情報と地理情報を併用した高精度な位置推定手法の提案と評価(ユビキタスネットワーク,ITS,センサーネットワーク,アドホックネットワーク)
- 通信プロトコルのエラーリカバリ性自動検証の一方式
- Deformable Templateマッチング法による唇輪郭抽出法の改良と歯科医療応用を目的とした評価(画像処理,画像パターン認識)
- Deformable-Templateマッチング法による唇輪郭抽出法の改良としきい値自動調整アルゴリズムの提案
- 関数合成による唇輪郭抽出法の提案
- Deformable-Templateマッチング法による唇輪郭抽出法の改良と内眼角点を原点とする座標系表現法の提案
- アプリケーション層マルチキャストミドルウェアの実装とPlanetLab上での評価(セッション4 : オーバレイネットワーク)
- アプリケーション層マルチキャストミドルウェアの実装とPlanetLab上での評価(セッション4 : オーバレイネットワーク)
- An Algebraic Method For Verifying Progress Property of Communication Protocolos
- 都市街路における排気ガス量の削減を目的とする車車間通信を想定したリアルタイム信号制御手法の提案
- 計算負荷分散を考慮した近隣端末の分散型移動予測手法の提案
- センサネットワークアプリケーションの実装支援APIの実装と評価
- 確率事象駆動型モデルを利用した無線ネットワークシミュレーション高速化手法の提案
- 確率事象駆動型モデルを利用した無線ネットワークシミュレーション高速化手法の提案
- 確率事象駆動型モデルを利用した無線ネットワークシミュレーション高速化手法の提案
- 遷移条件が状態訪問回数に依存する有限状態機械対からなる通信系の生存性検証
- 都市街路における排気ガス量の削減を目的とする車車間通信を想定したリアルタイム信号制御手法の提案
- 時間ペトリネットモデルで記述されたサービス仕様からのプロトコル仕様の一合成法
- 拡張有限状態機械とペトリネットを表示編集できるGUIツールの作成と応用例
- 動作実行時刻に制約のある分散システムの全体仕様から各ノードの動作記述の自動導出
- 正則な項書換え系のマルチプロセッサ上での一実現法
- レジスタ付き時間ペトリネットで記述された分散システムの時間制約付き全体仕様からその時間制約を満たす各ノードの動作記述の自動導出(並列・分散)
- ネットワークフローを分散制御するプログラム群の一合成法
- メッシュ型物理トポロジのマルチホップWDMネットワークでの階層型コーダルリングネットワーク構築法の検討(次世代ネットワーク,SIP・プレゼンス,一般)
- 負傷者の状態をリアルタイムに監視する電子トリアージ・タッグの評価
- 負傷者の状態をリアルタイムに監視する電子トリアージ・タッグの評価
- 負傷者の状態をリアルタイムに監視する電子トリアージ・タッグの評価
- プレスブルガー文真偽判定手続きにおける多元連立1次合同式の求解処理の高速化
- アプリケーション層マルチキャストミドルウェアにおける携帯端末への映像配信機構の実装
- 分散協調型無線センサノード群の実行コード自動生成
- 分散協調型無線センサノード群の実行コード自動生成
- 確率事象駆動型モデルを利用した無線ネットワークシミュレーション高速化手法の提案
- 確率事象駆動型モデルを利用した無線ネットワークシミュレーション高速化手法の提案
- 確率事象駆動型モデルを利用した無線ネットワークシミュレーション高速化手法の提案
- センサネットワークアプリケーションの実装支援APIの実装と評価
- センサネットワークアプリケーションの実装支援APIの実装と評価
- センサネットワークアプリケーションの実装支援APIの実装と評価
- 代数的仕様の作成・検証・実現支援システムにおける公理解析部の生成
- データ転送プロトコルに関する性能要求からのプロトコルパラメータの決定
- タイマを用いる有限状態機械でモデル化されたシステムの検証手続き
- タイマを用いる有限状態機械でモデル化されたシステムの検証手続き
- 一つのEFSMの複数EFSMによる実現の正しさの一証明法
- ノードの移動フローを考慮したMANET上での情報共有方式とその評価(セッション8:データマネージメント)
- ノードの移動フローを考慮したMANET上での情報共有方式とその評価(セッション8:データマネージメント)
- 遅延制約のもとで安定性の高いオーバレイマルチキャスト木を構築する分散型プロトコルの提案
- 利己的なエンドノード間でマルチキャストを実現するためのインセンティブ配分法(セッション4 : オーバレイネットワーク)
- 利己的なエンドノード間でマルチキャストを実現するためのインセンティブ配分法(セッション4 : オーバレイネットワーク)
- 利己的なエンドノード間でマルチキャストを実現するためのインセンティブ配分法(セッション4 : オーバレイネットワーク)
- トポロジの多重化によりトラヒック分散を実現した階層型論理トポロジの構成法とそのルーティングアルゴリズム(映像通信,コンテンツ配信ネットワーク,マルチキャスト,一般)
- コンポーネント連携によるサービスをオーバレイネットワーク上で実現するためのサービス設計技法の提案
- アプリケーションレベルマルチキャストEmmaの性能向上に関する検討
- カラーペトリネットを用いた分散協調システムの設計とSOAPを用いた一実装法の提案
- 文脈自由プロセスに対するプロトコル合成の一手法
- イベント間の時間制約を論理式で記述できるラベル付き遷移システムとその双模倣等価性検証
- レジスタ付きペトリネットで書かれたソフトウェアプロセス記述の分散実行系
- プログラム検証支援のためのプレスブルガー文真偽判定ルーチンの高速化
- マルチスレッド機構を用いたLOTOS仕様実行方式とその評価
- 代数的手法を用いた回路設計支援システムにおける状態図簡約機能とその評価
- 通信系の動作記述から各局のプロトコルマシンを生成するための一方法
- 行動検出に基づく空調及び照明機器省エネルギー制御システムの性能評価手法