Verification of Well-Formed Communicating Recursive State Machines.

In this paper we introduce a new (non-Turing powerful) formal model of recursive concurrent programs called well-formed communicating recursive state machines (). extend recursive state machines () by allowing a restricted form of concurrency: a state of a module can be refined into a finite collection of modules (working in parallel) in a potentially recursive manner. Communication is only possible between the activations of modules invoked on the same fork. We study the model checking problem of with respect to specifications expressed in a temporal logic that extends with a parallel operator (). We propose a decision algorithm that runs in time exponential in both the size of the formula and the maximum number of modules that can be invoked simultaneously. This matches the known lower bound for deciding model checking of , and therefore, we prove that model checking with respect to specifications is -complete. [ABSTRACT FROM AUTHOR]