2000 | OriginalPaper | Buchkapitel
Efficient Algorithms for Model Checking Pushdown Systems
verfasst von : Javier Esparza, David Hansel, Peter Rossmanith, Stefan Schwoon
Erschienen in: Computer Aided Verification
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We study model checking problems for pushdown systems and linear time logics. We show that the global model checking problem (computing the set of configurations, reachable or not, that violate the formula) can be solved in $O({g_{\cal P}}{g_{\cal P}}^3{g_{\cal B}}{g_{\cal B}}^3)$ time and $O({g_{\cal P}}{g_{\cal P}}^2{g_{\cal B}}{g_{\cal B}}^2)$ space, where ${g_{\cal P}}{g_{\cal P}}$ and ${g_{\cal B}}{g_{\cal B}}$ are the size of the pushdown system and the size of a Büchi automaton for the negation of the formula. The global model checking problem for reachable configurations can be solved in $O({g_{\cal P}}{g_{\cal P}}^4{g_{\cal B}}{g_{\cal B}}^3)$ time and $O({g_{\cal P}}{g_{\cal P}}^4{g_{\cal B}}{g_{\cal B}}^2)$ space. In the case of pushdown systems with constant number of control states (relevant for our application), the complexity becomes $O({g_{\cal P}}{g_{\cal P}}{g_{\cal B}}{g_{\cal B}}^3)$ time and $O({g_{\cal P}}{g_{\cal P}}{g_{\cal B}}{g_{\cal B}}^2)$ space and $O({g_{\cal P}}{g_{\cal P}}^2{g_{\cal B}}{g_{\cal B}}^3)$ time and $O({g_{\cal P}}{g_{\cal P}}^2{g_{\cal B}}{g_{\cal B}}^2)$ space, respectively. We show applications of these results in the area of program analysis and present some experimental results.