Reference:

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.

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.

Suggested BibTeX entry:

@inproceedings{EKS01,
    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}
}