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.

• Information and Media Technologies 編集運営会議の論文

著者

• Seki Hiroyuki

  Nara Inst. Sci. And Technol. Ikoma‐shi Jpn

• Nitta Naoya

  Nara Inst. Sci. And Technol. Ikoma‐shi Jpn

• Nitta Naoya

  Nara Institute of Science and Technology

関連論文

• Layered Transducing Term Rewriting System and Its Recognizability Preserving Property (Special Issue on Selected Papers from LA Symposium)
• Termination Property of Inverse Finite Path Overlapping Term Rewriting System is Decidable
• Finite State Translation Systems and Parallel Multiple Context-Free Grammars
• Policy Controlled System and Its Model Checking
• Decidability of the Security Verification Problem for Programs with Stack Inspection
• Formal Language Theoretic Approach to the Disclosure Tree Strategy in Trust Negotiation
• Comparison of the Expressive Power of Language-Based Access Control Models
• FOREWORD
• Error Control for High-density Monochrome Two-dimensional Barcodes
• LTL Model Checking for Extended Pushdown Systems with Regular Tree Valuations

スポンサーリンク