@inproceedings{ae1a20aeed0548abb01f1500ee604e09,
title = "Improved algorithm complexities for linear temporal logic model checking of pushdown systems",
abstract = "This paper presents a novel implementation strategy for linear temporal logic (LTL) model checking of pushdown systems (PDS). The model checking problem is formulated intuitively in terms of evaluation of Datalog rules. We use a systematic and fully automated method to generate a specialized algorithm and data structures directly from the rules. The generated implementation employs an incremental approach that considers one fact at a time and uses a combination of linked and indexed data structures for facts. We provide precise time complexity for the model checking problem; it is computed automatically and directly from the rules. We obtain a more precise and simplified complexity analysis, as well as improved algorithm understanding.",
author = "Katia Hristova and Liu, \{Yanhong A.\}",
year = "2006",
language = "English",
isbn = "3540311394",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "190--206",
booktitle = "Verification, Model Checking, and Abstract Interpretation - 7th International Conference, VMCAI 2006, Proceedings",
note = "7th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2006 ; Conference date: 08-01-2006 Through 10-01-2006",
}