Transcript Model Checking for Probabilistic Timed Systems

Model Checking Durational
Probabilistic Systems
Jeremy Sproston
Università di Torino
Joint work with François Laroussinie
LSV, ENS de Cachan & CNRS UMR 8643
Institut d’Informatique, FUNDP, Namur
30/5/2005
1
Verifying probabilistic timed systems
• Real-time systems:
– Quantitative information along paths
– E.g. time-out occurs 30ms after a request
• Probabilistic systems:
– Quantitative information between paths
– E.g. the packet is lost with probability 0.01
• In some systems, timing and probabilistic behaviour co-exist
– Multimedia equipment, communication protocols, fault-tolerant
systems
2
Verifying probabilistic timed systems
• Aim: verify probabilistic timed systems
– Properties: a request is followed by a response within 5ms with
probability 0.99 or greater (soft deadlines)
• System description formalism:
– Durational probabilistic systems
• Property description formalism:
– PTCTL (Probabilistic Timed CTL)
– E.g.: request  P0.99(true U5 response)
• Model checking
– Focus on complexity issues
3
Context
• Hansson and Jonsson [FACS94]:
– Fully probabilistic systems
– State-to-state transition corresponds to 1 time unit
– Probabilistic timed temporal logic
• De Alfaro [STACS97]:
– Probabilistic-nondeterministic systems
– State-to-state transition corresponds to 0 or 1 time units
– Probabilistic timed temporal logic
• Other work:
– De Alfaro [CONCUR98, PhD thesis]
– Andova et al. [FORMATS2003]
– Kwiatkowska et al. [TCS2002] (PTCTL, probabilistic timed
automata)
– Baier et al. [IEEE TSE2003]
4
Fully probabilistic systems
fail
1
idle
0.01
try
s0
1
s1
0.01
0.98
s3
succ
s2
1
State-to-state transition:
probabilistic choice of target
state according to the probability
distribution over the state’s
outgoing transitions.
• Fully probabilistic system: FPS = (S,sinit,P,lab)
– S is a set of states with initial state sinit
– P: S x S  [0,1] is a probabilistic transition matrix such
that s’ P(s,s’)=1 for all s
– lab: S  2AP is a state labelling function
5
Markov decision processes
fail
1
idle
0.02
try
s0
1
s1
1
0.98
s3
succ
s2
1
State-to-state transition:
1. Nondeterministic choice
over the outgoing probability
distributions of the source state
2. Probabilistic choice of target
state according to the
distribution chosen in step 1.
• Markov decision process: MDP = (S,sinit,,lab):
– S is a set of states with the initial state sinit
–   S x Dist(S) is a probabilistic transition relation
(elements are (s, ), for state s and distribution  over
states)
– lab: S  2AP is a state labelling function
6
Markov decision processes
fail
1
idle
0.02
try
s0
1
s1
1
0.98
s3
succ
s2
1
State-to-state transition:
1. Nondeterministic choice
over the outgoing probability
distributions of the source state
2. Probabilistic choice of target
state according to the
distribution chosen in step 1.
• The coexistence of nondeterministic and
probabilistic choice means that there may be no
unique probability of certain behaviours
• For example, we obtain the minimum and maximum
probabilities of reaching a set of states
7
Probabilistic CTL
• Extend classical logics for model checking to
reason about probabilistic behaviour
• Probabilistic CTL (PCTL)
– FPSs: Hansson and Jonsson [FAC94]
– MDPs: Bianco and de Alfaro [FSTTCS95]
– CTL with universal/existential path quantifiers replaced
by a probabilistic path quantifier
– This quantifier compares probability of exhibiting
particular set of behaviours with a probability threshold
8
Probabilistic CTL
• For example:
– CTL: (safe U completed)
• For all paths, the system will be safe until it has completed
a task
– PCTL on fully prob. systems: P 0.9(safe U completed)
• With probability 0.9 or greater, the system will be safe
until it has completed a task
– PCTL on Markov decision proc.s: P 0.9(safe U completed)
• For all ways of resolving nondeterministic choice, then with
probability 0.9 or greater, the system will be safe until it
has completed a task
9
PCTL model checking
• For finite-state FPSs/MDPs, by induction on
structure of formula, as for CTL
• “Quantitative Until” (arbitrary probability), solve
–
–
–
–
Recursive linear equation (FPSs) [HJ94,CY95]
Linear optimisation problem (MDPs) [BdA95]
Polynomial time algorithms
In practice: typically iterative solution methods
• “Qualitative Until” (probability 1, 0): proceed by
graph traversal [Vardi85]
10
Modelling (discrete) time
• If state-to-state transitions take 0 or 1 time
units, how to model a time-out of 100 time units?
100 transitions
…
• Blow-up in the state space is proportional to the
timing constraints of the system
11
Modelling (discrete) time
• If timing constraints are represented in binary, the size of
the state space is exponential in the size of timing
constraints
• Can we avoid this?
– Precedent for non-probabilistic timed systems: polynomial-time
model checking for some timed temporal logic formulae
(Laroussinie-Markey-Schnoebelen [FOSSACS2002])
• Aim: model checking algorithm for probabilistic timed
systems which is polynomial in the size of the system
12
Durational probabilistic systems
Revised
draft
New
idea
Draft
written
Submission
Notif.
reject
Draft
written
Submission
Notif.
accept
Publication
Final
version
13
Durational probabilistic systems
Revised
draft
[2,10]
[0,30]
[31,60]
Draft [0,60] Sub- [25,50]
written
mission [25,50]
Notif.
reject
[7,30]
[25,50]
Draft [0,30] Subwritten
mission [25,50]
Notif.
accept
New
idea
[0,100]
Publi- [50,110] Final
cation
version
[10,28]
14
Durational probabilistic systems
Revised
draft
[2,10]
[0,30]
[31,60]
New
idea
Draft [0,60] Sub- [25,50]
written
mission
0.3
0.7
0.5
[7,30]
[0,100]
Draft [0,30] Subwritten
mission [25,50]
Publi- [50,110] Final
cation
version
0.5
Notif.
reject
Notif.
accept
[10,28]
15
Durational probabilistic systems (DPS)
• Durational probabilistic system (Q,qinit,D,L)
– Q - finite set of states
– qinit – initial state
– D  Q x I x Dist(Q) – transition relation with
duration and probabilistic branching
– L: Q  2AP – labelling function
• I is the set of finite intervals [n,m] (n,mnaturals)
• Dist(Q) is the set of probability distributions over Q
• AP is the set of atomic propositions
16
Semantics of DPSs
• Transition of a DPS: (q,[n,m],)  D
– From state q, let d time units elapse (where d  [n,m]),
then select the next state probabilistically using the
distribution 
• Semantics of DPSs: timed Markov decision
processes (S,sinit,,lab)
– S – finite state space, with initial state sinit
–   S x Naturals x Dist(S)
(e.g. (s,d,))
– lab: S  2AP
• Assume that in every loop in the graph of the DPS,
at least 1 time unit must elapse
17
Semantics of DPSs
• Jump semantics: a transition takes exactly d time
units, and there are no intermediate states
0.5
0.5
Subq1
mission
[1,3]
0.5
DPS
Notif.
q2
reject
Notif.
q3
accept
(2)
0.5
0.5
Subq1
mission
(3)
Jump
semantics
Notif.
q2
reject
(1)
0.5
Notif.
q3
accept
0.5
0.5
18
Semantics of DPSs
• Continuous semantics: represent intermediate
states explicitly; transitions have duration 1 (or 0)
(q1,0)
0.5
Subq1
mission
[1,3]
0.5
DPS
Notif.
q2
reject
(1)
(q1,1)
Notif.
q3
accept
(1)
0.5
0.5
(1)
0.5
0.5
(1)
0.5
(q1,2)
0.5
(1)
Continuous
semantics
(q2,0)
(q3,0)
19
Semantics of DPSs
• Consider the jump semantics of a DPS
– The number of states of the jump semantics = number of
states of the DPS
– The number of transitions of the jump semantics is
exponential in the (binary) encoding of the timing
constraints
• Consider the continuous semantics of a DPS
– The number of states and transitions of the continuous
semantics is exponential in the (binary) encoding of the
timing constraints
20
PTCTL
• Probabilistic Timed CTL: a probabilistic and timed
extension of CTL
– Based on PCTL and TCTL (Emerson et al. [Real-Time
Systems92], Alur-Courcoubetis-Dill [I&C93])
• Includes P#(1 Uc 2)
– Probabilistically quantified, timed until operator
– Where #{<,,,>}, [0,1], {<,,=,,>}, c is a natural,
and 1, and 2 are PTCTL formulae
21
PTCTL
Example of the probabilistic timed until operator:
• P(1 Uc 2) – the probability of reaching a 2state via 1-states before c time units have
elapsed is at least 
• Probability must be at least  no matter how the
nondeterministic choice of the DPS is resolved
• A request is followed by a response within 5ms
with probability 0.99 or greater
request  P0.99(true U5 response)
22
Model checking DPSs
• First attempt: define the jump/continuous
semantic TMDP of a DPS, and model check it
• Require PTCTL model-checking algorithm for
TMDPs
• E.g. for P(1 Uc 2): for each state, want to
compute the minimal probability of 1 Uc 2
– For each state, compute f(s,i), the minimal probability of
1 Ui 2 for all ic
– Linear optimisation problem:
f(s,i) := min(s,d,)
s’ S (s’) . f(s’,i-d)
23
Model checking DPSs
• Repeat similar idea for all PTCTL operators
• Model checking the PTCTL formula  for
the TMDP M=(S,sinit, ,lab) runs in time
O(|| . ((|S| . || . cmax) + poly(|M|)))
where cmax is the largest timing constraint
used in the formula 
24
Model checking DPSs
• Now model check the jump/continuous semantic
TMDP of the DPS?
• Jump semantics: || is exponential in the size of
the timing bounds used in the DPS
• Continuous semantics: |S| and || are exponential
in the size of the timing bounds used in the DPS
• But we can obtain solutions which are independent
of the magnitude of the DPS’s timing constraints
for the fragment of PTCTL in which timesubscripts using =c are disallowed (PTCTL[,])
25
Model checking DPSs
• Solution for the jump semantics:
– Represent the TMDP transitions for the leftand right-endpoints of timing intervals only
– This is sufficient for verifying PTCTL (either
go “as fast as possible” or “as slow as possible”)
0.5
Subq1
mission
DPS
Notif.
q2
reject
Notif.
q3
accept
q2
0.5
q1
[1,300]
0.5
(1)
0.5
(300)
Jump
semantics
0.5
0.5
q3
26
Model checking DPSs
• Solution for the continuous semantics:
– Consider P(1 Uc 2)
– Partition the state space according to the
following general principles:
• States are distinguished on whether they satisfy 1
or not; similarly with 2
• States are distinguished on whether a particular DPS
transition can be taken or not
– The number of classes in the resulting partition
is polynomial in the size of the DPS and the size
of P(1 Uc 2)
27
Model checking DPSs
• Solution for the continuous semantics
(continued):
– Construct a TMDP from the partition
• States = classes of the partition
• Transitions: derived from the DPS
– The TMDP suffices for model checking PTCTL
against the continuous semantics
28
Model checking DPSs
• Model checking the PTCTL formula  for
DPS = (Q,qinit,D,L) runs in time:
– Jump semantics
O(|| . ((|Q| . |D| . cmax) + poly(|DPS|)))
– Continuous semantics:
O((||3 . |D|3 . cmax) + poly(|| . |D| . |DPS|)))
29
Model checking DPSs
• Considered model checking of DPSs against
PTCTL[,] formulae
– Polynomial time in the size of the DPS, but
exponential in the size of the timing constraints
of the formula
• Can we do any better?
– What are the lower bounds on the complexity
of model checking PTCTL[,]?
30
NP-hardness of P(Fc p)
• Consider P(Fc p)
– p is an atomic proposition
– (Fc p) is an abbreviation for (true Uc p)
• K-th largest subset problem (NP-hard problem):
– Finite set A = {a1, …, an} of natural numbers
– Two integers K and B
– Problem: do there exist at least K distinct subsets A’  A
such that:

