Další formáty:
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 a Stefan SCHWOON. Model-Checking LTL with Regular Valuations for Pushdown Systems. 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, s.~316-340. Lecture Notes in Computer Science, vol. 2215. ISBN~3-540-42736-8.
|