Model-Checking LTL with Regular Valuations for Pushdown Systems

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 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.

Základní údaje

Originální název

Model-Checking LTL with Regular Valuations for Pushdown Systems

Autoři

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

Vydání

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

Nakladatel

Springer

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

20206 Computer hardware and architecture

Stát vydavatele

Německo

Utajení

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

Kód RIV

RIV/00216224:14330/01:00004574

Organizační jednotka

Fakulta informatiky

ISBN

3-540-42736-8

Klíčová slova anglicky

concurrency; linear temporal logic; pushdown systems

Štítky

concurrency, linear temporal logic, pushdown systems

---

Anotace

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.

---

Návaznosti

GA201/00/1023, projekt VaV	Název: Algoritmy a nástroje pro praktickou verifikaci souběžných systémů Investor: Grantová agentura ČR, Algoritmy a nástroje pro praktickou verifikaci souběžných systémů
GA201/98/P046, projekt VaV	Název: Rozhodnutelné problémy v algebrách procesů Investor: Grantová agentura ČR, Rozhodnutelné problémy v algebrách procesů
MSM 143300001, záměr	Název: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů