Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Model-Checking LTL with Regular Valuations for Pushdown Systems
Authors: Stefan Schwoon ; Javier Esparza ; Antonin Kucera
Date:Aug 2001
Publication Title:Proceedings of TACS 2001
Publication Type:Conference Paper
Recent works have proposed pushdown systems as a tool for analyzing programs with (recursive) procedures. In particular, the model-checking problem for LTL has been studied. In this paper we examine an extension of this, namely model-checking with regular valuations. The problem is solved via two different techniques, with an eye on efficiency -- both techniques can be shown to be essentially optimal. Our methods are applicable to problems in different areas, e.g., data-flow analysis, analysis of systems with checkpoints, etc., and provide a general, unifying and efficient framework for solving these problems.
2001 by The University of Edinburgh. All Rights Reserved
Links To Paper
No links available
Bibtex format
author = { Stefan Schwoon and Javier Esparza and Antonin Kucera },
title = {Model-Checking LTL with Regular Valuations for Pushdown Systems},
book title = {Proceedings of TACS 2001},
year = 2001,
month = {Aug},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh