Download

lkdfjsdfjksdl;jfsdf - A testing scenario for probabilistic automata, Marielle Stoelinga UC Santa

Upload
0
Embed
Share
Upload and view presentations on any device and embed the player to your website! --- > >
Upload PPT
Upload PPT

Download this Presentation

josie

2021-9-26 published at Product Training/ Manuals category

Presentation Transcript

1.A testing scenario for probabilistic automata Marielle Stoelinga UC Santa Cruz Frits Vaandrager University of Nijmegen
2.Characterization of process equivalences process equivalences bisimulation / ready trace / ... equivalence algebraical / logical / denotional / ... definitions are these reasonable ? justify equivalence via testing scenarios / button pushing experiments comparative concurrency theory De Nicola & Hennesy [DH86], Milner [Mil80], van Glabbeek [vGl01] testing scenarios: define intuitive notion of observation, fundamental processes that cannot be distinguished by observation ce ´: P ´ Q iff Obs(P) = Obs(Q) ´ does not distinguish too much/too little P Q ´ ??
3.Characterization of process equivalences process equivalences bisimulation / ready trace / ... equivalence algebraical / logical / denotional / ... definitions are these reasonable ? justify equivalence via testing scenarios / button pushing experiments testing scenarios: define intuitive notion of observation, fundamental processes that cannot be distinguished by observation are deemed to be equivalent justify process equivalence ´: P ´ Q iff Obs(P) = Obs(Q) ´ does not distinguish too much/too little P Q ´ ??
4.Main results testing scenarios in non-probabilistic case trace equivalence bisimulation ... we define observations of a probabilistic automaton (PA) observe probabilities through statistical methods (hypothesis testing) characterization result Obs(P) = Obs(Q) iff trd(P) = trd(Q), P, Q finitely branching trd(P) extension of traces for PAs. [Segala] justifies trace distr equivalence in terms of observations
5.Model for testing scenarios a machine M a black box inside: process described by LTS P display showing current action buttons for user interaction display machine buttons
6.Model for testing scenarios a an observer records what s/he sees (over time) + buttons define ObsM(P): observations of P = what observer records, if LTS P is inside M display machine buttons
7.Model for testing scenarios a processes (LTSs) with same observations are deemed to be equivalent characterization results: ObsM(P) = ObsM(Q) iff P ´ Q ´ does not distinguish too much/too little display machine buttons
8.Trace Machine (TM) a no buttons for interaction display shows current action
9.Trace Machine (TM) a no buttons for interaction display shows current action with P inside M, an observer sees one of e, a, ab, ac ObsTM(P) = traces of P testing scenario justifies trace (language) equivalence b c a P
10.Trace Machine (TM) a no distinguishing observation between b c a a a b c
11.Trace Distribution Machine (TDM) reset button: start over repeat experiments each experiment yields trace of same length k (wlog) observe frequencies of traces d reset h t 1/2 1/2 d l P
12.Trace Distribution Machine (TDM) 100 exps, length 2 frequencies - hd tl tl hd tl .... hd hd 48 tl 52 other 0 (hh,dh,hl,...) d reset h t 1/2 1/2 d l P
13.Trace Distribution Machine (TDM) with many experiments: #hd ¼ # tl 100 exps, length 2 frequencies - hd tl tl hd tl .... hd hd 48 tl 52 other 0 d reset h t 1/2 1/2 d l P not every seq of experiments is an observation
14.Trace Distribution Machine (TDM) with many experiments: #hd ¼ # tl 100 exps, length 2 frequencies - hd tl tl hd tl ... hd hd 48 tl 52 other 0 - hd hd hd hd .... hd hd 100 tl 0 other 0 d reset h t 1/2 1/2 d l P 2 Obs(P) freq likely 2 Obs(P) freq unlikely /
15.Trace Distribution Machine (TDM) nondeterministic choice choose one transition probabilistically in large outcomes: 1/2 #c + 1/3 #d ¼ #b use statistics: b,b,b,....b 2 Obs(P) freqs likely b,d,c,b,b,b,c,... 2 Obs(P) freqs unlikey d reset b d 1/3 3/4 c b 2/3 1/4 P /
16.Observations TDM ObsTDM(P) = { s | s is likely to be produced by P} a reset h t 1/2 1/2 d l P
17.Observations TDM perform m experiments (m resets) each experiment yields trace of length k (wlog) sequence s2 (Actk)m Obs(P) = {s2 (Actk)m | s is likely to be produced by P, k,m 2 N} what is likely? use hypothesis testing a reset h t 1/2 1/2 d l P
18.Which frequencies are likely? I have a sequence s = h,t,t,t,h,t,... 2 {h,t}100 I claim: generated s with automaton P. do you believe me if s contains 15 h’s? if s contains 42 h’s? h t 1/2 1/2
19.Which frequencies are likely? I have a sequence s = h,t,t,t,h,t,... 2 {h,t}100 I claim: generated s with automaton P. do you believe me if s contains 15 h’s? if s contains 42 h’s? use hypothesis testing: fix confidence level a 2 (0,1) H0 null hypothesis = s is generated by P h t 1/2 1/2 0 50 100 40 60 K: accept H0 reject H0 reject H0 #h
20.Which frequencies are likely? I have a sequence s = h,t,t,t,h,t,... 2 {h,t}100 I claim: generated s with automaton P. do you believe me if s contains 15 h’s? if s contains 42 h’s? use hypothesis testing: fix confidence level a 2 (0,1) H0 null hypothesis = s is generated by P PH0[K] > 1-a : prob on false rejection · a P: H0[K] minimal : prob on false acceptance minimal h t 1/2 1/2 0 50 100 40 60 K: accept H0 reject H0 reject H0 #h
21.Which frequencies are likely? I have a sequence s = h,t,t,t,h,t,... 2 {h,t}100 I claim: generated s with automaton P. do you believe me if s contains 15 h’s? NO if s contains 42 h’s? YES use hypothesis testing: fix confidence level a 2 (0,1) H0 null hypothesis = s is generated by P PH0[K] > 1-a : prob on false rejection · a P: H0[K] minimal : prob on false acceptance minimal h t 1/2 1/2 0 50 100 40 60 K: accept H0 reject H0 reject H0 #h
22.Example: Observations for a =0.05 Obs(P) = {s2 (Actk)m | s is likely to be produced by P, k,m2 N } for k = 1 and m = 100 s2 (Act)100 is an observation iff 40 · freqs (hd) · 60 h t 1/2 1/2 0 50 100 40 K1,100 60
23.Example: Observations for a =0.05 Obs(P) = {s2 (Actk)m | s is likely to be produced by P, k,m2 N } for k = 1 and m = 100 s2 (Act)100 is an observation iff 40 · freqs (hd) · 60 for k = 1 and m = 200 s2 (Act)200 is an observation iff 88 · freqs (h) · 112 etc .... h t 1/2 1/2 0 100 200 88 K1,200 112
24.Example: Observations for a =0.05 Obs(P) = {s2 (Actk)m | s is likely to be produced by P, k,m2 N } for k = 1 and m = 100, s2 (Act)100 is an observation iff 40 · freqs (hd) · 60 for k = 1 and m = 200 s2 (Act)200 is an observation iff 88 · freqs (h) · 112 etc .... h t 1/2 1/2 0 100 200 88 K1,200 112 exp freq EP allowed deviation e ( = 12) 0
25.With nondeterminism s = b,c,c,d,b,d,....,c 2 Obs(P) ?? a a 1/3 3/4 b c 1/4 2/3 P
26.With nondeterminism s = b,c,c,d,b,d,....,c 2 Obs(P) ?? fix schedulers: p1, p2, p3... p100 pi = P[take left trans in experiment i] 1 - pi = P[take right trans in experiment i] H0: s is generated by P under p1, p2, p3... p100 critical section Kp1,...,p100 a a 1/3 3/4 b c 1/4 2/3 P
27.With nondeterminism s = b,c,c,d,b,d,....,c 2 Obs(P) ?? fix schedulers: p1, p2, p3... p100 pi = P[take left trans in experiment i] 1 - pi = P[take right trans in experiment i] H0: s is generated by P under p1, p2, p3... p100 critical section Kp1,...,p100 a a 1/3 3/4 b c 1/4 2/3 P s 2 Obs(P) iff s2 Kp1,...,p100 for some p1, p2, p3... p100
28.With nondeterminism fix p1, p2, p3... p100 compute Pp1, p2, p3... p100[s] for every s e.g pi = ½, Pp1, p2, p3... p100 [c,c...c] = (½*2/3)100 expected frequency Ep1,...,p100 for c = åi 2/3 pi d = åi 3/4 (1-pi) b = åi 1/3 pi + ¼ (1-pi) as before: critical section Kp1,...,p100 b b 1/3 pi ¾(1-pi) c d ¼(1-pi) 2/3pi
29.With nondeterminism fix p1, p2, p3... p100 compute Pp1, p2, p3... p100[ s] for every s expected frequency E as before: critical section Kp1,...,p100 H0: s is generated by P under p1, p2, p3... p100 allow observations to deviate < e from E Kp1,...,p100 – = Pp1, p2, p3... p100[spheree (E)] with e minimal with Pp1, p2, p3... p100[spheree (E)] > a b b 1/3 3/4 c d 1/4 2/3
30.Example: Observations Observations for k =1, m = 100. s contains b,c only with 54 · freqs (c) · 78 take pi = 1 for all i s contains b,d only with 62 · freqs (d) · 88 take pi = 0 for all i b b 1/3 3/4 c d 1/4 2/3
31.Example: Observations Observations for k =1, m = 100. s contains a,b only and 54 · freqs (c) · 78 take pi = 1 for all i s contains b,d only and 62 · freqs (d) · 88 take pi = 0 for all i Observations for k=1, m = 200 61 · freqs (c) · 71 and 70 · freqs (d) · 80 pi = ½ for all i (exp 66 c’s; 74 d’s; 60 b’s) (these are not all observations; they form a sphere) b b 1/3 3/4 c d 1/4 2/3
32.Main result TDM characterizes trace distr equivalence ObsTDM(P) = ObsTDM(Q) iff trd(P) = trd(Q) if P, Q are finitely branching justifies trace distribution equivalence in an observational way
33.
34.Main result TDM characterizes trace distr equiv ´TD ObsTDM(P) = ObsTDM(Q) iff trd(P) = trd(Q) “only if” part is immediate, “if”-part is hard. find a distinguishing observation if P, Q have different trace distributions. IAP for P. Q fin branching P, Q have the same infinite trace distrs iff P, Q have the same finite trace distrs the set of trace distrs is a polyhedron Law of large numbers for random vars with different distributions
35.Observations a =0.05 Obs(P) = {s2 (Actk)m | s likely to be produced by P} Obs(P) = {s2 (Actk)m | freq_s in K} for k = 1 and m = 100, b2 (Act)100 is an observation iff 40 · freqb (hd) · 60 h t 1/2 1/2 0 50 100 40 60 K
36.Nondeterministic case \sigma = \beta_1 ,...\beta_m fixed adversaries take in expect_freq for \gamma\in Act^k, freq_\gamma(\beta) freq \in \ we consider only frequency of traces in an outcome h t 1/2 1/2
37.a! b! a? b? b c a
38.a! b! a?
39.Trace Distribution Machine (TDM) reset button: start over repeat experiments: yields sequence of traces in large outcomes: #hd ¼ # tl use statistics: hd,hd,hd,...,hd 2 Obs(P) too unlikely hd,tl,tl,hd,...tl,hd 2 Obs(P) likely d reset / h t 1/2 1/2 d l
40. h t 1/2 1/2 0 50 100 40 60 exp freq
41.Process equivalences Q P
42.Testing scenario’s a a black box with display and buttons inside: process described by LTS P display: current action what do we see (over time)? ObsM(P) P, Q are deemed equivalent iff ObsM(Q) = ObsM(Q) desired characterization: display machine buttons
43.Observations a =0.05 Obs(P) = {s2 (Actk)m | s is likely to be produced by P} for k = 1 and m = 99, expectation E = (33,33,33) Obs(P) = {s2 (Act)99 | | s – E | < 15} h t 1/3 1/3

Latest Release