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