Details

Autor(en) / Beteiligte

• La Torre, Salvatore
• Parlato, Gennaro

Titel

On the Complexity of Ltl Model-Checking of Recursive State Machines

Ist Teil von

• Automata, Languages and Programming, p.937-948

Ort / Verlag

Berlin, Heidelberg: Springer Berlin Heidelberg

Link zum Volltext

Quelle

Alma/SFX Local Collection

Beschreibungen/Notizen

• 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 rsm s 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 rsm s, the complexity of model-checking either rises from Pspace-complete to Exptime-complete, or stays within Np.