Benutzer: Gast  Login
Titel:

Efficient Algorithm for Model Checking Pushdown Systems

Dokumenttyp:
Technical Report
Autor(en):
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)...     »
Stichworte:
model checking; pushdown systems; LTL; infinite-state systems; program analysis
Jahr:
2000
Jahr / Monat:
2000-01-01 00:00:00
Seiten/Umfang:
40
 BibTeX