Nothing Special   »   [go: up one dir, main page]

Information and Media Technologies
Online ISSN : 1881-0896
ISSN-L : 1881-0896
Computing
LTL Model Checking for Extended Pushdown Systems with Regular Tree Valuations
Naoya NittaHiroyuki Seki
Author information
JOURNAL FREE ACCESS

2006 Volume 1 Issue 2 Pages 712-729

Details
Abstract

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.

Content from these authors
© 2006 by Japan Society for Software Science and Technology
Previous article Next article
feedback
Top