ESPARZA, Javier, Antonín KUČERA a Stefan SCHWOON. Model checking LTL with regular valuations for pushdown systems. Information and Computation, Academic Press, 2003, roč. 186, č. 2, s. 355-376. ISSN 0890-5401.
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 (724 Španělsko), Antonín KUČERA (203 Česká republika, garant) a Stefan SCHWOON (276 Německo).
Vydání Information and Computation, Academic Press, 2003, 0890-5401.
Další údaje
Originální jazyk angličtina
Typ výsledku Článek v odborném periodiku
Obor Computer sciences, information science, bioinformatics
Stát vydavatele Spojené státy americké
Utajení není předmětem státního či obchodního tajemství
Impakt faktor Impact factor: 0.851
Kód RIV RIV/00216224:14330/03:00008160
Organizační jednotka Fakulta informatiky
UT WoS 000185794900008
Klíčová slova anglicky model-checking; liner-time logic; pushdown systems
Štítky liner-time logic, Model-Checking, pushdown systems
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: prof. RNDr. Antonín Kučera, Ph.D., učo 2508. Změněno: 22. 11. 2006 18:17.
Anotace
Recent works have proposed pushdown systems as a tool for analyzing programs with (recursive) procedures, and the model-checking problem for LTL has been devoted special attention. However, all these works impose a strong restriction on the possible valuations of atomic propositions: whether a configuration of the pushdown system satisfies an atomic proposition or not can only depend on the current control state of the pushdown automaton and on its topmost stack symbol. In this paper we consider LTL with regular valuations: the set of configurations satisfying an atomic proposition can be an arbitrary regular language. The model-checking problem is solved via two different techniques, with an eye on efficiency. The resulting algorithms are proved to be asymptotically optimal. We show that the extension to regular valuations allows to model problems in different areas, like data-flow analysis and analysis of systems with checkpoints. We claim that our model-checking algorithms provide a general, unifying and efficient framework for solving them.
Návaznosti
GA201/00/1023, projekt VaVNázev: Algoritmy a nástroje pro praktickou verifikaci souběžných systémů
Investor: Grantová agentura ČR, Standardní projekty
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, Výzkumné záměry
VytisknoutZobrazeno: 21. 10. 2019 12:54