ESPARZA, Javier, Antonín KUČERA and Stefan SCHWOON. Model checking LTL with regular valuations for pushdown systems. Information and Computation, Academic Press, 2003, vol. 186, No 2, p. 355-376. ISSN 0890-5401.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Model checking LTL with regular valuations for pushdown systems
Authors ESPARZA, Javier (724 Spain), Antonín KUČERA (203 Czechia, guarantor) and Stefan SCHWOON (276 Germany).
Edition Information and Computation, Academic Press, 2003, 0890-5401.
Other information
Original language English
Type of outcome article in a journal
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher United States of America
Confidentiality degree is not subject to a state or trade secret
Impact factor Impact factor: 0.851
RIV identification code RIV/00216224:14330/03:00008160
Organization unit Faculty of Informatics
UT WoS 000185794900008
Keywords in English model-checking; liner-time logic; pushdown systems
Tags liner-time logic, Model-Checking, pushdown systems
Tags International impact, Reviewed
Changed by Changed by: prof. RNDr. Antonín Kučera, Ph.D., učo 2508. Changed: 22/11/2006 18:17.
Abstract
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.
Links
GA201/00/1023, research and development projectName: Algoritmy a nástroje pro praktickou verifikaci souběžných systémů
Investor: Czech Science Foundation, Standard Projects
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, Research Intents
PrintDisplayed: 5/8/2020 15:24