How Fast and Fat Is Your Probabilistic Model Checker? an experimental performance comparison David N. Jansen3,1, Joost-Pieter Katoen1,2, Marcel Oldenkamp2, Mariëlle Stoelinga2, Ivan Zapreev1,2 MOVES Group, RWTH Aachen University 2 FMT Group, University of Twente, Enschede 3 ICIS, Radboud University, Nijmegen 1 Probabilistic Model Checking Probabilistic System Probabilistic Requirement PRISM PRISM MRMC (hybrid) (sparse) VESTA Probabilistic Model Probabilistic Formula ETMCC YMER Probabilistic Model Checker Yes No Probability Why Are Probabilities Useful? • • • • system performance uncertainty in the environment randomized (networking) algorithms abstract from large populations Probabilistic Model Checking... • What is inside? – temporal logics + model checking – numerical and optimisation techniques from performance and operations research • Where is it used? – powerful tools – applications: distributed systems, security, biology, quantum computing... • Problem: Which tool to choose? Probabilistic Models Probabilistic System Probabilistic Requirement Discrete time Markov chains Probabilistic Model Yes Probabilistic Formula Continuous time Markov chains Probabilistic automata Model Checker transitions are probabilistic timing for CTMC: No Prob(wait time t) = 1 – e– t Probability Synchronous Leader Election • nodes in a ring elect a leader – each node selects random number as id – passes it around the ring (synchronously) – if unique id, node with maximum unique id is leader • [Itai & Rodeh 1990] Synchronous Leader Election 1 4 2 2 5 3 1 5 Synchronous Leader Election 2 5 4 1 1 1 5 4 4 4 1 2 1 5 2 5 1 2 3 5 1 3 2 3 5 2 3 5 1 Models • Discrete time Markov chain – transitions are fully probabilistic – timing is irrelevant • Continuous time Markov chain – transitions are fully probabilistic – and timing also: Prob(wait time t) = 1 – e– t Probabilistic Formulas Probabilistic System Probabilistic Requirement Reachability Probabilistic Model Bounded Reachability Probabilistic Formula Probabilistic Steady-State Property Model Checker extensions of CTL Yes Probability No Probabilistic Model Checkers e d a m s Probabilistic System Probabilistic Requirement e c i o Ch s e l p m a x e e e r h n T o i t a Probabilistic Model ll evalu Probabilistic Formula a r e v O Probabilistic Model Checker Yes No Probability Tools numerical statist ETMC C MRMC PRISM hybrid PRISM sparse VESTA YMER CTMC DTMC + CTMC DTMC + CTMC MTBDD for transition matrix DTMC + CTMC sparse transition matrix CTMC, reachability CTMC, bounded reach Java C C(++ ) and Java Java C(++ ) Modelling informal description PRISM model .tra format model ETMCC MRMC adapt syntax VESTA model YMER model PRISM YMER VESTA Selected Benchmarks Synchronous Leader Election discrete time Randomized Dining Philosophers discrete time Birth–Death Process discrete time Tandem Queuing Network continuous time Cyclic Server Polling continuous time Experiment Relevance • • • • Repeatable Verifiable Significant Encapsulated Experiment 1 Reachability • Cyclic Polling Server: server cycles over n stations and serves each one in turn – e.g. teacher walks through class, each pupil may ask a question • busy1 P 1(true U poll1) If station 1 is busy, the server will poll it eventually 10000 1000 100 10 1 0,1 0,01 0,001 0,0001 0,00001 3 6 10000000 9 12 15 18 number of stations n 1000000 mrmc prism hybrid prism sparse etmcc ymer vesta 100000 10000 1000 100 10 1 3 6 9 12 15 18 number of stations n Analysis ETMCC slow, out of memory PRISM only symbolic MRMC fastest tool for small models VESTA excessive number of samples, slow YMER not implemented sparse=hybrid PRISM: MTBDD Size • Multi-Terminal BDD = data structure for transition matrix • size heavily depends on model • large MTBDD slow Model # states # MTBDD nodes Synchronous 500.000 1.000.000 . leader election Cyclic polling 7.000.000 < 3.000 . CPS versus SLE runtime 100000 10000 10000 1000 1000 100 100 10 10 1 1 0,1 0,1 0,01 0,01 0,001 0,001 0,0001 0,0001 4_4 ,00001 3 6 9 12 15 18 number of stations n 7.077.888 states 2.745 MTBDD nodes 4_8 4_12 4_16 8_2 8_4 number of processes_random set size n_k mrmc prism hybrid prism sparse etmcc ymer vesta 458.847 states 1.131.806 MTBDD nodes VESTA: simulation problem • • • • actual probability close to bound P p(...) estimate is almost always in [p– ,p+ ] some irregularity stops the simulation 0.95 Prob(yes actual Prob p) Prob(actual Prob p yes) Result Overview: Timing ETMCC MRMC PRISM PRISM VESTA YMER hybrid sparse unb’nded U – + +/++ +/++ depends heavily on MTBDD size –/0 N/A Result Overview: Memory ETMCC MRMC PRISM PRISM VESTA YMER hybrid sparse unb’nded U – + +/++ +/++ 0/+ N/A MTBDD size almost independent varies heavily from model size Experiment 2 Bounded Reachability • Tandem Queueing Network – two queues after each other checkin counter • security check P<0.01(true U 2 full ) Is the probability that the system gets full in 2 time units small? 10000 1000 100 10 1 0,1 0,01 0,001 0,0001 0,00001 10 10000000 50 100 255 511 1023 queue size n 1000000 100000 mrmc prism hybrid prism sparse etmcc ymer vesta 10000 1000 100 10 1 10 50 100 255 511 1023 queue size n Analysis ETMCC slow, out of memory PRISM sparse=faster, hybrid=smaller MRMC fast for small models VESTA YMER ok if you can afford statistical errors best choice if you can afford statistical errors Result Overview: Timing ETMCC MRMC PRISM PRISM VESTA YMER hybrid sparse unb’nded U bounded U – – + + +/++ +/++ 0/+ +/++ –/0 + N/A ++ Result Overview: Memory ETMCC MRMC PRISM PRISM VESTA YMER hybrid sparse unb’nded U bounded U – – + + +/++ +/++ +/++ + 0/+ + N/A ++ Experiment 3 Steady State Property • Tandem Queuing Network • (X 2nd 2nd queue queue full full)) ) S>0.2( PP>0.1 >0.1(X In equilibrium, the probability to satisfy P>0.1(X ... ) is > 0.2 10000 1000 100 10 1 0,1 0,01 0,001 0,0001 0,00001 10 10000000 50 100 255 511 1023 queue size n 1000000 100000 mrmc prism hybrid prism sparse etmcc ymer vesta 10000 1000 100 10 1 10 50 100 255 511 1023 queue size n Analysis ETMCC slow, out of memory PRISM sparse=faster hybrid=slightly smaller MRMC fastest VESTA not implemented YMER not implemented Simulating Steady State? • simulation of bounded reachability has clear stopping criterion • simulation of unbounded reachability reachability with very large bound • simulation of steady state? never stops Result Overview: Timing ETMCC MRMC PRISM PRISM VESTA YMER hybrid sparse unb’nded U bounded U steady state – – – + + ++ +/++ +/++ 0/+ +/++ 0/+ + –/0 + N/A N/A N/A ++ Result Overview: Memory ETMCC MRMC PRISM PRISM VESTA YMER hybrid sparse unb’nded U bounded U steady state – – – + + + +/++ +/++ +/++ + +/++ + 0/+ + N/A N/A N/A ++ Nested Formulas • we also checked nested properties P 0.8(P 0.9(true U • not detailed here 100 n70) U n50) Result Overview: Timing ETMCC MRMC PRISM PRISM VESTA YMER hybrid sparse unb’nded U bounded U steady state nested – – – – + + ++ ++ +/++ +/++ 0/+ +/++ 0/+ + 0/+ + –/0 + N/A N/A N/A –– N/A ++ based on a single property only: did not terminate Result Overview: Memory ETMCC MRMC PRISM PRISM VESTA YMER hybrid sparse unb’nded U bounded U steady state nested – – – – + + + + +/++ +/++ +/++ + +/++ + +/++ + 0/+ + N/A N/A N/A N/A N/A ++ Conclusions ETMCC MRMC PRISM hybrid PRISM sparse VESTA YMER worst, only small models fastest for small models fast if MTBDD is small fast rather slow, statistical errors slim & very fast, only bounded reach, few statistical errors