blob: 4f098fa25daaf51810c7d4a581714dfc5377be4a (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
\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}
|
