summaryrefslogblamecommitdiff
path: root/Assignment2/report/method.tex
blob: 4f098fa25daaf51810c7d4a581714dfc5377be4a (plain) (tree)

















                                                                                                                              
\section{Method}
To repair a DTMC $\mathcal M$ for a property $\phi$,
	we generate a parametric DTMC $\mathcal M'$ which is like $\mathcal M$ but adds a unique parameter to each transition.
For instance, if $s\to s'$ in $\mathcal M$ with probability $p$,
	in $\mathcal M'$, this transition has probability $p+v_{s,s'}$,
	where $v_{s,s'}$ is not a parameter in $\mathcal M$.
We let $\mathcal V$ denote the set of all parameters $v_{s,s'}$ with $s\to s'$ in $\mathcal M$.

Cost functions can be specified as minimalisation goals on $\mathcal V$.
For the examples in the previous section, we can define:
\begin{equation}
	\textsl{SSE}(\mathcal V) \stackrel{\text{def}}{=} \sum_{v\in\mathcal V} v
\end{equation}
\begin{equation}
	\textsl{MSE}(\mathcal V) \stackrel{\text{def}}{=} \frac{\textsl{SSE}(\mathcal V)}{|\mathcal V|}
\end{equation}
\begin{equation}
	\textsl{NMT}(\mathcal V) \stackrel{\text{def}}{=} \sum_{v\in\mathcal V, v\ne 0} 1
\end{equation}