拡張プッシュダウンシステムの正則木評価によるLTLモデル検査法

• 新田 直也

  奈良先端科学技術大学院大学

• 関 浩之

  奈良先端科学技術大学院大学

書誌事項

タイトル別名

• LTT Model Checking for Extended Pushdown Systems with Regular Tree Valuations
• LTL Model Checking for Extended Pushdown Systems with Regular Tree Valuations

抄録

In this paper, we show an algorithm of LTL (linear temporal logic) model checking for LL-GG-TRS with regular tree valuation. The class LL-GG-TRS is defined as a subclass of term rewriting systems, and extends the class of pushdown systems (PDS) in the sence that pushdown stack of PDS is extended to tree structure. By this extension, we can model recursive programs with exception handling.

収録刊行物

• コンピュータ ソフトウェア

  コンピュータ ソフトウェア 22 (3), 58-75, 2005

  日本ソフトウェア科学会

詳細情報

• CRID: 1390282679714990592
• NII論文ID: 110008016660
• NII書誌ID: AN10075819
• DOI: 10.11309/jssst.22.3_58
• NDL書誌ID: 7832257
• ISSN: 02896540
• Web Site: http://id.ndl.go.jp/bib/7832257
• Web Site: https://ndlsearch.ndl.go.jp/books/R000000004-I7832257
• 本文言語コード: en
• データソース種別:
  • JaLC
  • NDL
  • CiNii Articles
• 抄録ライセンスフラグ: 使用不可