Transcript Probabilistic Verification of Discrete Event Systems

Probabilistic Verification of
Discrete Event Systems
Håkan L. S. Younes
The Problem

Given a model of a discrete event
system, check if certain properties hold


The model is a stochastic process (GSMP)
Properties are expressed using a logic
formalism (CSL)
Probabilistic Verification

Verification of probabilistic properties


“The probability of reaching a failure state
within 60 minutes is less than 0.1”
Probabilistic verification of properties

“The probability of property P holding is at
least 0.95”
Discrete Event System (DES)



Event-driven system
Discrete state changes at the
occurrence of events
Examples:



Manufacturing systems
Queueing systems
Communication protocols
Why Probabilistic Verification?

The dynamics of a DES is too complex
for symbolic methods


Use simulation to generate sample paths
Use acceptance sampling to verify
probabilistic properties
Stochastic Processes

A stochastic process consists of


a set of states
a set of transitions (or events)
S2
S1
S3
S4
Markov Processes

The Markov assumption

There is enough information in the current
state to determine the future behavior
0.4
S2
S1
0.6
1.0
S4
1.0
0.2
S3
0.8
Holding Times


The holding time is the time spent in a
state before an event occurs
Holding times are positive random
variables

Can be discrete or continuous
Continuous-time
Markov Chain (CTMC)
Holding times are governed by
exponential distributions
0.4
S2
1.0
S1
4
1.0
State

3
2
1
S3
Time
0.6
S4
0.8
0.2
Semi-Markov Process

Holding times are governed by arbitrary
(positive) distributions
0.4
S2
1.0
S1
1.0
S3
0.6
S4
0.8
0.2
Generalized Semi-Markov
Process (GSMP)
Holding times can depend on the
history
4
0.4
S1 E1
E2
0.7
0.3
S2 E2
E3
0.5
0.5
1.0
3
2
1
Time
S3
0.6
S4 E1
State

1.0
E1
3.5
-
-
E2
5.0
1.5
-
E3
-
2.0
-
Properties

Qualitative


“P will eventually hold on all future
execution paths”
Quantitative

“P will hold before time t with probability at
least  on future execution paths”
Problem Space
Model
Properties
Qualitative
Quantitative
CTMC
[EMSS89]*
[ASSB96],[BKH99]
GSMP
[ACD91]
My Work
*Discrete time
Continuous Stochastic Logic
(CSL)

State formulas: a, ¬, 1  2, Pr()


Truth value is determined in a single state
Path formulas: X , 1 Ut 2

Truth value is determined over an
execution path
Execution Paths



Current state + current clock settings =
internal state
The internal state contains enough
information to determine the future
behavior
A sequence of internal states is an
execution path
S0,C0
t0
S1,C1
t1
S2,C2
t2
CSL Semantics
(State Formulas)


Atomic proposition: a
Negation: ¬


Holds iff  does not hold in current state
Conjunction: 1  2

Holds iff both 1 and 2 hold in current
state
CSL Semantics
(More State Formulas)

Probabilistic statement: Pr()

Holds iff  is true over at most a 
proportion of execution paths starting in
the current state
CSL Semantics
(Path Formulas)

Next state: X 


Holds iff  holds in the next state along the
current execution path
Until: 1 Ut 2

Holds iff 2 becomes true in some state
along the current execution path before
time t, and 1 is true in all prior states
More on Until

a,¬b
a,¬b
a,¬b
Consider the formula a U17 b
2
2
2
a,¬b
¬a,¬b
a,¬b
3
3
3
a,¬b
a,¬b
a,¬b
4
4
4
b
b
a,¬b
11
11
11
b
b
b
Verifying Probabilistic
Statements

Verify Pr()


Generate sample execution paths using
discrete event simulation
Verify  over each sample path



If  is true, then we have a positive sample
If  is false, then we have a negative sample
Based on the proportion of positive
samples, determine if Pr() holds
Sequential Hypothesis Testing

Hypothesis: Pr()
True, false,
or another
sample?
Error Bounds

Probability of false negative: 


We say that Pr() is false when it is true
Probability of false positive: 

We say that Pr() is true when it is false
Indifference Region
Probability of accepting
Pr () as true
False negatives
1–
Indifference region
False positives

–  +
Actual probability of  holding
Graphical Representation of
Statistical Test
We can find an acceptance line and a
rejection line given , , , and 
Number of
positive samples

Reject
Continue sampling
Accept
Number of samples
Verification of Nested
Probabilistic Statements

Suppose , in Pr(), contains
probabilistic statements
True, false,
or another
sample?
Indirect Sampling


Want samples from random variable X
Can only get samples from Y such that




Pr[Y=1|X=1]
Pr[Y=0|X=1]
Pr[Y=1|X=0]
Pr[Y=0|X=0]




1 – ’
’
’
1 – ’
Modified Test
find an acceptance line and a rejection
line given , , , , ’, and ’:
Number of
positive samples

Reject
Continue sampling
Accept
Number of samples
Verification of Compound
State Formulas

To verify ¬ with error bounds  and 


Verify  with error bounds  and 
To verify 1  2  …  n with error
bounds  and 

Verify 1 though n with error bounds /n
and /n
Sequential Verification of
Conjunction

To verify 1  2  …  n with error
bounds  and 
1.
2.
3.
4.
Verify each i with error bounds  and ’
Return false as soon as any i is verified
to be false
If all i are verified to be true, verify each
i again with error bounds  and /n
Return true iff all i are verified to be
true
Verification of Path Formulas

To verify X  with error bounds  and 


Verify  with error bounds  and  in the
next state
To verify 1 Ut 2 with error bounds 
and 

Convert to conjunction

1 Ut 2 holds if 2 holds in the first state, or if
2 holds in the second state and 1 holds in all
prior state, …
More on Verifying Until



Given 1 Ut 2, let n be the index of
the first state more than t time units
away from the current state
Conjunction of n conjuncts c1 through
cn, each of size i
Simplifies if 1 or 2, or both, do not
contain any probabilistic statements
Example

Verify Pr0.05(true U200 dead) in S1
E5 S4
6
4
S1
E1
E4
S3 E2
E3
S2 E2
2
S1:
S2:
S3:
S4:
20
Safe, at rest
Under attack, at rest
Under attack, jumping
Safe, jumping
40
60
80
100
E1: Stork
attacking
E1: 89.9
26.3
59.4
E2: E-2: Frog
124.5 killed
155.8
107.5
80.2
E3: E- : Start
44.3 jumping
48.3
E4:
-3
61.0
95.2
E
:
Stork
retreats
E5:
-4
36.2
t: 0.0
26.3 jumping
89.9
138.2
70.6 199.2
150.8 235.4
E5: Stop
Summary




Algorithm for probabilistic verification of
discrete event systems
Sample execution paths generated
using discrete event simulation
Probabilistic properties verified using
acceptance sampling
Algorithm can be used in an anytime
manner
Future Work



Apply to hybrid dynamic systems
Develop heuristics for formula ordering
and parameter selection
Use verification to aid policy generation
for real-time stochastic domains