文章基本信息

标题：LTL Model Checking for Extended Pushdown Systems with Regular Tree Valuations
本地全文：下载
作者：Naoya Nitta ; Hiroyuki Seki
期刊名称：Information and Media Technologies
电子版ISSN：1881-0896
出版年度：2006
卷号：1
期号：2
页码：712-729
DOI：10.11185/imt.1.712
出版社：Information and Media Technologies Editorial Board
摘要：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.