\documentclass[runningheads]{llncs}

\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{cleveref}
\usepackage{csquotes}
\usepackage{minted}
\usepackage{tikz}
\usetikzlibrary{automata,positioning}

\let\leq\leqslant
\let\le\leqslant
\let\geq\geqslant
\let\ge\geqslant

\DeclareMathOperator{\Uop}{\mathsf{U}}

\newcommand{\PRISM}{\texttt{PRISM}}

\begin{document}

\title{Model Repair in Clean \textbackslash{}o/}
\author{Camil Staps \and Erin van der Veen}
\authorrunning{C. Staps \and E. van der Veen}
\institute{%
	Radboud University, Nijmegen, The Netherlands\\
	\email{\{c.staps,e.vanderveen\}@student.ru.nl}}

\maketitle

\begin{abstract}
	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}

\end{document}