Other formats:
BibTeX
LaTeX
RIS
@article{488376,
author = {Esparza, Javier and Kučera, Antonín and Schwoon, Stefan},
article_number = {2},
keywords = {model-checking; liner-time logic; pushdown systems},
language = {eng},
issn = {0890-5401},
journal = {Information and Computation},
title = {Model checking LTL with regular valuations for pushdown systems},
volume = {186},
year = {2003}
}
TY - JOUR
ID - 488376
AU - Esparza, Javier - Kučera, Antonín - Schwoon, Stefan
PY - 2003
TI - Model checking LTL with regular valuations for pushdown systems
JF - Information and Computation
VL - 186
IS - 2
SP - 355
EP - 355
PB - Academic Press
SN - 08905401
KW - model-checking
KW - liner-time logic
KW - pushdown systems
N2 - Recent works have proposed pushdown systems as a tool for analyzing programs with (recursive) procedures, and the model-checking problem for LTL has been devoted special attention. However, all these works impose a strong restriction on the possible valuations of atomic propositions: whether a configuration of the pushdown system satisfies an atomic proposition or not can only depend on the current control state of the pushdown automaton and on its topmost stack symbol. In this paper we consider LTL with regular valuations: the set of configurations satisfying an atomic proposition can be an arbitrary regular language. The model-checking problem is solved via two different techniques, with an eye on efficiency. The resulting algorithms are proved to be asymptotically optimal. We show that the extension to regular valuations allows to model problems in different areas, like data-flow analysis and analysis of systems with checkpoints. We claim that our model-checking algorithms provide a general, unifying and efficient framework for solving them.
ER -
ESPARZA, Javier, Antonín KUČERA and Stefan SCHWOON. Model checking LTL with regular valuations for pushdown systems. \textit{Information and Computation}. Academic Press, vol.~186, No~2, p.~355-376. ISSN~0890-5401. 2003.
|
