- Abstract:
-
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.
- Copyright:
- 2001 by The University of Edinburgh. All Rights Reserved
- Links To Paper
- No links available
- Bibtex format
- @InProceedings{EDI-INF-RR-0044,
- 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},
- }
|
