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. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Hristova, K., & Liu, Y. A. (2006). Improved algorithm complexities for linear temporal logic model checking of pushdown systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3855 LNCS, pp. 190–206). https://doi.org/10.1007/11609773_13
Mendeley helps you to discover research relevant for your work.