Probabilistic symbolic model checking with PRISM: a hybrid approach

PRISM web site. www.cs.bham.ac.uk/∼dxp/prism

Alur R, Henzinger T (1996) Reactive modules. In: Proceedings of the 11th annual IEEE symposium on logic in computer science (LICS’96), New Brunswick, NJ, July 1996. IEEE Press, New York, pp 207–218

Aspnes J, Herlihy M (1990) Fast randomized consensus using shared memory. J Algorithms 15(1):441–460

Aziz A, Sanwal K, Singhal V, Brayton R (1996) Verifying continuous time Markov chains. In: Alur R, Henzinger T (eds) Proceedings of the 8th international conference on computer aided verification (CAV’96), New Brunswick, NJ, July–August 1996. Lecture notes in computer science, vol 1102. Springer, Berlin Heidelberg New York, pp 269–276

Bahar I, Frohm E, Gaona C, Hachtel G, Macii E, Pardo A, Somenzi F (1993) Algebraic decision diagrams and their applications. In: Proceedings of the international conference on computer-aided design (ICCAD’93), Santa Clara, CA, November 1993, pp 188–191. Also available in: (1997) Formal Meth Sys Des 10(2/3):171–206

Baier C (1998) On algorithmic verification methods for probabilistic systems. Habilitation thesis, Fakultät für Mathematik & Informatik, Universität Mannheim, Mannheim, Germany

Baier C, Clarke E, Hartonas-Garmhausen V, Kwiatkowska M, Ryan M (1997) Symbolic model checking for probabilistic processes. In: Degano P, Gorrieri R, Marchetti-Spaccamela A (eds) Proceedings of the 24th international colloquium on automata, languages and programming (ICALP’97), Bologna, Italy, July 1997. Lecture notes in computer science, vol 1256. Springer, Berlin Heidelberg New York, pp 430–440

Baier C, Haverkort B, Hermanns H, Katoen J-P (2000) Model checking continuous-time Markov chains by transient analysis. In: Emerson A, Sistla A (eds) Proceedings of the 12th international conference on computer aided verification (CAV’00), Chicago, July 2000. Lecture notes in computer science, vol 1855. Springer, Berlin Heidelberg New York, pp 358–372

Baier C, Katoen J-P, Hermanns H (1999) Approximate symbolic model checking of continuous-time Markov chains. In: Baeten J, Mauw S (eds) Proceedings of the 10th international conference on concurrency theory (CONCUR’99), Eindhoven, The Netherlands, August 1999. Lecture notes in computer science, vol 1664. Springer, Berlin Heidelberg New York, pp 146–161

Baier C, Kwiatkowska M (1998) Model checking for a probabilistic branching time logic with fairness. Distrib Comput 11(3):125–155

Bause F, Buchholz P, Kemper P (1998) A toolbox for functional and quantitative analysis of DEDS. In: Puigjaner R, Savino N, Serra B (eds) Proceedings of Computer Performance Evaluation (TOOLS’98), Palma de Mallorca, Spain, September 1998. Lecture notes in computer science, vol 1469. Springer, Berlin Heidelberg New York, pp 356–359

Bianco A, de Alfaro L (1995) Model checking of probabilistic and nondeterministic systems. In: Thiagarajan P (ed) Proceedings of the 15th conference on foundations of software technology and theoretical computer science, Bangalore, India, December 1995. Lecture notes in computer science, vol 1026. Springer, Berlin Heidelberg New York, pp 499–513

Bollig B, Wegner I (1996) Improving the variable ordering of OBDDs is NP-complete. IEEE Trans Comput 45(9):993–1006

Bozga M, Maler O (1999) On the representation of probabilities over structured domains. In: Halbwachs N, Peled D (eds) Proceedings of the 11th international conference on computer aided verification (CAV’99), Trento, Italy, July 1999. Lecture notes in computer science, vol 1633. Springer, Berlin Heidelberg New York, pp 261–273

Bryant R (1986) Graph-based algorithms for Boolean function manipulation. IEEE Trans Comput C-35(8):677–691

Buchholz P, Ciardo G, Donatelli S, Kemper P (1997) Complexity of Kronecker operations on sparse matrices with applications to the solution of Markov models. ICASE Report 97-66, Institute for Computer Applications in Science and Engineering, Hampton, VA

