Model-checking LTL with regular valuations for pushdown systems

Abstract

Recent works have proposed pushdown systems as a tool for analyzing programs with (recursive) procedures. In particular, the modelchecking 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.