In this paper we introduce a new (non-Turing powerful) formal model of recursive concurrent programs called well-formed communicating recursive state machines (CRSM). CRSM extend recursive state machines (RSM) 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 CRSM with respect to specifications expressed in a temporal logic that extends CARET with a parallel operator (CONCARET). 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 CARET model checking of RSM, and therefore, we prove that model checking CRSM with respect to CONCARET specifications is EXPTIME-complete. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Bozzelli, L., La Torre, S., & Peron, A. (2006). Verification of well-formed communicating recursive state machines. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3855 LNCS, pp. 412–426). https://doi.org/10.1007/11609773_27
Mendeley helps you to discover research relevant for your work.