www.prismmodelchecker.org

Main /

References

  • AD94: R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126:183-235, 1994.
  • AH99 R. Alur and T. Henzinger. Reactive modules. Formal Methods in System Design, 15(1):7-48, 1999.
  • ASSB96: A. Aziz, K. Sanwal, V. Singhal, and R. Brayton. Verifying continuous time Markov chains. In R. Alur and T. Henzinger, editors, Proc. 8th International Conference on Computer Aided Verification (CAV'96), volume 1102 of LNCS, pages 269-276. Springer, 1996.
  • Bai98: C. Baier. On algorithmic verification methods for probabilistic systems, 1998. Habilitation thesis, Fakultät für Mathematik & Informatik, Universität Mannheim.
  • BKLPW17: Christel Baier, Joachim Klein, Linda Leuschner, David Parker and Sascha Wunderlich. Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes. In Proc. 28th International Conference on Computer Aided Verification (CAV'17), volume 10426 of LNCS, pages 160-180, Springer, 2017.
  • BKH99: C. Baier, J.-P. Katoen, and H. Hermanns. Approximate symbolic model checking of continuous-time Markov chains. In J. Baeten and S. Mauw, editors, Proc. 10th International Conference on Concurrency Theory (CONCUR'99), volume 1664 of LNCS, pages 146-161. Springer, 1999.
  • BK98: C. Baier and M. Kwiatkowska. Model checking for a probabilistic branching time logic with fairness. Distributed Computing, 11(3):125-155, 1998.
  • BdA95: A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. In P. Thiagarajan, editor, Proc. 15th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'95), volume 1026 of LNCS, pages 499-513. Springer, 1995.
  • CHH+13: Taolue Chen, Ernst Moritz Hahn, Tingting Han, Marta Kwiatkowska, Hongyang Qu, and Lijun Zhang. Model repair for Markov decision processes. In Proc. 7th International Symposium on Theoretical Aspects of Software Engineering (TASE'13), pages 85-92. IEEE, 2013.
  • CE81: E. Clarke and A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. Workshop on Logic of Programs, volume 131 of LNCS. Springer, 1981.
  • DHK13: F. Dannenberg, E. M. Hahn, and M. Kwiatkowska. Computing cumulative rewards using fast adaptive uniformisation. In A. Gupta and T. Henzinger, editors, Proc. 11th Conference on Computational Methods in Systems Biology (CMSB'13), volume 8130 of LNCS, pages 33-49. Springer, 2013.
  • FKNP11: V. Forejt, M. Kwiatkowska, G. Norman, and D. Parker. Automated verification techniques for probabilistic systems. In M. Bernardo and V. Issarny, editors, Formal Methods for Eternal Networked Software Systems (SFM'11), volume 6659 of LNCS, pages 53-113. Springer, 2011.
  • FKN+11: V. Forejt, M. Kwiatkowska, G. Norman, D. Parker, and H. Qu. Quantitative multi-objective verification for probabilistic systems. In P. Abdulla and K. Leino, editors, Proc. 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'11), volume 6605 of LNCS, pages 112-127. Springer, 2011.
  • FKP12: V. Forejt, M. Kwiatkowska, and D. Parker. Pareto curves for probabilistic model checking. In S. Chakraborty and M. Mukund, editors, Proc. 10th International Symposium on Automated Technology for Verification and Analysis (ATVA'12), volume 7561 of LNCS, pages 317-332. Springer, 2012.
  • HM14: S. Haddad and B. Monmege. Reachability in MDPs: Refining convergence of value iteration. In 8th International Workshop on Reachability Problems (RP), volume 8762 of LNCS, pages 125–137, Springer. 2014.
  • HHZ11b: E. M. Hahn, H. Hermanns, and L. Zhang. Probabilistic reachability for parametric Markov models. International Journal on Software Tools for Technology Transfer (STTT), 13(1):3-19, 2011.
  • HHZ11: Ernst Moritz Hahn, Tingting Han, and Lijun Zhang. Synthesis for PCTL in parametric Markov decision processes. In Proc. 3rd NASA Formal Methods Symposium (NFM'11), volume 6617 of LNCS. Springer, 2011.
  • HJ94: H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6(5):512-535, 1994.
  • HLMP04: T. Hérault, R. Lassaigne, F. Magniette, and S. Peyronnet. Approximate probabilistic model checking. In Proc. 5th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'04), volume 2937 of LNCS, pages 307-329. Springer, 2004.
  • Hil96: J. Hillston. A Compositional Approach to Performance Modelling. Cambridge University Press, 1996.
  • KSK76: J. Kemeny, J. Snell, and A. Knapp. Denumerable Markov Chains. Springer-Verlag, 2nd edition, 1976.
  • KNP04b: M. Kwiatkowska, G. Norman, and D. Parker. Probabilistic symbolic model checking with PRISM: A hybrid approach. International Journal on Software Tools for Technology Transfer (STTT), 6(2):128-142, 2004.
  • KNP07a: M. Kwiatkowska, G. Norman, and D. Parker. Stochastic model checking. In M. Bernardo and J. Hillston, editors, Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM'07), volume 4486 of LNCS (Tutorial Volume), pages 220-270. Springer, 2007.
  • KNP09c: M. Kwiatkowska, G. Norman, and D. Parker. Stochastic games for verification of probabilistic timed automata. In J. Ouaknine and F. Vaandrager, editors, Proc. 7th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'09), volume 5813 of LNCS, pages 212-227. Springer, 2009.
  • KNPS06: M. Kwiatkowska, G. Norman, D. Parker, and J. Sproston. Performance analysis of probabilistic timed automata using digital clocks. Formal Methods in System Design, 29:33-78, 2006.
  • KNSW07: M. Kwiatkowska, G. Norman, J. Sproston, and F. Wang. Symbolic model checking for probabilistic timed automata. Information and Computation, 205(7):1027-1077, 2007.
  • MWDH10: F. Didier M. Mateescu, V. Wolf and T. Henzinger. Fast adaptive uniformisation of the chemical master equation. IET Syst Biol, 4(6):441-452, 2010.
  • Nim10: V. Nimal. Statistical Approaches for Probabilistic Model Checking. MSc Mini-project Dissertation, Oxford University Computing Laboratory, 2010.
  • NPS13: Gethin Norman, David Parker, and Jeremy Sproston. Model checking for probabilistic timed automata. Formal Methods in System Design, 43(2):164-190, 2013.
  • NPZ17: Gethin Norman, David Parker and Xueyi Zou. Verification and Control of Partially Observable Probabilistic Systems. Real-Time Systems, 53(3):354-402, Springer, 2017.
  • Par02: D. Parker. Implementation of Symbolic Model Checking for Probabilistic Systems. Ph.D. thesis, University of Birmingham, 2002.
  • Put94: M. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley and Sons, 1994.
  • Seg95: R. Segala. Modelling and Verification of Randomized Distributed Real Time Systems. Ph.D. thesis, Massachusetts Institute of Technology, 1995.
  • Ste94: W. Stewart. Introduction to the Numerical Solution of Markov Chains. Princeton, 1994.
  • YS02: H. Younes and R. Simmons. Probabilistic verification of discrete event systems using acceptance sampling. In E. Brinksma and K. Larsen, editors, Proc. 14th International Conference on Computer Aided Verification (CAV'02), volume 2404 of LNCS, pages 223-235. Springer, 2002.

PRISM Manual

[ View all ]