Model-Checking LTL with Regular Valuations for Pushdown Systems
| Authors | |
|---|---|
| Year of publication | 2001 |
| Type | Article in Proceedings |
| Conference | Proceedings of 4th International Symposium on Theoretical Aspects of Computer Software (TACS 2001) |
| MU Faculty or unit | |
| Citation | |
| Field | Computer hardware and software |
| Keywords | concurrency; linear temporal logic; pushdown systems |
| Description | 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. |
| Related projects: |