Note: This is an archvied version of our old webpage. Some links might be broken. The current one can be found here.
I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
Publications - Model-Checking LTL with Regular Valuations for Pushdown Systems


J. Esparza, A. Kučera, and S. Schwoon. Model-checking LTL with regular valuations for pushdown systems. In Proc. of TACS'2001, number 2215 in Lecture Notes in Computer Science, pages 306–339, 2001.


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.

Suggested BibTeX entry:

    author = {J. Esparza and A. Ku\v{c}era and S. Schwoon},
    booktitle = {Proc. of TACS'2001},
    number = {2215},
    pages = {306--339},
    series = {{Lecture Notes in Computer Science}},
    title = {Model-Checking {LTL} with Regular Valuations for Pushdown Systems},
    year = {2001}

GZipped PostScript (155 kB)
PDF (198 kB)
Journal version