User: Guest  Login
Title:

Efficient Algorithm for Model Checking Pushdown Systems

Document type:
Technical Report
Author(s):
Javier Esparza; David Hansel; Peter Rossmanith; Stefan Schwoon
Abstract:
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(gp^3 gb^3) time and O(gp^2 gb^2) space, where gp and gb are the size of the pushdown system and the size of a Buechi automaton for the negation of the formula. The global model checking problem for reachable configurations can be solved in O(gp^4 gb^3) time and O(gp^4 gb^2)...     »
Keywords:
model checking; pushdown systems; LTL; infinite-state systems; program analysis
Year:
2000
Year / month:
2000-01-01 00:00:00
Pages:
40
 BibTeX