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