Buchholz P, Kemper P (2001) Compact representations of probability distributions in the analysis of superposed GSPNs. In: German R, Haverkort B (eds) Proceedings of the 9th international workshop on Petri nets and performance models (PNPM’01). IEEE Press, New York, pp 81–90

Burch J, Clarke E, McMillan K, Dill D, Hwang J (1990) Symbolic model checking: 1020 states and beyond. In: Proceedings of the 5th annual IEEE symposium on logic in computer science (LICS’90). IEEE Press, New York, pp 428–439

Chiola G, Franceschinis G, Gaeta R, Ribaudo M (1995) GreatSPN 1.7: Graphical editor and analyzer for timed and stochastic Petri nets Perform Eval 24(1–2):47–68

Ciardo G, Miner A (1996) SMART: simulation and Markovian analyser for reliability and timing. In: Proceedings of the 2nd international computer performance and dependability symposium (IPDS’96). IEEE Press, New York, p 60

Ciardo G, Miner A (1999) A data structure for the efficient Kronecker solution of GSPNs. In: Buchholz P, Silva M (eds) Proceedings of the 8th international workshop on Petri nets and performance models (PNPM’99). IEEE Press, New York, pp 22–31

Ciardo G, Tilgner M (1996) On the use of Kronecker operators for the solution of generalized stocastic Petri nets. ICASE Report 96-35, Institute for Computer Applications in Science and Engineering, Hampton, VA

Clarke E, Fujita M, McGeer P, McMillan K, Yang J, Zhao X (1993) Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. In: Proceedings of the international workshop on logic synthesis (IWLS’93), Tahoe City, CA, May 1993, pp 1–15. Also available in: (1997) Formal Meth Sys Des 10(2/3):149–169

Clarke E, McMillan K, Zhao X, Fujita M, Yang J (1993) Spectral transforms for large Boolean functions with applications to technology mapping. In: Proceedings of the 30th design automation conference (DAC’93). ACM Press, New York, pp 54–60. Also available in: (1997) Formal Meth Sys Des 10(2/3):137–148

Daly D, Deavours D, Doyle J, Webster P, Sanders W (2000) Möbius: An extensible tool for performance and dependability modeling. In: Haverkort B, Bohnenkamp H, Smith C (eds) Proceedings of the 11th international conference on modelling techniques and tools for computer performance evaluation (TOOLS’00), Schaumburg, IL, March 2000. Lecture notes in computer science, vol 1786. Springer, Berlin Heidelberg New York, pp 332–336

D’Argenio P, Jeannet B, Jensen H, Larsen K (2001) Reachability analysis of probabilistic systems by successive refinements. In: De Alfaro L, Gilmore S (eds) Proceedings of the 1st joint international workshop on process algebra and probabilistic methods, performance modeling and verification (PAPM/PROBMIV’01), Aachen, Germany, September 2001. Lecture notes in computer science, vol 2165. Springer, Berlin Heidelberg New York, pp 39–56

De Alfaro L (1997) Formal verification of probabilistic systems. PhD thesis, Stanford University, Stanford, CA

De Alfaro L (1997) Temporal logics for the specification of performance and reliability. In: Reischuk R, Morvan M (eds) Proceedings of the symposium on theoretical aspects of computer science (STACS’97), Lübeck, Germany, February–March 1997. Lecture notes in computer science, vol 1200. Springer, Berlin Heidelberg New York, pp 165–176

De Alfaro L (1998) How to specify and verify the long-run average behavior of probabilistic systems. In: Proceedings of the 13th annual IEEE symposium on logic in computer science (LICS’98), Indianapolis, IN, June 1998, pp 454–465

De Alfaro L (1999) Computing minimum and maximum reachability times in probabilistic systems. In: Baeten J, Mauw S (eds) Proceedings of the 10th international conference on concurrency theory (CONCUR’99), Eindhoven, The Netherlands, August 1999. Lecture notes in computer science, vol 1664. Springer, Berlin Heidelberg New York, pp 66–81

De Alfaro L, Kwiatkowska M, Norman G, Parker D, Segala R (2000) Symbolic model checking of concurrent probabilistic processes using MTBDDs and the Kronecker representation. In: Graf S, Schwartzbach M (eds) Proceedings of the 6th international conference on tools and algorithms for the construction and analysis of systems (TACAS’00), Berlin, March–April 2000. Lecture notes in computer science, vol 1785. Springer, Berlin Heidelberg New York, pp 395–410

