On the complexity of LTL model-checking of recursive state machines

Abstract

Recursive state machines (RSMs) are models for programs with recursive procedural calls. While LTL model-checking is Exptime-complete on such models, on finite-state machines, it is PSPACE-complete in general and becomes NP-complete for interesting fragments. In this paper, we systematically study the computational complexity of model-checking RSMs against several syntactic fragments of LTL. Our main result shows that if in the specification we disallow next and until, and retain only the box and diamond operators, model-checking is in NP. Thus, differently from the full logic, for this fragment the abstract complexity of model-checking does not change moving from finite-state machines to RSMS. Our results on the other studied fragments confirm this trend, in the sense that, moving from finite-state machines to RSMS, the complexity of model-checking either rises from PSPACE-complete to EXPTIME-complete, or stays within NP. © Springer-Verlag Berlin Heidelberg 2007.