User: Guest  Login
Document type:
Technical Report 
Author(s):
Javier Esparza; David Hansel; Peter Rossmanith; Stefan Schwoon 
Title:
Efficient Algorithm for Model Checking Pushdown Systems 
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