Other formats:
BibTeX
LaTeX
RIS
@inproceedings{372791,
author = {Esparza, Javier and Kučera, Antonín and Schwoon, Stefan},
address = {Berlin, Heidelberg, New York},
booktitle = {Proceedings of 4th International Symposium on Theoretical Aspects of Computer Software (TACS 2001)},
keywords = {concurrency; linear temporal logic; pushdown systems},
language = {eng},
location = {Berlin, Heidelberg, New York},
isbn = {3-540-42736-8},
pages = {316-340},
publisher = {Springer},
title = {Model-Checking LTL with Regular Valuations for Pushdown Systems},
year = {2001}
}
TY - JOUR
ID - 372791
AU - Esparza, Javier - Kučera, Antonín - Schwoon, Stefan
PY - 2001
TI - Model-Checking LTL with Regular Valuations for Pushdown Systems
VL - Lecture Notes in Computer Science, vol. 2215
PB - Springer
CY - Berlin, Heidelberg, New York
SN - 3540427368
KW - concurrency
KW - linear temporal logic
KW - pushdown systems
N2 - 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.
ER -
ESPARZA, Javier, Antonín KUČERA and Stefan SCHWOON. Model-Checking LTL with Regular Valuations for Pushdown Systems. Online. N. Kobayashi, B.C. Pierce (Eds.). In \textit{Proceedings of 4th International Symposium on Theoretical Aspects of Computer Software (TACS 2001)}. Berlin, Heidelberg, New York: Springer, 2001. p.~316-340. Lecture Notes in Computer Science, vol. 2215. ISBN~3-540-42736-8. [citováno 2024-04-24]
|
