As has been the case with finite-state systems, the automata-theoretic framework is quite versatile. We demonstrate it by solving several versions of the model-checking problem for LTL specifications and prefix-recognizable systems. Our algorithm is exponential in both the size of (the description of) the system and the size of the LTL specification, and we prove a matching lower bound. This is the first optimal algorithm for solving the LTL model-checking problem for prefix recognizable systems. Our framework also handles systems with regular labeling, and in fact we show that LTL model checking with respect to pushdown systems with regular labeling is intereducible with LTL model checking with respect to prefix-recognizable systems with simple labeling.
@inproceedings{KPV02,
author = "O. Kupferman and N. Piterman and M. Vardi",
title = "Model Checking Linear Properties of Prefix-Recognizable Systems",
booktitle = "14th International Conference on Computer Aided Verification",
series = "Lecture Notes in Computer Science",
volume = 2404,
pages = "371--385",
month = "July",
year = 2002
}