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. s. 316-340. Lecture Notes in Computer Science, vol. 2215. ISBN 3-540-42736-8. 2001.
Další formáty:   BibTeX LaTeX RIS
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
Originální 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
Změnil Změnil: prof. RNDr. Antonín Kučera, Ph.D., učo 2508. Změněno: 29. 11. 2001 12:25.
Anotace
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 VaVNá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 VaVNázev: Rozhodnutelné problémy v algebrách procesů
Investor: Grantová agentura ČR, Rozhodnutelné problémy v algebrách procesů
MSM 143300001, záměrNá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ů
VytisknoutZobrazeno: 29. 3. 2024 01:18