Reachability and Reward Checking for Stochastic Timed

AVOCS, SEPTEMBER 2014, ENSCHEDE
a
,
Reachability and Reward Checking
for Stochastic Timed Automata
TA
s
,b
,
A
PT
DP
M
C
M
te s
DT iscrebilitie
A
/T
meocks
cl
d a
b
S ter- pro
T
L de
n is
nomin
m
E. Moritz Hahn, Arnd Hartmanns, Holger Hermanns
Chinese Academy
of Sciences,
ChinaChecking
/ Saarlandfor
University,
Germany
Arnd Hartmanns
Reachability
and Reward
Stochastic
Timed Automata
Talk Outline
1
2
3
Stochastic Timed Automata
,b
a
,
,
Model Checking STA
mcsta
Experimental Results
Arnd Hartmanns


Reachability and Reward Checking for Stochastic Timed Automata
Stochastic Timed Automata
Nondeterministic
= unquantified
= uncertainty
Probabilistic
= quantified
= uncertainty
b
a
1
2
1
, {𝑐
2
𝑐 ≥ 6, 𝜏
MDP
≔ 0}
𝑐 ≥ 8, 𝜏
LTS
DTMC
nondeter- discrete
minism probabilities
Arnd Hartmanns
Reachability and Reward Checking for Stochastic Timed Automata
Stochastic Timed Automata
Nondeterministic Probabilistic Timed
+ clocks
clock c;
𝑐≥6
guards
invariants 𝑐 ≤ 8
b
𝑡𝑟𝑢𝑒
𝑡𝑟𝑢𝑒
a
𝑐 ≥ 6, 𝜏
Pmax ⋄
time/ TA
clocks
≔ 0}
𝑐≤8
𝑐 ≥ 8, 𝜏
∧ 𝑡𝑖𝑚𝑒 < 8 = ?
Arnd Hartmanns
𝑡𝑟𝑢𝑒
1
2
1
, {𝑐
2
PTA
𝑡𝑟𝑢𝑒
LTS
MDP
DTMC
nondeter- discrete
minism probabilities
Reachability and Reward Checking for Stochastic Timed Automata
Stochastic Timed Automata
Nondeterministic Probabilistic Timed
+ sampling from arbitrary distributions
𝑐≤𝑥
𝑡𝑟𝑢𝑒
a
𝑐 ≥ 6, 𝜏
Pmax ⋄
𝑐 ≥ 𝑥, b
1
, {𝑐
2
≔ 0}
∧ 𝑡𝑖𝑚𝑒 < 8 = ?
Arnd Hartmanns
𝑡𝑟𝑢𝑒
≔ 0, 𝑥 ≔ EX P (λ)}
𝑐 ≥ 8, 𝜏
arbitrary STA
distributions
PTA
1
, {𝑐
2
𝑐≤8
Stochastic
𝑡𝑟𝑢𝑒
time/ TA
clocks
LTS
MDP
DTMC
nondeter- discrete
minism probabilities
Reachability and Reward Checking for Stochastic Timed Automata
Stochastic Timed Automata
+
{𝑐 ≔ 0}
wait for 𝑐 = 8 when it
causes most problems?
always wait
until 𝑐 = 8?
𝑐≤𝑥
𝑡𝑟𝑢𝑒
a
𝑐 ≥ 6, 𝜏
Pmax ⋄
𝑐≤8
distributions
𝑐 ≥ 𝑥, b
PTA
𝑡𝑟𝑢𝑒
1
, {𝑐
2
≔ 0, 𝑥 ≔ EX P (λ)}
1
, {𝑐
2
≔ 0}
𝑐≤8
𝑐 ≥ 8, 𝜏
∧ 𝑡𝑖𝑚𝑒 < 8 = ?
Arnd Hartmanns
+
nondeterministic
delay
always go as
soon as 𝑐 = 6 ?
arbitrary STA
𝑐≥6
𝑡𝑟𝑢𝑒
time/ TA
clocks
LTS
MDP
DTMC
nondeter- discrete
minism probabilities
Reachability and Reward Checking for Stochastic Timed Automata
Stochastic Timed Automata
{𝑐 ≔ 0}
+
𝑐≥6
+
𝑐≤8
{𝑐 ≔ 0, 𝑥 ≔ UN I (6,8)}
+
𝑐≥𝑥
+
𝑐≤𝑥
nondeterministic
delay
arbitrary STA
stochastic delay
distributions
= specific resolution of the nondeterminism
PTA
𝑐≤𝑥
𝑡𝑟𝑢𝑒
a
𝑐 ≥ 6, 𝜏
Pmax ⋄
𝑐 ≥ 𝑥, b
1
, {𝑐
2
≔ 0, 𝑥 ≔ EX P (λ)}
1
, {𝑐
2
≔ 0}
𝑐≤8
𝑐 ≥ 8, 𝜏
∧ 𝑡𝑖𝑚𝑒 < 8 = ?
Arnd Hartmanns
𝑡𝑟𝑢𝑒
𝑡𝑟𝑢𝑒
time/ TA
clocks
LTS
MDP
DTMC
nondeter- discrete
minism probabilities
Reachability and Reward Checking for Stochastic Timed Automata
Stochastic Timed Automata
Nondeterministic Probabilistic
+ rate and transition rewards
∗: der 𝑤𝑎𝑖𝑡 = 1
∗∗: {𝑟𝑒𝑡𝑟𝑖𝑒𝑠 ≔ 𝑟𝑒𝑡𝑟𝑖𝑒𝑠 + 1}
∗
a
𝑡𝑟𝑢𝑒
𝑐 ≥ 6, 𝜏
∗∗
Emax 𝑤𝑎𝑖𝑡 |
Arnd Hartmanns
𝑐 ≥ 𝑥, b
𝑐≤𝑥
Timed
arbitrary STA
distributions
PTA
𝑡𝑟𝑢𝑒
1
, {𝑐
2
≔ 0, 𝑥 ≔ EX P (λ)}
1
, {𝑐
2
≔ 0}
𝑐≤8
=?
𝑐 ≥ 8, 𝜏
∗
Stochastic
Priced
𝑡𝑟𝑢𝑒
time/ TA
clocks
LTS
MDP
DTMC
nondeter- discrete
minism probabilities
Reachability and Reward Checking for Stochastic Timed Automata
Stochastic Timed Automata
continuous
dynamics SHA
Stochastic Hybrid Automata
+ complex continuous
behaviour
arbitrary STA
distributions
der(𝑣) = 𝑎 ∧ 𝑣 ⋅ 𝑣𝑚𝑎𝑥
"Markovian" models
= exponentially distributed
delays
MA
PTA
IMC time/ TA
MDP
clocks
CTMC
LTS
DTMC
exp. distr. nondeter- discrete
minism probabilities
delays
Arnd Hartmanns
Reachability and Reward Checking for Stochastic Timed Automata
Stochastic Timed Automata
nondeterministic
probabilistic
stochastic
∗
a
𝑡𝑟𝑢𝑒
𝑐 ≥ 6, 𝜏
∗∗
×
choices
delays
𝑐 ≥ 𝑥, b
𝑐≤𝑥
1
, {𝑐
2
≔ 0}
∗
arbitrary STA
distributions
𝑡𝑟𝑢𝑒
≔ 0, 𝑥 ≔ EX P (λ)}
𝑐 ≥ 8, 𝜏
rewards
PTA
1
, {𝑐
2
𝑐≤8
+
𝑡𝑟𝑢𝑒
time/ TA
clocks
LTS
MDP
DTMC
nondeter- discrete
minism probabilities
Arnd Hartmanns
Reachability and Reward Checking for Stochastic Timed Automata
Where are we?
1
2
3
Stochastic Timed Automata
,b
a
,
,
Model Checking STA
mcsta
Experimental Results
Arnd Hartmanns


Reachability and Reward Checking for Stochastic Timed Automata
Model Checking STA
Adapt existing method for SHA
implemented in the prohver tool:
upper bound on maximum reachability probabilities
P(crash within 15 years) ≤ 10-5 ?
+ min probabilities
+ max/min rewards
in theory
Fränzle, Hahn, Hermanns, Wolovick, Zhang:nn
Measurability and Safety Verification forn
Stochastic Hybrid Systems (HSCC 2011)
Arnd Hartmanns
Reachability and Reward Checking for Stochastic Timed Automata
Model Checking STA
Overapproximation of continuous distributions
𝑥 ≔ NO R M (𝑚, 1)}
0.2
0.2
0.2
0.2
0.2
discrete pr. choice of interval + nondeterministic value
Arnd Hartmanns
Reachability and Reward Checking for Stochastic Timed Automata
Model Checking STA
Overapproximation of continuous distributions
𝑐≤𝑥
𝑡𝑟𝑢𝑒
a
𝑐 ≥ 6, 𝜏
Arnd Hartmanns
𝑐 ≥ 𝑥, b
𝑡𝑟𝑢𝑒
1
2, {𝑐
≔ 0, 𝑥 ≔ EX P (λ)}
1
2, {𝑐
≔ 0}
𝑐≤8
𝑐 ≥ 8, 𝜏
𝑡𝑟𝑢𝑒
Reachability and Reward Checking for Stochastic Timed Automata
Model Checking STA
Overapproximation of continuous distributions
𝑐≤𝑥
𝑡𝑟𝑢𝑒
a
1
2, {𝑐
𝑐 ≥ 𝑥, b
𝑡𝑟𝑢𝑒
≔ 0, 𝑥 ≔ EX P (λ)}
1
2, …
𝑐 ≥ 𝑥, b
𝑐≤𝑥
1−𝑒 −𝜆
2 , {𝑐
≔ 0, 𝑥 ≔ [0,1]}
𝑡𝑟𝑢𝑒
Arnd Hartmanns
a
1
,…
2
𝑐≤𝑥
𝑒 −𝜆
2 , {𝑐
𝑡𝑟𝑢𝑒
𝑐 ≥ 𝑥, b
≔ 0, 𝑥 ≔ [1, ∞)}
Reachability and Reward Checking for Stochastic Timed Automata
Model Checking STA
Specialised method for STA
upper bounds on max. reachability & rewards
lower bounds on min. reachability & rewards
prohver for SHA:
Arnd Hartmanns
Reachability and Reward Checking for Stochastic Timed Automata
Where are we?
1
2
3
Stochastic Timed Automata
,b
a
,
,
Model Checking STA
mcsta
Experimental Results
Arnd Hartmanns


