concl.tex
\vspace*{-0.4cm}
\section{Conclusions}\label{concl-sect}

\vspace*{-0.2cm}
We have presented novel techniques for multi-objective model checking of MDPs,
using a value iteration-based computation to build successive approximations of the Pareto curve.
%based on generation of successive approximations of the Pareto curve using value iteration.
Compared to existing approaches, this gives significant gains in efficiency and scalability,
and enables verification of time-bounded properties.
Furthermore, we showed the benefits of visualising the Pareto curve
for several probabilistic model checking case studies.
%
Future directions include extending our techniques
to timed probabilistic models such as CTMDPs and PTAs.

graph3d.tex
\begin{tikzpicture}[scale=0.3,x = {(-4.499513cm,-1.834018cm)}, y = {(0cm,6.577848cm)},z = {(2.304853cm,-0.661467cm)},font=\scriptsize]
\tikzstyle{every node}+=[font=\tiny]
\draw[-latex'] (0,0,0) -- (0,0,2.4465306122448984);
\draw[-latex'] (0,0,0) -- (0,1.1200000000000006,0);
\draw[-latex'] (0,0,0) -- (1.1200000000000006,0,0);
\draw (0.5,0,0) -- (0.5,0.04,0) node[above, inner sep=1pt] {0.5};
\draw (1.0,0,0) -- (1.0,0.04,0) node[above, inner sep=1pt] {1};
\draw (0,0.5,0) -- (0.04,0.5,0) node[left, inner sep=1pt] {0.5};
\draw (0,1.0,0) -- (0.04,1.0,0) node[left, inner sep=1pt] {1};
\draw (0,0,0.5) -- (0,0.04,0.5) node[above, inner sep=1pt] {0.5};
\draw (0,0,1.0) -- (0,0.04,1.0) node[above, inner sep=1pt] {1};
\draw (0,0,1.5) -- (0,0.04,1.5) node[above, inner sep=1pt] {1.5};
\draw (0,0,2.0) -- (0,0.04,2.0) node[above, inner sep=1pt] {2};
\path[fill, line width=0pt, opacity=0.3, color=gray!40] (0.7551020408163269, 0.0, 2.326530612244897) -- (0.0, 0.7551020408163269, 2.3265306122448965) -- (0.0, 0.0, 2.3265306122448983) -- cycle;
\path[fill, line width=0pt, opacity=0.3, color=gray!40] (0.2448979591836734, 0.9999999999999997, 0.0) -- (0.0, 1.0000000000000007, 0.0) -- (0.0, 1.0000000000000007, 2.020408163265302) -- cycle;
\path[fill, line width=0pt, opacity=0.3, color=gray!40] (1.0000000000000007, 0.0, 0.0) -- (1.0000000000000007, 0.24489795918366936, 0.0) -- (1.0000000000000007, 0.0, 2.0204081632653015) -- cycle;
\path[fill, line width=0pt, opacity=0.3, color=gray!40] (0.7551020408163269, 0.0, 2.326530612244897) -- (0.7551020408163269, 0.48979591836734715, 2.3265306122448934) -- (0.0, 0.7551020408163269, 2.3265306122448965) -- cycle;
\path[fill, line width=0pt, opacity=0.3, color=gray!40] (0.9387755102040825, 0.0, 2.142857142857143) -- (0.7551020408163269, 0.48979591836734715, 2.3265306122448934) -- (0.7551020408163269, 0.0, 2.326530612244897) -- cycle;
\path[fill, line width=0pt, opacity=0.3, color=gray!40] (0.8775510204081638, 0.3673469387755106, 0.0) -- (0.2448979591836734, 0.9999999999999997, 0.0) -- (0.7551020408163269, 0.48979591836734715, 2.3265306122448934) -- cycle;
\path[fill, line width=0pt, opacity=0.3, color=gray!40] (1.0000000000000007, 0.24489795918366936, 0.0) -- (0.8775510204081638, 0.3673469387755106, 0.0) -- (0.7551020408163269, 0.48979591836734715, 2.3265306122448934) -- cycle;
\path[fill, line width=0pt, opacity=0.3, color=gray!40] (0.2448979591836734, 0.9999999999999998, 2.0204081632653073) -- (0.0, 1.0000000000000007, 2.020408163265302) -- (0.0, 0.9387755102040825, 2.142857142857141) -- cycle;
\path[fill, line width=0pt, opacity=0.3, color=gray!40] (0.2448979591836734, 0.9999999999999998, 2.0204081632653073) -- (0.2448979591836734, 0.9999999999999997, 0.0) -- (0.0, 1.0000000000000007, 2.020408163265302) -- cycle;
\path[fill, line width=0pt, opacity=0.3, color=gray!40] (0.7551020408163269, 0.48979591836734715, 2.3265306122448934) -- (0.2448979591836734, 0.9999999999999997, 0.0) -- (0.2448979591836734, 0.9999999999999998, 2.0204081632653073) -- cycle;
\path[fill, line width=0pt, opacity=0.3, color=gray!40] (1.0000000000000007, 0.0, 2.0204081632653015) -- (1.0000000000000007, 0.2448979591836734, 2.0204081632653077) -- (0.9387755102040825, 0.0, 2.142857142857143) -- cycle;
\path[fill, line width=0pt, opacity=0.3, color=gray!40] (1.0000000000000007, 0.24489795918366936, 0.0) -- (1.0000000000000007, 0.2448979591836734, 2.0204081632653077) -- (1.0000000000000007, 0.0, 2.0204081632653015) -- cycle;
\path[fill, line width=0pt, opacity=0.3, color=gray!40] (1.0000000000000007, 0.24489795918366936, 0.0) -- (0.7551020408163269, 0.48979591836734715, 2.3265306122448934) -- (1.0000000000000007, 0.2448979591836734, 2.0204081632653077) -- cycle;
%\path[fill, line width=0pt, opacity=0.3, color=gray!40] (1.0000000000000007, 0.2448979591836734, 2.0204081632653077) -- (0.7551020408163269, 0.48979591836734715, 2.3265306122448934) -- (0.2448979591836734, 0.9999999999999998, 2.0204081632653073) -- cycle;
%\path[fill, line width=0pt, opacity=0.3, color=gray!40] (1.0000000000000007, 0.2448979591836734, 2.0204081632653077) -- (0.2448979591836734, 0.9999999999999998, 2.0204081632653073) -- (0.7551020408163269, 0.48979591836734715, 2.3265306122448934) -- cycle;
%\path[fill, line width=0pt, opacity=0.3, color=gray!40] (1.0000000000000007, 0.2448979591836734, 2.0204081632653077) -- (0.2448979591836734, 0.9999999999999998, 2.0204081632653073) -- (0.7551020408163269, 0.48979591836734715, 2.3265306122448934) -- cycle;
%\path[fill, line width=0pt, opacity=0.3, color=gray!40] (0.7551020408163269, 0.48979591836734715, 2.3265306122448934) -- (0.2448979591836734, 0.9999999999999998, 2.0204081632653073) -- (1.0000000000000007, 0.2448979591836734, 2.0204081632653077) -- cycle;
%\path[fill, line width=0pt, opacity=0.3, color=gray!40] (0.9387755102040825, 0.0, 2.142857142857143) -- (0.7551020408163269, 0.2448979591836734, 2.326530612244897) -- (0.7551020408163269, 0.48979591836734715, 2.3265306122448934) -- cycle;
%\path[fill, line width=0pt, opacity=0.3, color=gray!40] (0.7551020408163269, 0.48979591836734715, 2.3265306122448934) -- (0.7551020408163269, 0.2448979591836734, 2.326530612244897) -- (0.9387755102040825, 0.0, 2.142857142857143) -- cycle;
\path[fill, line width=0pt, opacity=0.3, color=gray!40] (0.48979591836734715, 0.7551020408163269, 2.3265306122448965) -- (0.0, 0.9387755102040825, 2.142857142857141) -- (0.0, 0.7551020408163269, 2.3265306122448965) -- cycle;
\path[fill, line width=0pt, opacity=0.3, color=gray!40] (0.7551020408163269, 0.48979591836734715, 2.3265306122448934) -- (0.48979591836734715, 0.7551020408163269, 2.3265306122448965) -- (0.0, 0.7551020408163269, 2.3265306122448965) -- cycle;
\path[fill, line width=0pt, opacity=0.3, color=gray!40] (0.7551020408163269, 0.48979591836734715, 2.3265306122448934) -- (0.2448979591836734, 0.9999999999999998, 2.0204081632653073) -- (0.48979591836734715, 0.7551020408163269, 2.3265306122448965) -- cycle;
\path[fill, line width=0pt, opacity=0.3, color=gray!40] (0.9387755102040825, 0.30612244897959184, 2.1428571428571392) -- (0.7551020408163269, 0.48979591836734715, 2.3265306122448934) -- (0.9387755102040825, 0.0, 2.142857142857143) -- cycle;
\path[fill, line width=0pt, opacity=0.3, color=gray!40] (1.0000000000000007, 0.2448979591836734, 2.0204081632653077) -- (0.9387755102040825, 0.30612244897959184, 2.1428571428571392) -- (0.9387755102040825, 0.0, 2.142857142857143) -- cycle;
\path[fill, line width=0pt, opacity=0.3, color=gray!40] (1.0000000000000007, 0.2448979591836734, 2.0204081632653077) -- (0.7551020408163269, 0.48979591836734715, 2.3265306122448934) -- (0.9387755102040825, 0.30612244897959184, 2.1428571428571392) -- cycle;
\path[fill, line width=0pt, opacity=0.3, color=gray!40] (0.2448979591836734, 0.9387755102040825, 2.142857142857141) -- (0.0, 0.9387755102040825, 2.142857142857141) -- (0.48979591836734715, 0.7551020408163269, 2.3265306122448965) -- cycle;
\path[fill, line width=0pt, opacity=0.3, color=gray!40] (0.2448979591836734, 0.9999999999999998, 2.0204081632653073) -- (0.0, 0.9387755102040825, 2.142857142857141) -- (0.2448979591836734, 0.9387755102040825, 2.142857142857141) -- cycle;
\path[fill, line width=0pt, opacity=0.3, color=gray!40] (0.30612244897959184, 0.9387755102040825, 2.1428571428571406) -- (0.2448979591836734, 0.9387755102040825, 2.142857142857141) -- (0.48979591836734715, 0.7551020408163269, 2.3265306122448965) -- cycle;
\path[fill, line width=0pt, opacity=0.3, color=gray!40] (0.2448979591836734, 0.9999999999999998, 2.0204081632653073) -- (0.30612244897959184, 0.9387755102040825, 2.1428571428571406) -- (0.48979591836734715, 0.7551020408163269, 2.3265306122448965) -- cycle;
\path[fill, line width=0pt, opacity=0.3, color=gray!40] (0.2448979591836734, 0.9999999999999998, 2.0204081632653073) -- (0.2448979591836734, 0.9387755102040825, 2.142857142857141) -- (0.30612244897959184, 0.9387755102040825, 2.1428571428571406) -- cycle;
\draw[color=gray] (0.7551020408163269, 0.0, 2.326530612244897) -- (0.7551020408163269, 0.48979591836734715, 2.3265306122448934);
\draw[color=gray] (0.2448979591836734, 0.9999999999999998, 2.0204081632653073) -- (0.0, 1.0000000000000007, 2.020408163265302);
\draw[color=gray] (0.2448979591836734, 0.9999999999999998, 2.0204081632653073) -- (0.2448979591836734, 0.9999999999999997, 0.0);
\draw[color=gray] (1.0000000000000007, 0.0, 2.0204081632653015) -- (1.0000000000000007, 0.2448979591836734, 2.0204081632653077);
\draw[color=gray] (1.0000000000000007, 0.24489795918366936, 0.0) -- (1.0000000000000007, 0.2448979591836734, 2.0204081632653077);
\draw[color=gray] (0.48979591836734715, 0.7551020408163269, 2.3265306122448965) -- (0.0, 0.7551020408163269, 2.3265306122448965);
\draw[color=gray] (0.7551020408163269, 0.48979591836734715, 2.3265306122448934) -- (0.48979591836734715, 0.7551020408163269, 2.3265306122448965);
\draw[color=gray] (0.9387755102040825, 0.30612244897959184, 2.1428571428571392) -- (0.9387755102040825, 0.0, 2.142857142857143);
\draw[color=gray] (0.9387755102040825, 0.30612244897959184, 2.1428571428571392) -- (0.7551020408163269, 0.48979591836734715, 2.3265306122448934);
\draw[color=gray] (1.0000000000000007, 0.2448979591836734, 2.0204081632653077) -- (0.9387755102040825, 0.30612244897959184, 2.1428571428571392);
\draw[color=gray] (0.2448979591836734, 0.9387755102040825, 2.142857142857141) -- (0.0, 0.9387755102040825, 2.142857142857141);
\draw[color=gray] (0.30612244897959184, 0.9387755102040825, 2.1428571428571406) -- (0.48979591836734715, 0.7551020408163269, 2.3265306122448965);
\draw[color=gray] (0.30612244897959184, 0.9387755102040825, 2.1428571428571406) -- (0.2448979591836734, 0.9387755102040825, 2.142857142857141);
\draw[color=gray] (0.2448979591836734, 0.9999999999999998, 2.0204081632653073) -- (0.30612244897959184, 0.9387755102040825, 2.1428571428571406);

\path[-latex'] (0,0,0) -- (0,0,2.4465306122448984) node[pos=1, above] {$z$};
\path[-latex'] (0,0,0) -- (0,1.1200000000000006,0) node[pos=0.95, right] {$y$};;
\path[-latex'] (0,0,0) -- (1.1200000000000006,0,0) node[pos=0.9, below] {$x$};;
\end{tikzpicture}

paper.bbl
\begin{thebibliography}{10}
\providecommand{\url}[1]{\texttt{#1}}
\providecommand{\urlprefix}{URL }

\bibitem{Altman99}
Altman, E.: Constrained Markov Decision Processes. Chapman \& Hall/CRC (1999)

\bibitem{BLTZ03}
Bleuler, S., Laumanns, M., Thiele, L., Zitzler, E.: {PISA-A Platform and
  Programming Language Independent Interface for Search Algorithms}. In: EMO'03
  (2003)

\bibitem{Boyd04}
Boyd, S., Vandenberghe, L.: Convex Optimization. Cambridge Univ. Press (2004)

\bibitem{BBC+11}
Br\'azdil, T., Bro\v{z}ek, V., Chatterjee, K., Forejt, V., Ku\v{c}era, A.: Two
  views on multiple mean-payoff objectives in {M}arkov decision processes. In:
  LICS'11 (2011)

\bibitem{CMH06}
Chatterjee, K., Majumdar, R., Henzinger, T.: Markov decision processes with
  multiple objectives. In: Proc. STACS'06. pp. 325--336. Springer (2006)

\bibitem{Cli97}
Cl\'{i}ımaco, J. (ed.): Multicriteria Analysis. Springer (1997)

\bibitem{CLV07}
Coello, C., Lamont, G., van Veldhuizen, D.: Evolutionary Algorithms for Solving
  Multi-Objective Problems. Springer (2007)

\bibitem{DY08}
Diakonikolas, I., Yannakakis, M.: Succinct approximate convex {Pareto} curves.
  In: Proc. SODA'08. pp. 74--83. SIAM (2008)

\bibitem{EKVY08}
Etessami, K., Kwiatkowska, M., Vardi, M., Yannakakis, M.: Multi-objective model
  checking of {Markov} decision processes. LMCS  4(4),  1--21 (2008)

\bibitem{FKNP11}
Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated verification
  techniques for probabilistic systems. In: SFM'11. LNCS, vol. 6659. Springer
  (2011)

\bibitem{FKN+11}
Forejt, V., Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Quantitative
  multi-objective verification for probabilistic systems. In: Proc. TACAS'11
  (2011)

\bibitem{FKP12}
Forejt, V., Kwiatkowska, M., Parker, D.: Pareto curves for probabilistic model
  checking. In: Proc. ATVA'12. LNCS, Springer (2012), to appear

\bibitem{KSK76}
Kemeny, J., Snell, J., Knapp, A.: Denumerable {M}arkov Chains. Springer (1976)

\bibitem{KNP11}
Kwiatkowska, M., Norman, G., Parker, D.: {PRISM} 4.0: Verification of
  probabilistic real-time systems. In: Proc. CAV'11. LNCS, vol. 6806, pp.
  585--591. Springer (2011)

\bibitem{KNPQ10}
Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Assume-guarantee verification
  for probabilistic systems. In: Proc. TACAS'10. pp. 23--37. Springer (2010)

\bibitem{LCM11}
Legriel, J., Cotton, S., Maler, O.: On universal search strategies for
  multi-criteria optimization using weighted sums. In: Proc. CEC'11. pp.
  2351--2358 (2011)

\bibitem{LLCM10}
Legriel, J., Guernic, C.L., Cotton, S., Maler, O.: Approximating the {Pareto}
  front of multi-criteria optimization problems. In: Proc. TACAS'10. pp. 69--83
  (2010)

\bibitem{PY00}
Papadimitriou, C., Yannakakis, M.: On the approximability of trade-offs and
  optimal access of web sources. In: Proc. FOCS'00. pp. 86--92 (2000)

\bibitem{Put94}
Puterman, M.: Markov Decision Processes: Discrete Stochastic Dynamic
  Programming. John Wiley and Sons (1994)

\end{thebibliography}
