Model-Checking LTL with Regular Valuations for Pushdown Systems
| Autoři | |
|---|---|
| Rok publikování | 2001 |
| Druh | Článek ve sborníku |
| Konference | Proceedings of 4th International Symposium on Theoretical Aspects of Computer Software (TACS 2001) |
| Fakulta / Pracoviště MU | |
| Citace | |
| Obor | Počítačový hardware a software |
| Klíčová slova | concurrency; linear temporal logic; pushdown systems |
| Popis | 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. |
| Související projekty: |