Model-Checking LTL with Regular Valuations for Pushdown Systems
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F01%3A00004574" target="_blank" >RIV/00216224:14330/01:00004574 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
Model-Checking LTL with Regular Valuations for Pushdown Systems
Original language description
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 systemswith checkpoints, etc., and provide a general, unifying and efficient framework for solving these problems.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
JC - Computer hardware and software
OECD FORD branch
—
Result continuities
Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
Z - Vyzkumny zamer (s odkazem do CEZ)
Others
Publication year
2001
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Proceedings of 4th International Symposium on Theoretical Aspects of Computer Software (TACS 2001)
ISBN
3-540-42736-8
ISSN
—
e-ISSN
—
Number of pages
25
Pages from-to
316
Publisher name
Springer
Place of publication
Berlin, Heidelberg, New York
Event location
Berlin, Heidelberg, New York
Event date
Jan 1, 2001
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—