Reachability and Reward Checking for Stochastic Timed Automata
Experimental Results
Implementation: mcsta tool
1. Automatic overapproximation
unit-width intervals, single parameter ϱ:
"remaining probability" for unbounded distributions
2. On-the-fly digital clocks semantics
3. Explicit-state MDP model checking
part of the Modest Toolset
www.modestchecker.net
Arnd Hartmanns
Reachability and Reward Checking for Stochastic Timed Automata
Experimental Results
Example: M/G/1/6 queueing system
arrivals: exponentially distributed
service time: normal distribution
P(queue full within time bound) = ?
Arnd Hartmanns
Reachability and Reward Checking for Stochastic Timed Automata
Experimental Results
Example: M/G/1/6 queueing system
arrivals: exponentially distributed
service time: normal distribution
P(queue full within time bound) = ?
Arnd Hartmanns
Reachability and Reward Checking for Stochastic Timed Automata
Experimental Results
Example: M/G/1/6 queueing system
arrivals: exponentially distributed
service time: normal distribution
Time-bounded reachability probability
P(queue full within time bound) = ?


Time-unbounded expected accumulated reward
E(time until queue full) = ?
[43.4, ∞) (actually ≈ 61)


E(#customers until queue full) = ? [3.52, ∞) (actually ≈ 6.2)
 136 K MDP
Arnd Hartmanns
states only
Reachability and Reward Checking for Stochastic Timed Automata
Experimental Results
Example: tandem queueing system
time dilation
to reduce error
Example: WLAN (CSMA/CA)
uniform instead of nondeterministic transmission time
Arnd Hartmanns
Reachability and Reward Checking for Stochastic Timed Automata
Experimental Results
Example: file server with slow archival storage
= exponentially distributed interarrival times for requests
+ uniformly distributed file size (= time to send reply)
+ 2 % chance for file to be in slow archival storage
+ time for archive retrieval nondeterministic in [30, 40] s
+ initial queue length follows discrete uniform distribution
Arnd Hartmanns
Reachability and Reward Checking for Stochastic Timed Automata
Where are we?
1
2
3
Stochastic Timed Automata
,b
a
,
,
Model Checking STA
mcsta
Experimental Results
Arnd Hartmanns


Reachability and Reward Checking for Stochastic Timed Automata
Summary
Stochastic Timed Automata
nondeterministic
choices
probabilistic ×
delays
stochastic
continuous
dynamics SHA
+ rewards
arbitrary STA
distributions
Model checking with mcsta
PTA
bounds for reachability
probabilities & expected rewards
State space nuclear explosion
Over-/underapproximation

www.modestchecker.net
Arnd Hartmanns
time/ TA
clocks
LTS
MDP
?
DTMC
nondeter- discrete
minism probabilities
Reachability and Reward Checking for Stochastic Timed Automata

Download Report