プッシュダウンシステムの拡張およびそのモデル検査法

• Item type: Trans(1)
• 公開日: 2003-10-15
• タイトル: プッシュダウンシステムの拡張およびそのモデル検査法
• タイトル / 言語: en
• タイトル: An Extension of Pushdown System and Its Model Checking Method
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 発表概要
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 奈良先端科学技術大学院大学情報科学研究科
• 著者所属: 奈良先端科学技術大学院大学情報科学研究科
• 著者所属(英): en
• 著者所属(英): Graduate School of Information Science, Nara Institute of Science and Technology
• 著者所属(英): en
• 著者所属(英): Graduate School of Information Science, Nara Institute of Science and Technology
• 著者名: 新田, 直也; 関, 浩之
• 著者名(英): Naoya, Nitta; Hiroyuki, Seki
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 現在，無限の状態空間を持つ遷移システムに対するモデル検査法の研究がさかんに行われており，特にプッシュダウンシステムやペトリネットに対するモデル検査において良い結果が得られている．本発表では，プッシュダウンシステムを拡張した遷移システムを項書き換え系の部分クラスとして定義し，そのLTL （線形時相論理）によるモデル検査が決定可能となることを示す．プッシュダウンシステムの項書き換え系による定式化は，一般に文字列で表現されるスタック構造の木構造への拡張を意味し，この拡張によってより豊かなデータ構造を持った遷移システムの自動検証が可能になることが期待される．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Recently, in the field of model checking, many researches for infinite systems have been done. Particularly for pushdown systems and petri nets, there are good decidablity results on model checking. In this presentation, we define a class of transition systems which is an extension of pushdown systems as a subclass of TRS (term rewriting systems) and show that LTL (linear temporal logic) model checking problem for the class is decidable. Formulating pushdown systems as a subclass of TRS, we can extend the structure of stacks to tree structure. By this extension, it is expected that transition systems with richer data structure become verifiable.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 44, 号 SIG13(PRO18), p. 111-111, 発行日 2003-10-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会