Accelerating Parametric Probabilistic Verification Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker Software Modeling and Verification RWTH Aachen University
September 10, 2014
QEST 2014
Nils Jansen - Accelerating Parametric Probabilistic Verification
1 / 34
Contents
1 Motivation 2 Preliminaries 3 Model Checking Algorithm 4 Factorization of Polynomials and Implementation 5 Conclusion and Future Work
Nils Jansen - Accelerating Parametric Probabilistic Verification
2 / 34
Motivation
Discrete-time Markov Chains (DTMCs) model probabilistic behavior of systems can efficiently be verified (PRISM, MRMC)
Nils Jansen - Accelerating Parametric Probabilistic Verification
3 / 34
Motivation
Discrete-time Markov Chains (DTMCs) model probabilistic behavior of systems can efficiently be verified (PRISM, MRMC) Probabilities that are fitting are often difficult or impossible to specify when designing systems can alternatively be left unspecified
Nils Jansen - Accelerating Parametric Probabilistic Verification
3 / 34
Motivation
Discrete-time Markov Chains (DTMCs) model probabilistic behavior of systems can efficiently be verified (PRISM, MRMC) Probabilities that are fitting are often difficult or impossible to specify when designing systems can alternatively be left unspecified Parametric Discrete-time Markov Chains enable greater variability in system modeling can be instantiated in a way such that certain properties are satisfied
Nils Jansen - Accelerating Parametric Probabilistic Verification
3 / 34
Motivation: Dueling Cowboys 0.9
lukeaim
joedead
0.75 1 start
0.4
0.1 1
0.25
joeaim Nils Jansen - Accelerating Parametric Probabilistic Verification
0.6
lukedead 4 / 34
Motivation: Dueling Cowboys
joedead 0.796875
start 0.203125
lukedead Nils Jansen - Accelerating Parametric Probabilistic Verification
4 / 34
Motivation: Parametric Dueling Cowboys Probabilities of missing target as parameters pluke , pjoe ∈ [0, 1] 1 − pluke
lukeaim
joedead
0.75 1 pjoe
start
pluke 1
0.25
joeaim
Nils Jansen - Accelerating Parametric Probabilistic Verification
1 − pjoe
lukedead
5 / 34
Motivation: Parametric Dueling Cowboys Probabilities of missing target as parameters pluke , pjoe ∈ [0, 1] joedead −0.75pluke +0.25pjoe −0.25pluke pjoe +0.75 1−pluke pjoe
start 0.75pluke −0.25pjoe −0.75pluke pjoe +0.25 1−pluke pjoe
lukedead
Nils Jansen - Accelerating Parametric Probabilistic Verification
5 / 34
Motivation: Parametric Dueling Cowboys Probabilities of missing target as parameters pluke , pjoe ∈ [0, 1] joedead −0.75pluke +0.25pjoe −0.25pluke pjoe +0.75 1−pluke pjoe
start 0.75pluke −0.25pjoe −0.75pluke pjoe +0.25 1−pluke pjoe
lukedead
0.75pluke − 0.25pjoe − 0.75pluke pjoe + 0.25 1 2 ≥ 0.75 ⇐⇒ pluke ≥ pjoe + 1 − pluke pjoe 3 3 Nils Jansen - Accelerating Parametric Probabilistic Verification
5 / 34
Related Work Daws (2004) Symbolic model checking for reachability properties on DTMCs Regular expressions capture reachability by means of the sets of all paths leading to certain states State elimination algorithm from automata theory adapted for probabilities
Nils Jansen - Accelerating Parametric Probabilistic Verification
6 / 34
Related Work Daws (2004) Symbolic model checking for reachability properties on DTMCs Regular expressions capture reachability by means of the sets of all paths leading to certain states State elimination algorithm from automata theory adapted for probabilities Hahn, Hermanns, Wachter, Zhang (2009) Based on Daws’ idea Rational functions describe probabilities Tool PARAM Can also handle Markov decision processes
Nils Jansen - Accelerating Parametric Probabilistic Verification
6 / 34
Contents
1 Motivation 2 Preliminaries 3 Model Checking Algorithm 4 Factorization of Polynomials and Implementation 5 Conclusion and Future Work
Nils Jansen - Accelerating Parametric Probabilistic Verification
7 / 34
Rational Function Definition (Rational Function) V = {x1 , ..., xn } finite set of variables with domain R Polynomial g over V : e
e
e
e
g = a1 · x1 1,1 · . . . · xn 1,n + · · · + am · x1 m,1 · . . . · xn m,n where ei,j ∈ N and ai ∈ Z for 1 ≤ i ≤ m and 1 ≤ j ≤ n.
Nils Jansen - Accelerating Parametric Probabilistic Verification
8 / 34
Rational Function Definition (Rational Function) V = {x1 , ..., xn } finite set of variables with domain R Polynomial g over V : e
e
e
e
g = a1 · x1 1,1 · . . . · xn 1,n + · · · + am · x1 m,1 · . . . · xn m,n where ei,j ∈ N and ai ∈ Z for 1 ≤ i ≤ m and 1 ≤ j ≤ n. Rational function f over V : g1 with g2 = 6 0 g2 | g1 , g2 ∈ Z[x1 , ..., xn ] ∧ g2 6= 0 : set of rational functions f =
FV =
g1 g2
Nils Jansen - Accelerating Parametric Probabilistic Verification
8 / 34
Parametric Markov Chain Definition (PDTMC) A Parametric Discrete-time Markov Chain (PDTMC) is a tuple M = (S, V , I , P) with S a set of states V = {x1 , ..., xn } the finite set of parameters with domain R P I : S → FV the initial distribution with s∈S I (s) = 1 P : S × SP→ FV the parametric transition probability matrix with ∀s ∈ S. s 0 ∈S P(s, s 0 ) = 1 0.4 1
2 0.6 1
q
3 1
4
Nils Jansen - Accelerating Parametric Probabilistic Verification
1−q
5
1
9 / 34
For the sake of formalisms... Definition (Evaluation) Evaluation u : V → R g [u] for polynomial g substitutes each x ∈ V by u(x) For rational function f =
g1 g2
∈ FV we define f [u] =
Nils Jansen - Accelerating Parametric Probabilistic Verification
g1 [u] g2 [u]
∈R
10 / 34
For the sake of formalisms... Definition (Evaluation) Evaluation u : V → R g [u] for polynomial g substitutes each x ∈ V by u(x) For rational function f =
g1 g2
∈ FV we define f [u] =
g1 [u] g2 [u]
∈R
Definition (Evaluated PDTMC) An evaluated PDTMC PDTMC M = (S, V , I , P) for evaluation u is the DTMC D = (Su , Iu , Pu ) with Su = S ∀s ∈ Su . Iu (s) = I (s)[u] ∀s ∈ Su . Pu (s, s 0 ) = P(s, s 0 )[u]
Nils Jansen - Accelerating Parametric Probabilistic Verification
10 / 34
For the sake of formalisms...
Definition (Well-defined evaluation) An evaluation u is well-defined for a PDTMC M = (S, V , I , P) if for the evaluated PDTMC D = (Su , Iu , Pu ) it holds that P Iu : Su → [0, 1] with s∈Su Iu (s) = 1 P Pu : Su × Su → [0, 1] with s 0 ∈Su Pu (s, s 0 ) = 1 for all s ∈ Su . An evaluation u is called graph preserving if it is well-defined and it holds that ∀s, s 0 ∈ S : P(s, s 0 ) 6= 0 =⇒ P(s, s 0 )[u] > 0.
Nils Jansen - Accelerating Parametric Probabilistic Verification
11 / 34
Parametric Probabilistic Model Checking Definition Given a PDTMC M = (S, V , I , P) with absorbing states T ⊆ S: Find rational function fsI ,t ∈ FV for each initial state sI ∈ S and each t ∈ T “describing” the reachability probability from sI to t.
Nils Jansen - Accelerating Parametric Probabilistic Verification
12 / 34
Parametric Probabilistic Model Checking Definition Given a PDTMC M = (S, V , I , P) with absorbing states T ⊆ S: Find rational function fsI ,t ∈ FV for each initial state sI ∈ S and each t ∈ T “describing” the reachability probability from sI to t. Intuition: Rational function gives probability of all paths leading from initial states to target states via a graph-preserving evaluation.
pd
sI
pa
s
pb
t
pc
Nils Jansen - Accelerating Parametric Probabilistic Verification
12 / 34
Parametric Probabilistic Model Checking Definition Given a PDTMC M = (S, V , I , P) with absorbing states T ⊆ S: Find rational function fsI ,t ∈ FV for each initial state sI ∈ S and each t ∈ T “describing” the reachability probability from sI to t. Intuition: Rational function gives probability of all paths leading from initial states to target states via a graph-preserving evaluation.
pd
sI
pa
s
pb
t
sI
1 pa 1−p p + pd c b
t
pc
Nils Jansen - Accelerating Parametric Probabilistic Verification
12 / 34
Parametric Probabilistic Model Checking Definition Given a PDTMC M = (S, V , I , P) with absorbing states T ⊆ S: Find rational function fsI ,t ∈ FV for each initial state sI ∈ S and each t ∈ T “describing” the reachability probability from sI to t. Intuition: Rational function gives probability of all paths leading from initial states to target states via a graph-preserving evaluation.
0.5
sI
0.5
s
0.1
t
sI
1 pa 1−p p + pd c b
t
sI
1
t
0.9
Nils Jansen - Accelerating Parametric Probabilistic Verification
12 / 34
Contents
1 Motivation 2 Preliminaries 3 Model Checking Algorithm 4 Factorization of Polynomials and Implementation 5 Conclusion and Future Work
Nils Jansen - Accelerating Parametric Probabilistic Verification
13 / 34
SCC-based Model Checking - Summary
Problem Model Checking PDTMCs for unbounded reachability properties Idea Reduce each (nested) SCC to an abstract node whose outgoing edges carry the whole probability mass of all paths traversing this SCC. Recursive algorithm Bottom-Up computing starting with “minimal sub-SCCs” Exploiting specific properties of Markov Chains
Nils Jansen - Accelerating Parametric Probabilistic Verification
14 / 34
SCCs - Point of View Example SCC s2 s1 s3
Input node: s1 Output nodes: s2 and s3
Nils Jansen - Accelerating Parametric Probabilistic Verification
15 / 34
SCCs - Point of View Example SCC - more abstract view pr
s1
p2
s2
p3 s3
Input node: s1 Output nodes: s2 and s3 Probability pr of returning to input node Probabilities p2 , p3 of reaching output nodes Nils Jansen - Accelerating Parametric Probabilistic Verification
15 / 34
SCCs - Facts
pr
s1
p2
s2
Every path through a DTMC will eventually reach a Bottom-SCC (and stay there).
p3 s3
Nils Jansen - Accelerating Parametric Probabilistic Verification
16 / 34
SCCs - Facts
pr
s1
p2
s2
p3 s3
Nils Jansen - Accelerating Parametric Probabilistic Verification
Every path through a DTMC will eventually reach a Bottom-SCC (and stay there). Non-Bottom-SCC will be left at some point in time with probability 1.
16 / 34
SCCs - Facts
pr
s1
p2
s2
p3 s3
Nils Jansen - Accelerating Parametric Probabilistic Verification
Every path through a DTMC will eventually reach a Bottom-SCC (and stay there). Non-Bottom-SCC will be left at some point in time with probability 1. Probability of reaching one output node is composed of the probabilities of all finite paths through the SCC.
16 / 34
SCCs - One Input Node Probability of all paths entering and eventually leaving SCC: pr
p2
s2
X i∈N
s1
pri · (p2 + p3 ) =
1 · (p2 + p3 ) 1 − pr
p3 s3
Nils Jansen - Accelerating Parametric Probabilistic Verification
17 / 34
SCCs - One Input Node Probability of all paths entering and eventually leaving SCC: pr
p2
s2
X i∈N
s1
p3
pri · (p2 + p3 ) =
1 · (p2 + p3 ) 1 − pr
Prob. for leaving SCC is 1: s3
1 · (p2 + p3 ) = 1 1 − pr ⇔ pr = 1 − p2 − p3
Probability of coming back to input node can be computed without considering paths that lead back to it!
Nils Jansen - Accelerating Parametric Probabilistic Verification
17 / 34
SCCs Probability of reaching s2 : pr p2 s1
s2
1 · p2 1 − pr
p3 s3
Nils Jansen - Accelerating Parametric Probabilistic Verification
18 / 34
SCCs Probability of reaching s2 : p20 s1
1 · p2 1 − pr
s2
Discard pr and scale p2 and p3 :
p30 s3
Nils Jansen - Accelerating Parametric Probabilistic Verification
p20 =
p2 p2 + p3
p30 =
p3 p2 + p3
18 / 34
SCCs Probability of reaching s2 : p20 s1
1 · p2 1 − pr
s2
Discard pr and scale p2 and p3 :
p30 s3
p20 =
p2 p2 + p3
p30 =
p3 p2 + p3
Scaling preserves reachability probabilities: p20 =
p2 p2 1 = = · p2 p2 + p3 p2 + (1 − p2 − pr ) 1 − pr
Nils Jansen - Accelerating Parametric Probabilistic Verification
18 / 34
SCCs
s2 s1 s3
Paths returning to input node are ignored during computations.
Nils Jansen - Accelerating Parametric Probabilistic Verification
19 / 34
SCC-based Model Checking for PDTMCs
Preserve information about transition probabilities and outgoing probabilities =⇒ additional constraints in parametric case Keep graph structure
Constraints Constraint 1. The probability of every transition must be greater than 0: ∀s, s 0 ∈ S : P(s, s 0 ) 6= 0 =⇒ P[u](s, s 0 ) > 0 Constraint 2. The outgoing P probability of each state must be 1: ∀s ∈ S : s 0 ∈S P(s, s 0 ) = 1.
Nils Jansen - Accelerating Parametric Probabilistic Verification
20 / 34
Example S
S1 0.2
0.8
2
0.4 1
q
1 4
0.2
3
1−q
5
1
0.2 0.2
0.4 6
0.5
7
9 p
0.3
1
1−p
0.8 8 S2 Nils Jansen - Accelerating Parametric Probabilistic Verification
S2.1
21 / 34
Example 0.2
0.8
2
0.4 1
q
1 4
0.2
3
1−q
5
1
0.2 0.2
0.4 6
0.5
7
9 p
0.3
1
1−p
0.8 Identify input and output nodes
8 S2.1
Nils Jansen - Accelerating Parametric Probabilistic Verification
21 / 34
Example 0.2
0.8
2
0.4 1
q
1 4
0.2
3
1−q
5
1
0.2 0.2p 0.3p
0.4
0.5p S2.1
6
1−p
9
1
0.8
Compute outgoing probabilities
Nils Jansen - Accelerating Parametric Probabilistic Verification
21 / 34
Example 0.2
0.8
2
0.4 1
q
1 4
0.2
3
1−q
5
1
0.2 0.2p 1−0.3p
0.5p 1−0.3p
0.4
S2.1
6
1−p 1−0.3p
9
1
0.8 Scale with sum of all outgoing probabilities
Nils Jansen - Accelerating Parametric Probabilistic Verification
21 / 34
Example 0.2
0.8
2
0.4 1
q
1 4
0.2
3
1−q
5
1
0.2 0.2p 1−0.3p
0.5p 1−0.3p
0.4
S2.1
6 S2
1−p 1−0.3p
9
1
0.8
Nils Jansen - Accelerating Parametric Probabilistic Verification
21 / 34
Example 0.2
0.8
2
0.4 1
0.2−0.06p 1−0.7p
q
3 1
4
1−q
5
1
0.2 0.16p 1−0.7p
0.4 S2
Nils Jansen - Accelerating Parametric Probabilistic Verification
0.8−0.8p 1−0.7p
9
1
21 / 34
Example S1 0.2
0.8
2
0.4 1
0.2−0.06p 1−0.7p
q
3 1
4
1−q
5
1
0.2 0.16p 1−0.7p
0.4 S2
Nils Jansen - Accelerating Parametric Probabilistic Verification
0.8−0.8p 1−0.7p
9
1
21 / 34
Example 0.2
S12
0.8−0.8q 1−0.8q
S13 1−q 1−0.8q
0.4 0.2 1−0.8q
1
0.2−0.06p 1−0.7p
5
0.2q 1−0.8q
1
0.16p 1−0.7p
0.4 S2
Nils Jansen - Accelerating Parametric Probabilistic Verification
0.8−0.8p 1−0.7p
9
1
21 / 34
Example S 0.2
S12
0.8−0.8q 1−0.8q
S13 1−q 1−0.8q
0.4 0.2 1−0.8q
1
0.2−0.06p 1−0.7p
5
0.2q 1−0.8q
1
0.16p 1−0.7p
0.4 S2
Nils Jansen - Accelerating Parametric Probabilistic Verification
0.8−0.8p 1−0.7p
9
1
21 / 34
Example
S
−0.2872p−0.52q+0.3192pq+0.52 −0.6712p−0.744q+0.5432pq+0.904
5
1
−0.384p−0.224q+0.224pq+0.384 −0.6712p−0.744q+0.5432pq+0.904
9
Nils Jansen - Accelerating Parametric Probabilistic Verification
1
21 / 34
Computation of abstract probabilities
For each (sub-)SCC, the abstract probabilities can be computed by Path analysis Solving linear equation systems (by keeping rational functions as constants) State elimination
Nils Jansen - Accelerating Parametric Probabilistic Verification
22 / 34
Correctness
Theorem The SCC abstraction preserves reachability probabilities. Define probability measures on subsets of states w.r.t. ingoing and outgoing transitions Show correctness of abstraction for these subsets Assuming graph-preserving parameter evaluations
Nils Jansen - Accelerating Parametric Probabilistic Verification
23 / 34
Parameter Synthesis Intuitive approach Give rational function and additional constraints to SMT-solver and check against probability bound: fsI ,T ≤ λ If satisfiable, solver returns an assignment of variables which induces a well-defined evaluation of the rational function. If unsatisfiable, solver might return an UNSAT core whose information can be used for debugging purposes
Nils Jansen - Accelerating Parametric Probabilistic Verification
24 / 34
Parameter Synthesis Intuitive approach Give rational function and additional constraints to SMT-solver and check against probability bound: fsI ,T ≤ λ If satisfiable, solver returns an assignment of variables which induces a well-defined evaluation of the rational function. If unsatisfiable, solver might return an UNSAT core whose information can be used for debugging purposes Not feasible Ongoing work Approximative solutions Reduction of solution space Nils Jansen - Accelerating Parametric Probabilistic Verification
24 / 34
Contents
1 Motivation 2 Preliminaries 3 Model Checking Algorithm 4 Factorization of Polynomials and Implementation 5 Conclusion and Future Work
Nils Jansen - Accelerating Parametric Probabilistic Verification
25 / 34
Problems
Practical problems of parametric model checking Rapid growth of polynomials is major bottleneck of proposed procedures cancellation in every step, as done in PARAM Arithmetic operations involve costly computation of the gcd
Nils Jansen - Accelerating Parametric Probabilistic Verification
26 / 34
Problems
Practical problems of parametric model checking Rapid growth of polynomials is major bottleneck of proposed procedures cancellation in every step, as done in PARAM Arithmetic operations involve costly computation of the gcd our approach: maintain a (partial) factorization of occurring polynomials
Nils Jansen - Accelerating Parametric Probabilistic Verification
26 / 34
Factorization of Polynomials Intuition: Define arithmetical operations like ·, :, + on factorizations Develop algorithm for gcd-computation using these operations Reuse all factorizations computed beforehand Benchmarks are usually very symmetrical
Nils Jansen - Accelerating Parametric Probabilistic Verification
many similar polynomials
27 / 34
Factorization of Polynomials Intuition: Define arithmetical operations like ·, :, + on factorizations Develop algorithm for gcd-computation using these operations Reuse all factorizations computed beforehand Benchmarks are usually very symmetrical
many similar polynomials
Partial factorization obtained through use of gcd during algorithm Maintain g1 = G · F1 · F10 and g2 = G · F2 · F20 where G contains common factors, Fi will be checked and Fi0 does not contain common factors Compute gcd on relatively small polynomials and exclude irreducible polynomials no explicit computation of factorization Nils Jansen - Accelerating Parametric Probabilistic Verification
27 / 34
Factorization of Polynomials
Example: Two toy-factorizations: xyz
Nils Jansen - Accelerating Parametric Probabilistic Verification
xy
28 / 34
Factorization of Polynomials
Example: Two toy-factorizations: xyz
xy 1
Fxyz = {(xyz) }
Nils Jansen - Accelerating Parametric Probabilistic Verification
Fxy = {(x)1 , (y )1 }
28 / 34
Factorization of Polynomials
Example: Two toy-factorizations: xyz
xy 1
Fxyz = {(xyz) }
Fxy = {(x)1 , (y )1 }
(xyz)1
(x)1 (y )1
Nils Jansen - Accelerating Parametric Probabilistic Verification
28 / 34
Factorization of Polynomials
Example: Two toy-factorizations: xyz
xy 1
common factor x:
Fxyz = {(xyz) }
Fxy = {(x)1 , (y )1 }
(xyz)1
(x)1 (y )1
(x)1 (yz)1
(x)1 (y )1
Nils Jansen - Accelerating Parametric Probabilistic Verification
28 / 34
Factorization of Polynomials
Example: Two toy-factorizations: xyz
xy 1
Fxyz = {(xyz) }
Fxy = {(x)1 , (y )1 }
(xyz)1
(x)1 (y )1
common factor x:
(x)1 (yz)1
(x)1 (y )1
common factor y :
(x)1 (y )1 (z)1
(x)1 (y )1
Nils Jansen - Accelerating Parametric Probabilistic Verification
28 / 34
Implementation In COMICS1 in C++ with GiNaC Both Model Checking Strategies using Factorization of Polynomials SCC based State-elimination approach as used by PARAM
1
http://www-i2.informatik.rwth-aachen.de/i2/comics/
Nils Jansen - Accelerating Parametric Probabilistic Verification
29 / 34
Data structures
Data structure for rational functions: Store each polynomial only once Tree-like storage of factors for polynomials 2x 2 − 2
2
x −1
x 2 + 3x + 2
x +1
x +2
GiNaC’s GCD as fallback Representation of rational functions captures factorization =⇒ intuitive view
Nils Jansen - Accelerating Parametric Probabilistic Verification
30 / 34
Case Studies: BRP
Bounded Retransmission Protocol (BRP) Sending files in unreliable network Parameters: probability of reliability of 2 channels Structure: acyclic Graph States Trans.
SCC MC Time
Poly
3528 4611 29.05 3283 4361 5763 511.50 4247 7048 9219 548.73 6547 10759 13827 147.31 9231 21511 27651 1602.53 18443
STATE ELIM Mem
Time
Poly
Mem
PARAM Time
Mem
48.10 4.33 8179 61.17 98.99 32.90 501.71 6.87 9520 78.49 191.52 58.43 281.86 25.05 16435 216.05 988.28 142.66 176.89 85.54 26807 682.24 3511.96 304.07 776.48 718.66 53687 3134.59 34322.60 1757.12
Nils Jansen - Accelerating Parametric Probabilistic Verification
31 / 34
Case Studies: BRP
Bounded Retransmission Protocol (BRP) Sending files in unreliable network Parameters: probability of reliability of 2 channels Structure: acyclic Graph States Trans.
SCC MC Time
Poly
3528 4611 29.05 3283 4361 5763 511.50 4247 7048 9219 548.73 6547 10759 13827 147.31 9231 21511 27651 1602.53 18443
STATE ELIM Mem
Time
Poly
Mem
PARAM Time
Mem
48.10 4.33 8179 61.17 98.99 32.90 501.71 6.87 9520 78.49 191.52 58.43 281.86 25.05 16435 216.05 988.28 142.66 176.89 85.54 26807 682.24 3511.96 304.07 776.48 718.66 53687 3134.59 34322.60 1757.12
Nils Jansen - Accelerating Parametric Probabilistic Verification
31 / 34
Case Studies: Crowds Crowds protocol Anonymous network communication using random routing Parameters: probability of member being “good” probability if “good” member delivers message
Structure: nested SCCs Graph States 198201 482979 726379 961499 1729494 2888763
Trans.
SCC MC Time
Poly
STATE ELIM Mem
Time
Poly
PARAM Mem
Time
Mem
348349 60.90 13483 140.15 243.07 27340 133.91 46380.00 227.66 728677 35.06 35916 478.85 247.75 65966 297.40 TO — 1283297 223.24 36649 515.61 1632.63 73704 477.10 TO — 1452537 81.88 61299 1027.78 646.76 112452 589.21 TO — 2615272 172.59 97655 2372.35 1515.63 178885 1063.15 TO — 5127151 852.76 110078 2345.06 12326.80 224747 2123.96 TO —
TO: 14h = 50400s
Nils Jansen - Accelerating Parametric Probabilistic Verification
32 / 34
Case Studies: Crowds Crowds protocol Anonymous network communication using random routing Parameters: probability of member being “good” probability if “good” member delivers message
Structure: nested SCCs Graph States 198201 482979 726379 961499 1729494 2888763
Trans.
SCC MC Time
Poly
STATE ELIM Mem
Time
Poly
PARAM Mem
Time
Mem
348349 60.90 13483 140.15 243.07 27340 133.91 46380.00 227.66 728677 35.06 35916 478.85 247.75 65966 297.40 TO — 1283297 223.24 36649 515.61 1632.63 73704 477.10 TO — 1452537 81.88 61299 1027.78 646.76 112452 589.21 TO — 2615272 172.59 97655 2372.35 1515.63 178885 1063.15 TO — 5127151 852.76 110078 2345.06 12326.80 224747 2123.96 TO —
TO: 14h = 50400s
Nils Jansen - Accelerating Parametric Probabilistic Verification
32 / 34
Case Studies: NAND NAND multiplexing Computation on copies of NAND unit with unreliable hardware Parameters: probability of faultiness of units probability of erroneous input
Structure: acyclic, many paths join in specific states and diverge again Graph States
Trans.
SCC MC Time
Poly
STATE ELIM Mem
Time
Poly
PARAM Mem
Time
Mem
7393 11207 8.35 15688 114.60 17.02 140057 255.13 5.00 10.67 14323 21567 39.71 25504 366.79 59.60 405069 926.33 15.26 16.89 21253 31927 100.32 35151 795.31 121.40 665584 2050.67 29.51 24.45 28183 42287 208.41 44799 1405.16 218.85 925324 3708.27 50.45 30.47 78334 121512 639.29 184799 3785.11 — — MO 1138.82 111.58
MO: 4GB
Nils Jansen - Accelerating Parametric Probabilistic Verification
33 / 34
Case Studies: NAND NAND multiplexing Computation on copies of NAND unit with unreliable hardware Parameters: probability of faultiness of units probability of erroneous input
Structure: acyclic, many paths join in specific states and diverge again Graph States
Trans.
SCC MC Time
Poly
STATE ELIM Mem
Time
Poly
PARAM Mem
Time
Mem
7393 11207 8.35 15688 114.60 17.02 140057 255.13 5.00 10.67 14323 21567 39.71 25504 366.79 59.60 405069 926.33 15.26 16.89 21253 31927 100.32 35151 795.31 121.40 665584 2050.67 29.51 24.45 28183 42287 208.41 44799 1405.16 218.85 925324 3708.27 50.45 30.47 78334 121512 639.29 184799 3785.11 — — MO 1138.82 111.58
MO: 4GB
Nils Jansen - Accelerating Parametric Probabilistic Verification
33 / 34
Contribution and Future Work Contribution SCC-based Model Checking for Parametric Markov Chains New gcd-computation based on Factorization of Polynomials
Nils Jansen - Accelerating Parametric Probabilistic Verification
34 / 34
Contribution and Future Work Contribution SCC-based Model Checking for Parametric Markov Chains New gcd-computation based on Factorization of Polynomials Future Work Better Management of Polynomials Interaction for user to change or restrict parameter values =⇒ finer intervals for parameters, abstract transitions and model checking bound Efficient methods to synthesize parameters Parametric Markov chains are operational semantics of probabilistic programs Tool Upcoming!
Nils Jansen - Accelerating Parametric Probabilistic Verification
34 / 34
Contribution and Future Work Contribution SCC-based Model Checking for Parametric Markov Chains New gcd-computation based on Factorization of Polynomials Future Work Better Management of Polynomials Interaction for user to change or restrict parameter values =⇒ finer intervals for parameters, abstract transitions and model checking bound Efficient methods to synthesize parameters Parametric Markov chains are operational semantics of probabilistic programs Thank You!
Nils Jansen - Accelerating Parametric Probabilistic Verification
34 / 34
