Operatori

Gli operatori servono per comporre le azioni ed i processi in espressioni che descrivono il comportamento di un sistema concorrente. Ad ogni operatore è associato un certo numero di assiomi e regole di transizione (regole di inferenza) che permettono al sistema stesso di passare da uno stato ad un altro.

Solitamente una regola di transizione viene definita tramite una barra orizzontale sopra la quale si scrive un insieme di premesse $ \pi_1\:,\: \cdots, \pi_n$ e sotto la quale si indica la conclusione $ c \rightarrow c'$:

$\displaystyle \renewcommand {\arraystretch}{1.2}
\begin{array}{c}\pi_1\:,\: \cdots , \pi_n\\
\hline c \rightarrow c'
\end{array} $

Data una regola di questo tipo possiamo dire che "se valgono le condizioni $ \pi_1\:,\: \cdots, \pi_n$, allora è sicuramente valida l'implicazione $ c \rightarrow c'\:$".

In un assioma invece non sono presenti le premesse, perciò la conclusione è sempre valida:

$\displaystyle \renewcommand {\arraystretch}{1.2}
\begin{array}{c}\\
\hline c \rightarrow c'
\end{array} $

Ogni algebra di processi ha un numero fissato di operatori, i quali possono essere statici o dinamici. Nel primo caso il combinatore $ opr$ è presente sia prima che dopo l'esecuzione della transizione in cui viene utilizzato, quindi la sua costruzione persiste attraverso qualunque sequenza di azioni:

$\displaystyle \renewcommand {\arraystretch}{1.2}
\begin{array}{c}P_{i1} \stack...
...ts,P_n) \stackrel{\alpha}{\longrightarrow} opr (P_1',\cdots,P_n')
\end{array} $

dove $ \{i1,\cdots,1m\} \subseteq \{1,\cdots,n\}$.

Nei combinatori dinamici, al contrario, $ opr$ è presente prima dell'azione, ma è assente dopo.

Inoltre gli operatori possono essere deterministici o non deterministici a seconda del modo in cui influenzano appunto il determinismo di un sistema.

Qui trattiamo gli operatori più utilizzati e conosciuti nella teoria. Possiamo suddividerli in gruppi per comprenderne meglio l'utilizzo.



Subsections
Morpheus 2004-02-10