## 2 Event Language
### Trace Semantics of Expressions  
In this section, we define the trace semantics of expressions of the language. The first step is the definition of the notion of dependence between events; the relation we use is taken from [PERSON]'s trace theory [3, 15]. _Dependence._A dependence relation (dependence for short) over a finite alphabet \(A\) is any reflexive, symmetric relation \(D\subseteq A\times A\). A dependence \(D\) over the alphabet \(A\) determines the symmetric and irreflexive relation \(I_{D}\subseteq A\times A\), called the independence relation determined by \(D\) and defined as \(I_{D}=A\times A-D\). The ordered triple \((A^{*},.,\epsilon)\), where \(\epsilon\) is the empty string and. is the concatenation operation on strings, is the standard string monoid over \(A\). Usually, the sign. for concatenation is omitted. Let \(A\) be an alphabet and \(\sigma\in A^{*}\); then for any alphabet \(B\) we denote \(\Pi_{B}(\sigma)\) the string projection of \(\sigma\) onto \(B\), _i.e._, a string over \(A\cap B\) obtained from \(\sigma\) deleting all symbols not belonging to \(B\). If \(A\cap B=\emptyset\), \(\Pi_{B}(\sigma)=\epsilon\), for any \(\sigma\). A concurrent alphabet is any ordered pair \(\Sigma=(A,D)\), where \(A\) is a finite set of symbols, called also the alphabet of \(\Sigma\), and \(D\) is a dependence over \(A\). Given \(\Sigma=(A,D)\), the trace equivalence for \(\Sigma\) is the least congruence \(\equiv_{\Sigma}\) in the string monoid over \(A\), such that for all \(a,b\):  
\[(a,b)\in I_{D}\Rightarrow ab\equiv_{\Sigma}ba\]  
In other words, it holds that \(\sigma\equiv_{\Sigma}\sigma^{\prime}\) if there is a finite sequence of strings \(\sigma_{0},\sigma_{1},\ldots,\sigma_{n},\ n\geq 0\), such that \(\sigma_{0}=\sigma,\ \sigma_{n}=\sigma^{\prime}\), and for each \(i\), \(1\leq i\leq n\), \(\sigma_{i-1}=\delta_{1}ab\delta_{2}\), \(\sigma_{i}=\delta_{1}ba\delta_{2}\), for some \((a,b)\in I_{D}\) and \(\delta_{1},\delta_{2}\in A^{*}\). Equivalence classes of \(\equiv_{\Sigma}\) are called traces over \(\Sigma\); given a string \(\sigma\in A^{*}\), \([\sigma]_{\Sigma}\) is the equivalence class of \(\sigma\) over \(\Sigma\). When clear from the context, we omit \(\Sigma\). The set \(\Theta(\Sigma)=[A^{*}]_{\Sigma}\) is the set of all traces over \(\Sigma\). The concatenation of traces, denoted by \([\sigma_{1}][\sigma_{2}]\), is defined as \([\sigma_{1}\sigma_{2}]\). For any alphabet \(B\), it holds that \(\Pi_{B}([\sigma])=[\Pi_{B}(\sigma)]\) and \(alph([\sigma])=alph(\sigma)\). _Dependence Closure._Given two dependencies, \(D_{1}\) and \(D_{2}\), defined on the alphabets \(A_{1}\) and \(A_{2}\), respectively, we call dependence closure the derived dependence on the alphabet \(A_{1}\cup A_{2}\):  
\[D_{1}D_{2}^{\circ}=D_{1}\cup D_{2}\cup\{(a_{1},a_{2}),(a_{2},a_{1})\mid a_{1} \in A_{1},a_{2}\in A_{2}\}\]  
_Trace System._A trace system \(TS\) is any ordered pair \((\Sigma,T)\), where \(\Sigma=(A,D)\) is a concurrent alphabet and \(T\subseteq\Theta(\Sigma)\) is a trace language over \(\Sigma\). To manage only finite sets of traces also in the presence of recursive behaviors, we extend the alphabet \(A\) by a set of special symbols (called holes): a hole represents the fact that the trace is incomplete and can be expanded; we also call this type of trace a partial trace. Each hole has the form \(\lfloor\ \rfloor_{x}\), where \(x\) is the name of a trace language; in fact, any trace belonging to the language \(x\) can be used to fill the hole giving rise to another partial trace. Some operations can be performed on trace systems. * Given the trace system \(TS=((A,D),T)\),
* its unbounded iteration is the system: \[TS_{1}=(((A,D),T))^{*}=((A\cup\{\lfloor\ \rfloor_{T}\},D\cup D^{\prime}),\{[\epsilon],\lfloor\ \rfloor_{T}\})\] where: \[D^{\prime}=\{(\lfloor\ \rfloor_{T},\lfloor\ \rfloor_{T})\}\cup\{(a,\lfloor\ \rfloor_{T}),(\lfloor\ \rfloor_{T},a)\mid a\in A\}\]  
The following example gives a first hint of the effect of the unbounded iteration of trace systems. **Example 1**.