非有界な状態空間をもつ並行システムに対する縮約状態空間の生成について

• 平石 邦彦

  北陸先端科学技術大学院大学 情報科学研究科

書誌事項

タイトル別名

• On Reduced State Space Generation for Concurrent Systems with Unbounded States

抄録

状態空間爆発は並行動作を許すようなシステムの検証において深刻な問題である.本稿ではプロセスが動的に生成されるような並行システムのモデルとして非有界ペトリネットを考え,その検証問題を扱う.非有界ペトリネットの状態空間は無限集合となり、そのままでは有限の手続きですべての状態を調べ尽くすことはできない.本稿では半線形集合の表現を用いることにより、有限の手続きで状態空間を表現する方法を示す.並行システムの効率的な検証方法として,デッドロック等の重要な性質を保存する縮約状態空間を構成する半順序法が提案されているが,本稿では,これらの手法が半線形集合により表現された非有界な状態空間に対しても適用可能であることを示す.

収録刊行物

• 電子情報通信学会技術研究報告. CST, コンカレント工学

  電子情報通信学会技術研究報告. CST, コンカレント工学 95 (137), 1-6, 1995-07-07

  一般社団法人電子情報通信学会

キーワード

• 状態空間爆発
• 並行システム
• 検証
• ペトリネット
• 半線形集合

詳細情報

• CRID: 1572261552350954368
• NII論文ID: 110003300046
• NII書誌ID: AN10438446
• 本文言語コード: ja
• データソース種別:
  • CiNii Articles