@inproceedings(DBLP:conf/concur/Alfaro99,
 author       = "Luca de Alfaro",
 year         = "1999",
 title        = "Computing Minimum and Maximum Reachability Times in Probabilistic Systems",
 editor       = "Jos C. M. Baeten and Sjouke Mauw",
 booktitle    = "CONCUR",
 series       = "Lecture Notes in Computer Science",
 volume       = "1664",
 publisher    = "Springer",
 pages        = "66--81",
 doi          = "10.1007/3-540-48320-9\_7",
)
@book(DBLP:books/daglib/0020348,
 author       = "Christel Baier and Joost-Pieter Katoen",
 year         = "2008",
 title        = "Principles of model checking",
 publisher    = "MIT Press",
)
@article(DBLP:journals/iandc/BaierKHW05,
 author       = "Christel Baier and Joost-Pieter Katoen and Holger Hermanns and Verena Wolf",
 year         = "2005",
 title        = "Comparative branching-time semantics for {M}arkov chains",
 journal      = "Inf. Comput.",
 volume       = "200",
 number       = "2",
 pages        = "149--214",
 doi          = "10.1016/j.ic.2005.03.001",
)
@book(bertsekas1996neuro,
 author       = "D. P. Bertsekas and J.N. Tsitsiklis",
 year         = "1996",
 title        = "Neuro-Dynamic Programming",
 series       = "Anthropological Field Studies",
 publisher    = "Athena Scientific",
)
@article(bertsekas1991analysis,
 author       = "Dimitri P Bertsekas and John N Tsitsiklis",
 year         = "1991",
 title        = "An analysis of stochastic shortest path problems",
 journal      = "Mathematics of Operations Research",
 volume       = "16",
 number       = "3",
 pages        = "580--595",
 doi          = "10.1287/moor.16.3.580",
)
@incollection(blum2000probabilistic,
 author       = "Avrim L Blum and John C Langford",
 year         = "2000",
 title        = "Probabilistic planning in the graphplan framework",
 booktitle    = "Recent Advances in AI Planning",
 publisher    = "Springer",
 pages        = "319--332",
 doi          = "10.1007/10720246\_25",
)
@inproceedings(DBLP:conf/cav/BohyBFJR12,
 author       = "Aaron Bohy and V{\'e}ronique Bruy{\`e}re and Emmanuel Filiot and Naiyong Jin and Jean-Fran\c {c}ois Raskin",
 year         = "2012",
 title        = "Acacia+, a Tool for {LTL} Synthesis",
 editor       = "P. Madhusudan and Sanjit A. Seshia",
 booktitle    = "CAV",
 series       = "Lecture Notes in Computer Science",
 volume       = "7358",
 publisher    = "Springer",
 pages        = "652--657",
 doi          = "10.1007/978-3-642-31424-7\_45",
)
@article(DBLP:journals/corr/abs-1210-3539,
 author       = "Aaron Bohy and V{\'e}ronique Bruy{\`e}re and Emmanuel Filiot and Jean-Fran\c {c}ois Raskin",
 year         = "2012",
 title        = "Synthesis from {LTL} Specifications with Mean-Payoff Objectives",
 journal      = "CoRR",
 volume       = "abs/1210.3539",
 url          = "http://arxiv.org/abs/1210.3539",
)
@inproceedings(DBLP:conf/tacas/BohyBFR13,
 author       = "Aaron Bohy and V{\'e}ronique Bruy{\`e}re and Emmanuel Filiot and Jean-Fran\c {c}ois Raskin",
 year         = "2013",
 title        = "Synthesis from {LTL} Specifications with Mean-Payoff Objectives",
 editor       = "Nir Piterman and Scott A. Smolka",
 booktitle    = "TACAS",
 series       = "Lecture Notes in Computer Science",
 volume       = "7795",
 publisher    = "Springer",
 pages        = "169--184",
 doi          = "10.1007/978-3-642-36742-7\_12",
)
@article(2014arXiv1402.1076B,
 author       = "Aaron Bohy and V{\'e}ronique Bruy{\`e}re and Jean-Fran\c {c}ois Raskin",
 year         = "2014",
 title        = "Symblicit algorithms for optimal strategy synthesis in monotonic {M}arkov decision processes (extended version)",
 journal      = "CoRR",
 volume       = "abs/1402.1076",
 url          = "http://arxiv.org/abs/1402.1076",
)
@inproceedings(DBLP:conf/wia/BouajjaniHHTV08,
 author       = "Ahmed Bouajjani and Peter Habermehl and Luk{\'a}s Hol\'{\i }k and Tayssir Touili and Tom{\'a}s Vojnar",
 year         = "2008",
 title        = "Antichain-Based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata",
 editor       = "Oscar H. Ibarra and Bala Ravikumar",
 booktitle    = "CIAA",
 series       = "Lecture Notes in Computer Science",
 volume       = "5148",
 publisher    = "Springer",
 pages        = "57--67",
 doi          = "10.1007/978-3-540-70844-5\_7",
)
@article(buchholz1994exact,
 author       = "Peter Buchholz",
 year         = "1994",
 title        = "Exact and ordinary lumpability in finite {M}arkov chains",
 journal      = "Journal of applied probability",
 pages        = "59--75",
 doi          = "10.2307/3215235",
)
@article(DBLP:journals/iandc/BurchCMDH92,
 author       = "Jerry R. Burch and Edmund M. Clarke and Kenneth L. McMillan and David L. Dill and L. J. Hwang",
 year         = "1992",
 title        = "Symbolic Model Checking: $10^{20}$ States and Beyond",
 journal      = "Inf. Comput.",
 volume       = "98",
 number       = "2",
 pages        = "142--170",
 doi          = "10.1016/0890-5401(92)90017-A",
)
@inproceedings(DBLP:conf/tacas/ChatterjeeHJS11,
 author       = "Krishnendu Chatterjee and Thomas A. Henzinger and Barbara Jobstmann and Rohit Singh",
 year         = "2011",
 title        = "QUASY: Quantitative Synthesis Tool",
 editor       = "Parosh Aziz Abdulla and K. Rustan M. Leino",
 booktitle    = "TACAS",
 series       = "Lecture Notes in Computer Science",
 volume       = "6605",
 publisher    = "Springer",
 pages        = "267--271",
 doi          = "10.1007/978-3-642-19835-9\_24",
)
@inproceedings(DBLP:conf/lop/ClarkeE81,
 author       = "Edmund M. Clarke and E. Allen Emerson",
 year         = "1981",
 title        = "Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic",
 editor       = "Dexter Kozen",
 booktitle    = "Logic of Programs",
 series       = "Lecture Notes in Computer Science",
 volume       = "131",
 publisher    = "Springer",
 pages        = "52--71",
 doi          = "10.1007/BFb0025774",
)
@article(DBLP:journals/ipl/DerisaviHS03,
 author       = "Salem Derisavi and Holger Hermanns and William H. Sanders",
 year         = "2003",
 title        = "Optimal state-space lumping in {M}arkov chains",
 journal      = "Inf. Process. Lett.",
 volume       = "87",
 number       = "6",
 pages        = "309--315",
 doi          = "10.1016/S0020-0190(03)00343-0",
)
@inproceedings(DBLP:conf/tacas/DoyenR07,
 author       = "Laurent Doyen and Jean-Fran\c {c}ois Raskin",
 year         = "2007",
 title        = "Improved Algorithms for the Automata-Based Approach to Model-Checking",
 editor       = "Orna Grumberg and Michael Huth",
 booktitle    = "TACAS",
 series       = "Lecture Notes in Computer Science",
 volume       = "4424",
 publisher    = "Springer",
 pages        = "451--465",
 doi          = "10.1007/978-3-540-71209-1\_34",
)
@inproceedings(DBLP:conf/tacas/DoyenR10,
 author       = "Laurent Doyen and Jean-Fran\c {c}ois Raskin",
 year         = "2010",
 title        = "Antichain Algorithms for Finite Automata",
 editor       = "Javier Esparza and Rupak Majumdar",
 booktitle    = "TACAS",
 series       = "Lecture Notes in Computer Science",
 volume       = "6015",
 publisher    = "Springer",
 pages        = "2--22",
 doi          = "10.1007/978-3-642-12002-2\_2",
)
@inproceedings(DBLP:conf/vmcai/EssenJ12,
 author       = "Christian von Essen and Barbara Jobstmann",
 year         = "2012",
 title        = "Synthesizing Efficient Controllers",
 editor       = "Viktor Kuncak and Andrey Rybalchenko",
 booktitle    = "VMCAI",
 series       = "Lecture Notes in Computer Science",
 volume       = "7148",
 publisher    = "Springer",
 pages        = "428--444",
 doi          = "10.1007/978-3-642-27940-9\_28",
)
@book(filar1996competitive,
 author       = "Jerzy Filar and Koos Vrieze",
 year         = "1997",
 title        = "Competitive Markov decision processes",
 publisher    = "Springer",
)
@article(DBLP:journals/fmsd/FiliotJR11,
 author       = "Emmanuel Filiot and Naiyong Jin and Jean-Fran\c {c}ois Raskin",
 year         = "2011",
 title        = "Antichains and compositional algorithms for {LTL} synthesis",
 journal      = "Formal Methods in System Design",
 volume       = "39",
 number       = "3",
 pages        = "261--296",
 doi          = "10.1007/s10703-011-0115-3",
)
@article(DBLP:journals/tcs/FinkelS01,
 author       = "Alain Finkel and Ph. Schnoebelen",
 year         = "2001",
 title        = "Well-structured transition systems everywhere!",
 journal      = "Theor. Comput. Sci.",
 volume       = "256",
 number       = "1-2",
 pages        = "63--92",
 doi          = "10.1016/S0304-3975(00)00102-X",
)
@article(DBLP:journals/fac/HanssonJ94,
 author       = "Hans Hansson and Bengt Jonsson",
 year         = "1994",
 title        = "A Logic for Reasoning about Time and Reliability",
 journal      = "Formal Asp. Comput.",
 volume       = "6",
 number       = "5",
 pages        = "512--535",
 doi          = "10.1007/BF01211866",
)
@inproceedings(DBLP:conf/fdl/Hartmanns12,
 author       = "Arnd Hartmanns",
 year         = "2012",
 title        = "MODEST - A unified language for quantitative models",
 booktitle    = "FDL",
 publisher    = "IEEE",
 pages        = "44--51",
)
@book(howard1960dynamic,
 author       = "Ronald A Howard",
 year         = "1960",
 title        = "Dynamic Programming and Markov Processes",
 publisher    = "John Wiley and Sons",
)
@inproceedings(DBLP:conf/hvc/JansenKOSZ07,
 author       = "David N. Jansen and Joost-Pieter Katoen and Marcel Oldenkamp and Mari{\"e}lle Stoelinga and Ivan S. Zapreev",
 year         = "2007",
 title        = "How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison",
 editor       = "Karen Yorav",
 booktitle    = "Haifa Verification Conference",
 series       = "Lecture Notes in Computer Science",
 volume       = "4899",
 publisher    = "Springer",
 pages        = "69--85",
 doi          = "10.1007/978-3-540-77966-7\_9",
)
@article(DBLP:journals/pe/KatoenZHHJ11,
 author       = "Joost-Pieter Katoen and Ivan S. Zapreev and Ernst Moritz Hahn and Holger Hermanns and David N. Jansen",
 year         = "2011",
 title        = "The ins and outs of the probabilistic model checker {MRMC}",
 journal      = "Perform. Eval.",
 volume       = "68",
 number       = "2",
 pages        = "90--104",
 doi          = "10.1016/j.peva.2010.04.001",
)
@book(kemeny1960jl,
 author       = "John G Kemeny and J. L. Snell",
 year         = "1960",
 title        = "Finite Markov Chains",
 publisher    = "Van Nostrand Company, Inc",
)
@inproceedings(KNP11,
 author       = "M. Kwiatkowska and G. Norman and D. Parker",
 year         = "2011",
 title        = "{PRISM} 4.0: Verification of Probabilistic Real-time Systems",
 editor       = "G. Gopalakrishnan and S. Qadeer",
 booktitle    = "Proc. 23rd International Conference on Computer Aided Verification (CAV'11)",
 series       = "LNCS",
 volume       = "6806",
 publisher    = "Springer",
 pages        = "585--591",
 doi          = "10.1007/978-3-642-22110-1\_47",
)
@article(DBLP:journals/iandc/LarsenS91,
 author       = "Kim Guldstrand Larsen and Arne Skou",
 year         = "1991",
 title        = "Bisimulation through Probabilistic Testing",
 journal      = "Inf. Comput.",
 volume       = "94",
 number       = "1",
 pages        = "1--28",
 doi          = "10.1016/0890-5401(91)90030-6",
)
@inproceedings(DBLP:conf/aips/MajercikL98,
 author       = "Stephen M. Majercik and Michael L. Littman",
 year         = "1998",
 title        = "MAXPLAN: A New Approach to Probabilistic Planning",
 editor       = "Reid G. Simmons and Manuela M. Veloso and Stephen F. Smith",
 booktitle    = "AIPS",
 publisher    = "AAAI",
 pages        = "86--93",
)
@misc(Parker,
 author       = "David Parker",
 year         = "2013-11-20",
 howpublished = "personal communication",
)
@misc(prismwebsite,
 author       = "{PRISM Model Checker - Frequently asked questions}",
 howpublished = "\url {http://www.prismmodelchecker.org/} \url {manual/FrequentlyAskedQuestions/PRISMModelling}",
 note         = "Accessed: 2014-06-20",
)
@book(putermanMDP,
 author       = "Martin L. Puterman",
 year         = "1994",
 title        = "Markov Decision Processes: Discrete Stochastic Dynamic Programming",
 publisher    = "John Wiley and Sons",
 doi          = "10.1002/9780470316887",
)
@book(russell1995artificial,
 author       = "Stuart J. Russell and Peter Norvig",
 year         = "1995",
 title        = "Artificial intelligence: a modern approach",
 publisher    = "Prentice hall Englewood Cliffs",
)
@article(veinott1966finding,
 author       = "Arthur F Veinott",
 year         = "1966",
 title        = "On finding optimal policies in discrete dynamic programming with no discounting",
 journal      = "The Annals of Mathematical Statistics",
 volume       = "37",
 number       = "5",
 pages        = "1284--1294",
 doi          = "10.1214/aoms/1177699272",
)
@misc(prismEMP,
 author       = "Christian Von Essen",
 year         = "2013-11-20",
 howpublished = "personal communication",
)
@inproceedings(DBLP:conf/qest/WimmerBBHCHDT10,
 author       = "Ralf Wimmer and Bettina Braitling and Bernd Becker and Ernst Moritz Hahn and Pepijn Crouzen and Holger Hermanns and Abhishek Dhama and Oliver E. Theel",
 year         = "2010",
 title        = "Symblicit Calculation of Long-Run Averages for Concurrent Probabilistic Systems",
 booktitle    = "QEST",
 publisher    = "IEEE Computer Society",
 pages        = "27--36",
 doi          = "10.1109/QEST.2010.12",
)
@inproceedings(DBLP:conf/cav/WulfDHR06,
 author       = "Martin De Wulf and Laurent Doyen and Thomas A. Henzinger and Jean-Fran\c {c}ois Raskin",
 year         = "2006",
 title        = "Antichains: A New Algorithm for Checking Universality of Finite Automata",
 editor       = "Thomas Ball and Robert B. Jones",
 booktitle    = "CAV",
 series       = "Lecture Notes in Computer Science",
 volume       = "4144",
 publisher    = "Springer",
 pages        = "17--30",
 doi          = "10.1007/11817963\_5",
)