Model-checking LTL with regular valuations for pushdown systems

Javier Esparza; Antonín Kucera; Stefan Schwoon

doi:10.1007/3-540-45500-0_16

Model-checking LTL with regular valuations for pushdown systems

Javier Esparza, Antonín Kucera, Stefan Schwoon

Informatics 7 - Chair of Theoretical Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

29 Scopus citations

Abstract

Recent works have proposed pushdown systems as a tool for analyzing programs with (recursive) procedures. In particular, the modelchecking 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.

Original language	English
Title of host publication	Theoretical Aspects of Computer Software - 4th International Symposium, TACS 2001, Proceedings
Editors	Naoki Kobayashi, Benjamin C. Pierce
Publisher	Springer Verlag
Pages	316-339
Number of pages	24
ISBN (Print)	3540427368, 9783540427360
DOIs	https://doi.org/10.1007/3-540-45500-0_16
State	Published - 2001
Event	4th International Symposium on Theoretical Aspects of Computer Software, TACS 2001 - Sendai, Japan Duration: 29 Oct 2001 → 31 Oct 2001

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	2215
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	4th International Symposium on Theoretical Aspects of Computer Software, TACS 2001
Country/Territory	Japan
City	Sendai
Period	29/10/01 → 31/10/01

Access to Document

10.1007/3-540-45500-0_16

Cite this

Esparza, J., Kucera, A., & Schwoon, S. (2001). Model-checking LTL with regular valuations for pushdown systems. In N. Kobayashi, & B. C. Pierce (Eds.), Theoretical Aspects of Computer Software - 4th International Symposium, TACS 2001, Proceedings (pp. 316-339). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2215). Springer Verlag. https://doi.org/10.1007/3-540-45500-0_16

Esparza, Javier ; Kucera, Antonín ; Schwoon, Stefan. / Model-checking LTL with regular valuations for pushdown systems. Theoretical Aspects of Computer Software - 4th International Symposium, TACS 2001, Proceedings. editor / Naoki Kobayashi ; Benjamin C. Pierce. Springer Verlag, 2001. pp. 316-339 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{dbf236356edf4508933344b6daeb5067,

title = "Model-checking LTL with regular valuations for pushdown systems",

abstract = "Recent works have proposed pushdown systems as a tool for analyzing programs with (recursive) procedures. In particular, the modelchecking 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.",

author = "Javier Esparza and Anton{\'i}n Kucera and Stefan Schwoon",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2001.; 4th International Symposium on Theoretical Aspects of Computer Software, TACS 2001 ; Conference date: 29-10-2001 Through 31-10-2001",

year = "2001",

doi = "10.1007/3-540-45500-0_16",

language = "English",

isbn = "3540427368",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "316--339",

editor = "Naoki Kobayashi and Pierce, {Benjamin C.}",

booktitle = "Theoretical Aspects of Computer Software - 4th International Symposium, TACS 2001, Proceedings",

}

Esparza, J, Kucera, A & Schwoon, S 2001, Model-checking LTL with regular valuations for pushdown systems. in N Kobayashi & BC Pierce (eds), Theoretical Aspects of Computer Software - 4th International Symposium, TACS 2001, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2215, Springer Verlag, pp. 316-339, 4th International Symposium on Theoretical Aspects of Computer Software, TACS 2001, Sendai, Japan, 29/10/01. https://doi.org/10.1007/3-540-45500-0_16

Model-checking LTL with regular valuations for pushdown systems. / Esparza, Javier; Kucera, Antonín; Schwoon, Stefan.
Theoretical Aspects of Computer Software - 4th International Symposium, TACS 2001, Proceedings. ed. / Naoki Kobayashi; Benjamin C. Pierce. Springer Verlag, 2001. p. 316-339 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2215).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Model-checking LTL with regular valuations for pushdown systems

AU - Esparza, Javier

AU - Kucera, Antonín

AU - Schwoon, Stefan

N1 - Publisher Copyright: © Springer-Verlag Berlin Heidelberg 2001.

PY - 2001

Y1 - 2001

N2 - Recent works have proposed pushdown systems as a tool for analyzing programs with (recursive) procedures. In particular, the modelchecking 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.

AB - Recent works have proposed pushdown systems as a tool for analyzing programs with (recursive) procedures. In particular, the modelchecking 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.

UR - http://www.scopus.com/inward/record.url?scp=84978974912&partnerID=8YFLogxK

U2 - 10.1007/3-540-45500-0_16

DO - 10.1007/3-540-45500-0_16

M3 - Conference contribution

AN - SCOPUS:84978974912

SN - 3540427368

SN - 9783540427360

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 316

EP - 339

BT - Theoretical Aspects of Computer Software - 4th International Symposium, TACS 2001, Proceedings

A2 - Kobayashi, Naoki

A2 - Pierce, Benjamin C.

PB - Springer Verlag

T2 - 4th International Symposium on Theoretical Aspects of Computer Software, TACS 2001

Y2 - 29 October 2001 through 31 October 2001

ER -

Esparza J, Kucera A, Schwoon S. Model-checking LTL with regular valuations for pushdown systems. In Kobayashi N, Pierce BC, editors, Theoretical Aspects of Computer Software - 4th International Symposium, TACS 2001, Proceedings. Springer Verlag. 2001. p. 316-339. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-45500-0_16

Model-checking LTL with regular valuations for pushdown systems

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this