Model-Checking LTL with Regular Valuations for Pushdown Systems

Logo poskytovatele
Logo poskytovatele

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

ESPARZA Javier KUČERA Antonín SCHWOON Stefan

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

Fakulta informatiky

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:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.