文章基本信息

标题：拡張プッシュダウンシステムの正則木評価によるLTLモデル検査法
本地全文：下载
作者：新田直也 ; 関浩之
期刊名称：コンピュータソフトウェア
印刷版ISSN：0289-6540
出版年度：2005
卷号：22
期号：3
页码：3_58-3_75
DOI：10.11309/jssst.22.3_58
出版社：Japan Society for Software Science and Technology
摘要：
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.