## 3 Selective Mu-Calculus
### The Satisfaction of the Formulae on Trace Systems  
To define the formula satisfaction on trace systems, we will build a particular trace presentation; the behavior of the operators that produce this presentation is based on a rewriting rule, which transforms a trace into an equivalent one. **Definition 3** (Rewriting rule). : _Consider \(\Sigma=(A,D)\) and \(\gamma ba\gamma^{\prime}\in A^{*}\)._  
\[\gamma ba\gamma^{\prime}\mapsto\gamma ab\gamma^{\prime}\quad\text{if }(b,a)\in I_{D}\]  
_The rule transforms a string into an equivalent one, since:_  
\[(b,a)\in I_{D}\Rightarrow\gamma ba\gamma^{\prime}\equiv_{\Sigma}\gamma ab \gamma^{\prime}\]The following function \(\mathcal{D}\) uses the auxiliary function \(\mathcal{M}\), shown in Table 1. The function \(\mathcal{M}\), given a string \(\beta\), marks all the events in \(\beta\). If \(A\) is an alphabet, we write \(A^{-}\) for the set \(\{a\mid a\in A\wedge a\
eq\lfloor\ \rfloor_{x},\forall\ \lfloor\ \rfloor_{x}\in A\}\). Intuitively, \(A^{-}\) is the set of all of the symbols of the alphabet \(A\), except for the holes. \(\mathcal{D}_{a,S}(\sigma)\) manipulates traces exploiting a simple algorithm that moves events according to the rewriting rule. The result of \(\mathcal{D}_{a,S}(\sigma)\) is a trace without the events occurring before \(a\) in any run (the events in \(\delta_{1}\) do not matter for the successive verification), but that includes the events occurring in some run after \(a\) and in some run before \(a\) (they are the marked events in \(\delta_{2}\), with the mark remembering that they do not necessarily occur where they are); it includes also (they are the events in \(\delta_{3}\)) the events that occur after \(a\) in any run and, if present, the event in \(S\) (such an event is required to occur after \(a\) in all runs of interest; this fact is guaranteed by the constraint expressed in Point a) of Definition 4). The complexity of the trace manipulations is polynomial in the number of elements of the trace itself in the worst case, when at each step, all of the events are moved up and down to verify if they can occur before and/or after \(a\); linear in the better case, when only the reading of all of the events of the trace is required, since the rewriting rule cannot ever be applied. The following example shows, in more detail, the effect of \(\mathcal{M}\). \begin{table}
\begin{tabular}{l l} \hline \hline \multicolumn{2}{l}{Let \(A\) be an alphabet: consider \(a\in A\) and \(\beta\in A^{*}\).} \\ \(\mathcal{M}(a.\beta)\) & \(=\) & \(\bar{a}.\mathcal{M}(\beta)\) \\ \(\mathcal{M}(\epsilon)\) & \(=\) & \(\epsilon\) \\ \hline \hline \end{tabular}
\end{table} 
Table 1: Marking function. **Example 5**. : _Consider the two concurrent alphabets: \(\Sigma_{1}=(\{a,b,c\},\ \{(a,a),\ (b,b),\ (c,c),\ (a,b),\ (b,a)\})\) and: \(\Sigma_{2}=(\{a,b,c\},\ \{(a,a),\ (b,b),\ (c,c),\ (b,c),\ (c,b)\})\)._  
* _If_ \(S=\emptyset\)_:_ \(\mathcal{D}_{a,S}(cab)=[\bar{c}b]\)_, for_ \(\Sigma_{1}\)_, and_ \(\mathcal{D}_{a,S}(cab)=[\bar{c}\bar{b}]\)_, for_ \(\Sigma_{2}\)_, while_ \(\mathcal{D}_{b,S}(cab)=[\bar{c}]\)_, for_ \(\Sigma_{1}\)_, and_ \(\mathcal{D}_{b,S}(cab)=[\bar{a}]\)_, for_ \(\Sigma_{2}\)__
* _If_ \(S=\{b\}\)__ \(\mathcal{D}_{a,S}(cab)=[\bar{c}b]\) _for both_ \(\Sigma_{1}\) _and_ \(\Sigma_{2}\)_, while_ \(\mathcal{D}_{b,S}(cab)=[\bar{c}]\)_, for_ \(\Sigma_{1}\)_, and_ \(\mathcal{D}_{b,S}(cab)=[\bar{a}]\)_, for_ \(\Sigma_{2}\)__  
The formal satisfaction of a formula \(\psi\) by a trace \([\sigma]\) is defined as follows. Note that we consider the event set \(\widetilde{X}=X\cup\bar{X}\), where \(\bar{X}=\{\bar{x}|x\in X\}\) as the alphabet for strings, since it is possible to obtain strings containing marked events. In Table 2, auxiliary cleaning functions are shown that either eliminate the marks from the events of a string (\(\mathcal{C}l^{2}\)) before the next verification step is performed or eliminate the marked events at all (\(\mathcal{C}l^{1}\)), as shown in the following Example 6.