LTL Model Checking for Extended Pushdown Systems with Regular Tree Valuations

• Nitta Naoya

  Nara Institute of Science and Technology

• Seki Hiroyuki

  Nara Institute of Science and Technology

Abstract

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

• Information and Media Technologies

  Information and Media Technologies 1 (2), 712-729, 2006

  Information and Media Technologies Editorial Board

Details

• CRID: 1390282680241913472
• NII Article ID: 130000058345
• DOI: 10.11185/imt.1.712
• ISSN: 18810896
• Text Lang: en
• Data Source:
  • JaLC
  • CiNii Articles
• Abstract License Flag: Disallowed