Presentation

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