Anzeige
Erschienen in:
2000 | OriginalPaper | Buchkapitel
Model Checking CTL Properties of Pushdown Systems
verfasst von : Igor Walukiewicz
Erschienen in: FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
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
A pushdown system is a graph G(P) of configurations of a pushdown automaton P. The model checking problem for a logic L is: given a pushdown automaton P and a formula ? ∈ L decide if ? holds in the vertex of G(P) which is the initial configuration of P. Computation Tree Logic (CTL) and its fragment EF are considered. The model checking problems for CTL and EF are shown to be EXPTIME-complete and PSPACE-complete, respectively.