6533b836fe1ef96bd12a148c

RESEARCH PRODUCT

Verification of Well-Formed Communicating Recursive State Machines

Laura BozzelliAdriano PeronSalvatore La Torre

subject

Model checkingModel checkingTheoretical computer scienceGeneral Computer ScienceComputer scienceInfinite state systemModuloConcurrencyTree automataTheoretical Computer ScienceFormal models of concurrency and recursionTuring machinesymbols.namesakeFormal specificationTemporal logicContext-free specificationsRecursionLinear-time logicsPushdown systemsAbstract interpretationAutomatonTheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGESInfinite-state systemsrecursive state machinesymbolsState (computer science)Linear time logicAlgorithmComputer Science(all)

description

AbstractIn this paper we introduce a new (non-Turing equivalent) 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.

yearjournalcountryeditionlanguage
2008-08-01
10.1007/11609773_27http://hdl.handle.net/11588/120564