LTT Model Checking for Extended Pushdown Systems with Regular Tree Valuations

DOI Web Site 24 References

Bibliographic Information

Other Title
  • 拡張プッシュダウンシステムの正則木評価によるLTLモデル検査法
  • LTL Model Checking for Extended Pushdown Systems with Regular Tree Valuations

Search this article

Description

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.

Journal

  • Computer Software

    Computer Software 22 (3), 58-75, 2005

    Japan Society for Software Science and Technology

References(24)*help

See more

Details 詳細情報について

Report a problem

Back to top