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.

Verification of Well-Formed Communicating Recursive State Machines / A., Bozzelli; S., LA TORRE S; Peron, Adriano. - STAMPA. - 3855:(2006), pp. 412-426. (Intervento presentato al convegno 7th International Conference, VMCAI 2006, tenutosi a Charleston, SC, USA, nel 8-10 gennaio 2006) [10.1007/11609773_27].

Verification of Well-Formed Communicating Recursive State Machines

A. BOZZELLI;PERON, ADRIANO
2006

Abstract

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.
2006
3540311394
9783540311393
Verification of Well-Formed Communicating Recursive State Machines / A., Bozzelli; S., LA TORRE S; Peron, Adriano. - STAMPA. - 3855:(2006), pp. 412-426. (Intervento presentato al convegno 7th International Conference, VMCAI 2006, tenutosi a Charleston, SC, USA, nel 8-10 gennaio 2006) [10.1007/11609773_27].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11588/120564
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact