References

  1. 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.
  2. Christel Baier & Joost-Pieter Katoen (2008): Principles of model checking. MIT Press.
  3. 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.
  4. D. P. Bertsekas & J.N. Tsitsiklis (1996): Neuro-Dynamic Programming. Anthropological Field Studies. Athena Scientific.
  5. 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.
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. 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.
  11. 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.
  12. Peter Buchholz (1994): Exact and ordinary lumpability in finite Markov chains. Journal of applied probability, pp. 59–75, doi:10.2307/3215235.
  13. 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.
  14. 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.
  15. 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.
  16. 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.
  17. 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.
  18. 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.
  19. 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.
  20. Jerzy Filar & Koos Vrieze (1997): Competitive Markov decision processes. Springer.
  21. 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.
  22. 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.
  23. 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.
  24. Arnd Hartmanns (2012): MODEST - A unified language for quantitative models. In: FDL. IEEE, pp. 44–51.
  25. Ronald A Howard (1960): Dynamic Programming and Markov Processes. John Wiley and Sons.
  26. 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.
  27. 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.
  28. John G Kemeny & J. L. Snell (1960): Finite Markov Chains. Van Nostrand Company, Inc.
  29. 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.
  30. 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.
  31. 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.
  32. David Parker (2013-11-20). personal communication.
  33. PRISM Model Checker - Frequently asked questions. http://www.prismmodelchecker.org/ manual/FrequentlyAskedQuestions/PRISMModelling. Accessed: 2014-06-20.
  34. Martin L. Puterman (1994): Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley and Sons, doi:10.1002/9780470316887.
  35. Stuart J. Russell & Peter Norvig (1995): Artificial intelligence: a modern approach. Prentice hall Englewood Cliffs.
  36. 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.
  37. Christian Von Essen (2013-11-20). personal communication.
  38. 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.
  39. 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.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org