Efficient Algorithms for Model Checking Pushdown Systems

摘要: We study model checking problems for pushdown systems and linear time logics. show that the global problem (computing set of configurations, reachable or not, violate formula) can be solved in \(O({g_{\cal P}}{g_{\cal P}}^3{g_{\cal B}}{g_{\cal B}}^3)\) P}}^2{g_{\cal B}}^2)\) space, where \({g_{\cal P}}\) B}}\) are size system a Buchi automaton negation formula. The configurations P}}^4{g_{\cal space. In case with constant number control states (relevant our application), complexity becomes space respectively. applications these results area program analysis present some experimental results.