Model-Checking LTL with Regular Valuations for Pushdown Systems

Investor logo
Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

ESPARZA Javier KUČERA Antonín SCHWOON Stefan

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

Faculty of Informatics

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:

You are running an old browser version. We recommend updating your browser to its latest version.