Deavours D, Sanders W (1997) An efficient disk-based tool for solving very large Markov models. In: Marie R, Plateau B, Calzarossa M, Rubino G (eds) Proceedings of the 9th international conference on modelling techniques and tools (TOOLS’97), St Malo, France, June 1997. Lecture notes in computer science, vol 1245. Springer, Berlin Heidelberg New York, pp 58–71

Deavours D, Sanders W (1998) “On-the-fly” solution techniques for stochastic Petri nets and extensions. IEEE Trans Softw Eng 24(10):889–902

Gilmore S, Hillston J (1994) The PEPA workbench: a tool to support a process algebra-based approach to performance modelling. In: Haring G, Kotsis G (eds) Proceedings of the 7th international conference on modelling techniques and tools for computer performance evaluation, Vienna, May 1994. Lecture notes in computer science, vol 794. Springer, Berlin Heidelberg New York, pp 353–368

Hachtel G, Macii E, Pardo A, Somenzi F (1994) Probabilistic analysis of large finite state machines. In: Proceedings of the 31st design automation conference (DAC’94). ACM Press, New York, pp 270–275

Hachtel G, Macii E, Pardo A, Somenzi F (1996) Markovian analysis of large finite state machines. IEEE Trans CAD 15(12):1479–1493

Hansson H, Jonsson B (1994) A logic for reasoning about time and probability. Formal Aspects Comput 6(5):512–535

Hartonas-Garmhausen V, Campos S, Clarke E (1999) ProbVerus: probabilistic symbolic model checking. In: Katoen J-P (ed) Proceedings of the 5th international AMAST workshop on real-time and probabilistic systems (ARTS’99), Bamburg, Germany, May 1999. Lecture notes in computer science, vol 1601. Springer, Berlin Heidelberg New York, pp 96–110

Herman T (1990) Probabilistic self-stabilization. Inf Process Lett 35(2):63–67

Hermanns H, Herzog U, Klehmet U, Mertsiotakis V, Siegle M (2000) Compositional performance modelling with the TIPPtool. Perform Eval 39(1–4):5–35

Hermanns H, Katoen J-P, Meyer-Kayser J, Siegle M (2000) A Markov chain model checker. In: Graf S, Schwartzbach M (eds) Proceedings of the 6th international conference on tools and algorithms for the construction and analysis of systems (TACAS’00), Berlin, March–April 2000. Lecture notes in computer science, vol 1785. Springer, Berlin Heidelberg New York, pp 347–362

Hermanns H, Kwiatkowska M, Norman G, Parker D, Siegle M (2003) On the use of MTBDDs for performability analysis and verification of stochastic systems. J Logic Algebr Programm 56(1–2):23–67

Hermanns H, Meyer-Kayser J, Siegle M (1999) Multi terminal binary decision diagrams to represent and analyse continuous time Markov chains. In: Plateau B, Stewart W, Silva M (eds) Proceedings of the 3rd international workshop on numerical solution of Markov chains (NSMC’99), Prensas Universitarias de Zaragoza, Spain, September, pp 188–207

Ibe O, Trivedi K (1990) Stochastic Petri net models of polling systems. IEEE J Select Areas Commun 8(9):1649–1657

Itai A, Rodeh M (1990) Symmetry breaking in distributed networks. Inf Comput 88(1):60–87

Katoen J-P, Kwiatkowska M, Norman G, Parker D (2001) Faster and symbolic CTMC model checking. In: de Alfaro L, Gilmore S (eds) Proceedings of the 1st joint international workshop on process algebra and probabilistic methods, performance modeling and verification (PAPM/PROBMIV’01), Aachen, Germany, September 2001. Lecture notes in computer science, vol 2165. Springer, Berlin Heidelberg New York, pp 23–38

Knottenbelt W, Harrison P (1999) Distributed disk-based solution techniques for large Markov models. In: Plateau B, Stewart W, Silva M (eds) Proceedings of the 3rd international workshop on numerical solution of Markov chains (NSMC’99), Prensas Universitarias de Zaragoza, Spain, September 1999, pp 58–75