aA’
aB
31
NP-hardness of P(Fc p)
• Consider an instance of the K-th largest subset problem,
with {a1, …, an}, K and B
• Consider the following DPS
[a1,a1]
0.5
q0
[0,0]
0.5
q1
[a2,a2]
0.5
[0,0]
0.5
q2
[an,an]
0.5
…
qn-1
[0,0]
0.5
qn
• The only state labelled by p is qn
• Let =K/2n
• Then q0 satisfies P  (FB p) if and only if the instance of
K-th largest subset is positive
32
Complexity overview
Fully prob. DPS
Jump
Continuous
PTCTL0/1[,]
PTCTL0/1
•
•
•
Jump
Continuous
P-complete
P-complete
P-hard
in PSPACE
P-hard
in EXPTIME
2p-complete
PSPACEcomplete
PSPACE-hard
in EXPTIME
PSPACE-hard
in EXPTIME
NP-hard and coNP-hard
in EXPTIME
PTCTL [,]
PTCTL
DPS
2p-hard
in EXPTIME
PSPACE-hard
in EXPTIME
PSPACE-hard
in EXPTIME
PSPACE-hard
in EXPTIME
PTCTL0/1: fragment of PTCTL with probability bounds 0 or 1 only
Fully probabilistic DPS: with no nondeterministic choice
Results in blue have a polynomial time algorithm in the size of the
DPS
33
Conclusions
• Obtained an algorithm running in polynomial time in
the description of the DPS for PTCTL [,]
• General picture of complexity results needs to be
completed
• Not considered in this talk: average-time-to-reach
operator
– Solution combines jump/continuous semantics
constructions with the polynomial average-to-time-reach
algorithm of de Alfaro [CONCUR98, PhD thesis])
• Applications to related models in continuous time:
– Probabilistic timed automata
– Continuous-time Markov decision processes
34
PCTL model checking of FPSs
• Obtaining the characteristic set Sat(.):
– Sat( P (1 U 2) ) =
{s  S | xs  }
where xs for all s  S, are obtained from the recursive
linear equation
xs =
Syes)
0
1
s’  S P(s,s’) . xs’
if s  Sno
if s  Syes
if s  S\(Sno 
and
Syes – states that satisfy 1 U 2 with probability exactly 1
Sno - states that satisfy 1 U 2 with probability exactly 0
35
PCTL model checking of MDPs
• The linear equation generalises to linear
optimisation problems solvable iteratively, e.g.
– Sat( P (1 U 2) )
xs =
=
{s  S | xs  }
0
if s  Sno
1
if s  Syes
min  Steps(s) s’  S (s’) . xs’ if s  S\(Sno  Syes)
and
Syes – states that satisfy 1 U 2 with min. prob. exactly 1
Sno - states that satisfy 1 U 2 with min. prob. exactly 0
36
PCTL model checking of MDPs
• The linear equation generalises to linear
optimisation problems solvable iteratively, e.g.
– Sat( P (1 U 2) )
xs =
Syes)
=
{s  S | xs  }
0
if s  Sno
1
if s  Syes
max  Steps(s) s’  S (s’) . xs’ if s  S\(Sno 
and
Syes – states that satisfy 1 U 2 with max. prob. exactly 1
Sno - states that satisfy 1 U 2 with max. prob. exactly 0
37
PCTL model checking of MDPs
• The linear equation generalises to linear
optimisation problems solvable iteratively, e.g.
– Sat( P (1 U 2) )
xs =
Syes)
=
{s  S | xs  }
0
if s  Sno
1
if s  Syes
max  Steps(s) s’  S (s’) . xs’ if s  S\(Sno 
• Cases for <, > follow similarly
38
PTCTL
•
•
•
•
Atomic propositions (New idea, Submission etc.)
Boolean connectives
P#(X ) – probabilistically quantified next operator
P#(1 Uc 2) – probabilistically quantified, timed until
operator
• D#() – average-time-to-reach operator
where #{<,,,>}, [0,1], {<,,=,,>}, c is a natural,  is a
non-negative real, and , 1, and 2 are PTCTL formulae
• Probabilistic quantifiers: Hansson and Jonsson 1994, Bianco
and de Alfaro 1995
• Average-time-to-reach operator: de Alfaro 1997
39