diff options
Diffstat (limited to 'Assignment2/report/assignment2.tex')
| -rw-r--r-- | Assignment2/report/assignment2.tex | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/Assignment2/report/assignment2.tex b/Assignment2/report/assignment2.tex index c9a94f7..48e9328 100644 --- a/Assignment2/report/assignment2.tex +++ b/Assignment2/report/assignment2.tex @@ -29,13 +29,22 @@ \maketitle \begin{abstract} - Model repair bladibla % TODO + We discuss an approach to the repair of parametric models using an SMT solver. + To repair a model $\mathcal M$ which does not satisfy a probabilistic CTL formula $\phi$, + we add an additional parameter to the probability of each transition in $\mathcal M$, + after which we eliminate all non-initial non-absorbing states. + The SMT solver gets constraints to ensure that the repaired model remains valid + and to satisfy $\phi$. + Cost functions for the model repair problem can be formulated as a minimisation goal for the SMT solver. + Unfortunately, some technical issues prevent us from using the tool in practice. + We provide pointers to future work to resolve these issues. \end{abstract} \input{intro} \input{method} \input{implementation} \input{discussion} +\input{future} \bibliography{library} \bibliographystyle{splncs04} |