J 2003

Model checking LTL with regular valuations for pushdown systems

ESPARZA, Javier, Antonín KUČERA a Stefan SCHWOON

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

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Spojené státy

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

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 22. 11. 2006 18:17, prof. RNDr. Antonín Kučera, Ph.D.

Anotace

V originále

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