Kuntz M, Siegle M (2002) Deriving symbolic representations from stochastic process algebras. In: Hermanns H, Segala R (eds) Proceedings of the 2nd joint international workshop on process algebra and probabilistic methods, performance modeling and verification (PAPM/PROBMIV’02), Copenhagen, July 2002. Lecture notes in computer science, vol 2399. Springer, Berlin Heidelberg New York, pp 188–206

Kwiatkowska M, Mehmood R (2002) Out-of-core solution of large linear systems of equations arising from stochastic modelling. In: Hermanns H, Segala R (eds) Proceedings of the 2nd joint international workshop on process algebra and probabilistic methods, performance modeling and verification (PAPM/PROBMIV’02), Copenhagen, July 2002. Lecture notes in computer science, vol 2399. Springer, Berlin Heidelberg New York, pp 135–151

Kwiatkowska M, Norman G, Parker D, Segala R (1999) Symbolic model checking of concurrent probabilistic systems using MTBDDs and Simplex. Technical Report CSR-99-1, School of Computer Science, University of Birmingham, Birmingham, UK

Kwiatkowska M, Norman G, Segala R (2001) Automated verification of a randomized distributed consensus protocol using Cadence SMV and PRISM. In: Berry G, Comon H, Finkel A (eds) Proceedings of the 13th international conference on computer aided verification (CAV’01), Paris, July 2001. Lecture notes in computer science, vol 2102. Springer, Berlin Heidelberg New York, pp 194–206

Kwiatkowska M, Mehmood R, Norman G, Parker D (2002a) A symbolic out-of-core solution method for Markov models. In: Proceedings of the workshop on parallel and distributed model checking (PDMC’02), Brno, Czech Republic, August 2002. Electronic notes in theoretical computer science, vol 68.4. Elsevier, Amsterdam

Kwiatkowska M, Norman G, Parker D (2002b) PRISM: Probabilistic symbolic model checker. In: Field T, Harrison P, Bradley J, Harder U (eds) Proceedings of the 12th international conference on modelling techniques and tools for computer performance evaluation (TOOLS’02), London, April 2002. Lecture notes in computer science, vol 2324. Springer, Berlin Heidelberg New York, pp 200–204

Kwiatkowska M, Norman G, Sproston J (2003) Probabilistic model checking of deadline properties in the IEEE 1394 FireWire root contention protocol. Formal Aspects Comput 14:295–318

McMillan K (1993) Symbolic model checking. Kluwer, Dordrecht

Miner A (2000) Data structures for the analysis of large structured Markov chains. PhD thesis, Department of Computer Science, College of William & Mary, Williamsburg, VA

Parker D (2002) Implementation of symbolic model checking for probabilistic systems. PhD thesis, University of Birmingham, Birmingham, UK

Plateau B (1985) On the stochastic structure of parallelism and synchronisation models for distributed algorithms. In: Proceedings of the 1985 ACM SIGMETRICS conference on measurement and modeling of computer systems, Austin, TX, August 1985. Perform Eval Rev 13(2):147–153

Sanders W, Obal W, Qureshi M, Widjanarko F (1995) The UltraSAN modeling environment. Perform Eval 24(1):89–115

Somenzi F (1997) CUDD: Colorado University decision diagram package. Public software, Colorado Univeristy, Boulder. http://vlsi.colorado.edu/∼fabio/

Stewart W (1991) MARCA: Markov chain analyser, a software package for Markov modelling. In: Stewart W (eds) Proceedings of NSMC’91, Raleigh, NC, January 1990. Marcel Dekker, New York, pp 37–62

Tani S, Hamaguchi K, Yajima S (1993) The complexity of the optimal variable ordering problems of shared binary decision diagrams. In: Ng K, Raghavan P, Balasubramanian N, Chin F (eds) Proceedings of the 4th international symposium on algorithms and computation (ISAAC’93), Hong Kong, December 1993. Lecture notes in computer science, vol 762. Springer, Berlin Heidelberg New York, pp 389–398

Xie A, Beerel A (1997) Symbolic techniques for performance analysis of timed circuits based on average time separation of events. In: Proceedings of the 3rd international symposium on advanced research in asynchronous circuits and systems (ASYNC’97), Eindhoven, The Netherlands, April 1997. IEEE Press, New York, pp 64–75