NAISTAR
Advanced Search
Japanese | English

naistar (NAIST Academic Repository) >
学術リポジトリ naistar / NAIST Academic Repository naistar >
テクニカルレポート / Technical Report >

Please use this identifier to cite or link to this item: http://hdl.handle.net/10061/3155

Title: An extension of pushdown system and its model checking method
Authors: Nitta, Naoya
Seki, Hiroyuki
ニッタ, ナオヤ
セキ, ヒロユキ
新田, 直也
関, 浩之
Issue Date: Jun-2003
Publisher: Nara Institute of Science and Technology
Series/Report no.: Information Science Technical Report ~ TR2003007
Abstract: In this paper, we present a class of infinite transition systems which is an extension of pushdown systems (PDS), and show that LTL (linear temporal logic) model checking for the class is decidable. Sincthe class is defined as a subclass of term rewriting systems, pushdown stack of PDS is naturally extended to tree structure. By this extension, we can model recursive programs with exception handling.
URI: http://hdl.handle.net/10061/3155
URI: http://library.naist.jp/mylimedio/dllimedio/show.cgi?bookid=100037131&oldid=67913
Fulltext: http://library.naist.jp/mylimedio/dllimedio/show.cgi?bookid=100037131&oldid=67913
ISSN: 0919-9527
Text Version: author
Appears in Collections:テクニカルレポート / Technical Report

Files in This Item:

There are no files associated with this item.

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.

 

Copyright (c) 2007-2012 Nara Institute of Science and Technology All Rights Reserved.
DSpace Software Copyright © 2002-2010  Duraspace - Feedback