naistar (NAIST Academic Repository) >
学術リポジトリ naistar / NAIST Academic Repository naistar >
テクニカルレポート / Technical Report >
Please use this identifier to cite or link to this item:
|Title: ||An extension of pushdown system and its model checking method|
|Authors: ||Nitta, Naoya|
|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.|
|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.