Advertisement
Published in:
2007 | OriginalPaper | Chapter
On the Complexity of Ltl Model-Checking of Recursive State Machines
Authors : Salvatore La Torre, Gennaro Parlato
Published in: Automata, Languages and Programming
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Recursive state machines (
rsm
s) 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
rsm
s. 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
.