Model-Checking LTL with Regular Valuations for Pushdown Systems

ESPARZA, Javier, Antonín KUČERA and Stefan SCHWOON. Model-Checking LTL with Regular Valuations for Pushdown Systems. N. Kobayashi, B.C. Pierce (Eds.). In 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.

Basic information

Original name

Model-Checking LTL with Regular Valuations for Pushdown Systems

Authors

ESPARZA, Javier, Antonín KUČERA and Stefan SCHWOON
N. Kobayashi, B.C. Pierce (Eds.).

Edition

Berlin, Heidelberg, New York, Proceedings of 4th International Symposium on Theoretical Aspects of Computer Software (TACS 2001), p. 316-340, Lecture Notes in Computer Science, vol. 2215, 2001

Publisher

Springer

---

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

20206 Computer hardware and architecture

Country of publisher

Germany

Confidentiality degree

není předmětem státního či obchodního tajemství

RIV identification code

RIV/00216224:14330/01:00004574

Organization unit

Faculty of Informatics

ISBN

3-540-42736-8

Keywords in English

concurrency; linear temporal logic; pushdown systems

Tags

concurrency, linear temporal logic, pushdown systems

---

Abstract

V originále

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.

---

Links

GA201/00/1023, research and development project	Name: Algoritmy a nástroje pro praktickou verifikaci souběžných systémů Investor: Czech Science Foundation, Algorithms and tools for practical verification of concurrent systems.
GA201/98/P046, research and development project	Name: Rozhodnutelné problémy v algebrách procesů Investor: Czech Science Foundation, (Un)decidable Problems in Process Algebras
MSM 143300001, plan (intention)	Name: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů Investor: Ministry of Education, Youth and Sports of the CR, Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing