VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 58–73
Towards Model-checking Probabilistic Timed
Automata against Probabilistic Duration PropertiesI
Van Hung Dang1;, Miaomiao Zhang2, Dinh Chinh Pham1
1 VNU University of Engineering and Technology, Hanoi, Vietnam
2School of Software Engineering, Tongji University, Shanghai, China
Abstract
In this paper, we consider a subclass of Probabilistic Duration Calculus formula called Simple Probabilistic
Duration Calculus (SPDC) as a language for specifying dependability requirements for real-time systems, and
address the two problems: to decide if a probabilistic timed automaton satisfies a SPDC formula, and to decide
if there exists a strategy of a probabilistic timed automaton satisfies a SPDC formula.
We prove that the both
problems are decidable for a class of SPDC called probabilistic linear duration invariants, and provide model
checking algorithms for solving these problems.
Received 25 November 2015, revised 20 December 2015, accepted 31 December 2015
Keywords:
Probabilistic Duration Calculus, Probabilistic Timed Automata, Model-checking,
Markov Decision Process.
1. Introduction
developed by Dimitar Guelev [5],
and in [6]
we have shown that the calculus is useful for
In 1992, Chaochen Zhou, Hoare C.A.R and
reasoning about QoS contracts in component-
Anders Ravn introduced Duration Calculus [1]
based real-time systems.
as a logic for reasoning about real-time systems.
The calculus has attracted a great deal of
attention, and was then developed further in
many other works because of its rich meanings.
Many of those works have been summarized
in the monograph [2]. For specifying the
dependability of real-time systems, a kind of
probabilistic extension of Duration Calculus has
been introduced in [3, 4]. No rigorous syntax has
been introduced in these papers, and the authors
just focused on the development of techniques
for reasoning instead of the ones for checking.
A version with a proof system of Probabilistic
Duration Calculus with infinite interval was then
For Duration Calculus, some techniques for
checking if a timed automaton satisfies a duration
calculus formula written in the form of linear
duration invariants have been developed [7, 8,
9, 10, 11, 8]. However, to our knowledge,
not many works have been done for checking
if a probabilistic real-time system satisfies a
PDC formula. This is, perhaps, because in
the model of probabilistic systems, there is too
much randomization and nondeterminism, and
this makes model checking too complicated.
Kwiatkowska et al in [12, 13] proposed a
variant of probabilistic timed automata that
allows probabilistic choice only at discrete
I ThisresearchwasfundedbyVietnamNationalFoundation
for Science and Technology Development (NAFOSTED)
under grant number 102.03-2014.23.
 Corresponding author. Email: dvh@vnu.edu.vn
transitions. To resolve the nondeterminism
between the passage of time and discrete
transitions they used the concept of strategy
which is essentially a deterministic schedule
58
P
V. H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 58–73
59
policy.
Then,
the
set
of
executions
of
a
reachability graph of the timed automaton. Then,
probabilistic
timed
automaton
according
to
a
we generalize this technique to achieve our goal
strategy forms a Markov chain, and hence the
with a model-checking algorithm.
satisfaction of a probabilistic timed CTL formula
The first version of this paper was published
by this set can be defined, and then based on
in [14].
In this extended version, in addition to
the
region
graph
of
the
timed
automaton
the
the problem of verification, we formulate also
satisfaction of a probabilistic timed CTL formula
the problem of strategy synthesis, i.e.
to decide
by the timed automaton can be also verified.
if there is a strategy for a probabilistic timed
The idea of fixing a strategy when studying the
automaton
that
satisfies
a
probabilistic
linear
probabilistic behavior of a probabilistic timed
duration invariant and show that this problem is
automaton restricts the scope of the verification
also solvable.
We provide all proof details and
problem
significantly,
making
the
checking
algorithms for doing model-check.
problem more tractable.
Then,
verifying the
Our paper is organized as follows.
In the
set of all strategies against a given probabilistic
next section we present the Probabilistic Timed
property can be done by searching for the “worst
Automata
model.
Section
3
presents
syntax
case”
strategy
according
to
the
probabilistic
and semantics of our PDC. Our main results is
propertyandthenapplytheverificationtechnique
presented in Section 4 where we formulate our
toit. Thisideaisamotivationforustoreconsider
model checking problem and give our solution to
the
problem
of
checking
a
probabilistic
it. The last section is the conclusion of the paper.
timed
automaton
for
a
PDC
formula
that
we gave up before.
In this paper, we introduced a simple
probabilistic extension of DC called Probabilistic
Duration Calculus for specifying dependability
requirements of real-time systems. The extension
is conservative in the sense that a formula of
DC is also a formula of PDC with semantics
adapted to probabilistic domain. PDC also
consists of formulas representing the constraints
2. Probabilistic Timed Automata
In this section, we recall the concepts
of probabilistic timed automata model and
probabilistic timed structure as its semantics
from [15, 12]. We use a simple model of
gas burners to illustrate the concepts as its
requirement specification is a typical example for
time duration properties.
for
the
probability
of
the
satisfaction
of
a
Probability distributions and Markov decision
DC
formula
by
a
strategy
for
an
interval.
processes.
A discrete probability distribution
We
use
the
behavioral
model
proposed
by
over a set S is a mapping p : S
! [0;1] such
Kwiatkowska et al to define the semantics of
our logic. Since probabilistic timed CTL and
PDC are not comparable, and since for many
that the set fs j s 2 S and p(s) > 0g is finite, and
s2S p(s) = 1. The set of all discrete probability
distributions over S is denoted by (S).
probabilistic properties PDC is more convenient
A
Markov
decision
process
is
a
tuple
to
specify,
a
model
checking
technique
for
(Q;Steps),
where
Q
is
a
set
of
states,
and
checking
probabilistic
timed
automata
against
Steps
:
Q
!
2(Q)
is a function assigning
PDC properties is useful. To solve this problem,
a set of probability distributions to each state.
wefirstdevelopatechniquetodecideifastrategy
The
intuition
is
that
the
Markov
decision
in
a
probabilistic
timed
automaton
satisfies
a
process
traverses
the
state
space
by
making
PDC formula of a certain form.
This technique
transitions determined by Steps: in a state s, the
is
essentially
an
extension
of
our
technique
process selects nondeterministically a probability
developed earlier in [10, 9] to check if a timed
distribution
p
in
Steps(s),
and
then
makes
a
automaton satisfies a DC formula in the form
probabilistic choice according to p as to which
of linear duration invariants or discretisable DC
state to move to.
As in [12] we label the action
formulas
based
on
searching
in
the
integral
selecting a probability distribution with a letter
a;p
l
l l
0
1 2
l
l l
0
1 2
l
l l
0
1 2
0
1 2
0
l
l
l
l l
0
0
1
1 2
1
l
2
2
60
V. H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 32, No. 1 (2016) 58–73
from , and assume that Steps : Q ! 2(Q) and
on all other clocks. For t 2 R0, we write  + t
 is a set of actions. The intuition now becomes
fortheclockvaluationthatassigns(x)+t toeach
that the Markov decision process traverses the
clock x 2 C. A constraint over C is an expression
state space by making transitions determined by
of the form xi  c or xi xj  c, where i ,
j,
Steps:
in a state
s,
the process performs an
i; j  n and 2 f<;;>;g and c 2 N. A clock
action a
2
 selecting nondeterministically a
valuation  satisfies a clock constraint xi

c
probability distribution p in Steps(s), and then
(xi xj  c) i (xi)  c ((xi) (xj)  c). A
makes a probabilistic choice according to p as to
which state to move to. So, a transition is of the
form s ! s0, where (a; p) 2   (Q) is the
zoneofCisaconvexsubsetofthevaluationspace
(R0)C described by a conjunction of constraints.
For a zone  and a set of clocks X  C the set
label of the transition. We also assume a labeling
f[X := 0] j  2 g is also a zone, and is denoted
function L
:
Q
!
2AP, where AP is a set of
by [X := 0]. Let ZC denote the set of all zones
atomic propositions, that associates a state s with
of C.
the set of atomic propositions that hold at state
s. Then, a labeled Markov decision process is
a tuple (Q;Steps;L).
Labeled paths (or execution sequences)
are nonempty finite or infinite sequence of
consecutive transitions of the form
Probabilistictimedautomataandprobabilistic
timed structures. Timed automata were
introduced in [16] as a model of real-time
systems. They are extended with discrete
probability distribution to model probabilistic
real-timesystems. Inthesequel,let APbeagiven
!
=
s0 ! s1 ! s2 ! :::;
set of atomic propositions.
where si arestatesandli arelabelsfortransitions.
For a path !, let first(!) denote the first state
of !, and if ! is finite then let last(!) denote
Definition 1. A probabilistic timed automaton
(PTA) is a tuple G = (S;L;s¯;C;inv; prob;
hsis2S) consisting of
the last state of !. j!j is the length of ! and is
defined as the number of transition occurrences
in ! which is 1 if ! is infinite. For k  j!j,
 a finite set S of nodes, a start node s¯ 2 S, a
finite set C of clocks,
let !(k) denote the kth state of !, and step(!;k)
denote the label of the kth transition in !. For
two paths ! = s0 ! s1 ! s2 ! :::sn
0 0 0
and !0 = s0 ! s0 ! s0 ! ::: such that
sn = s0, the concatenation of ! and !0 is defined
0 0
as !!0 = s0 ! s1 ! s2 ! :::sn ! s0 !
0
s0 ! :::.
Clocks,clockvaluations,clockconstraints. Let
R0 denote the set of non negative real numbers.
 a function L : S ! 2AP assigning to
each node of the automaton a set of atomic
propositions that are supposed to be those
that are true in that node, a function inv :
S ! ZC assigningtoeachnodeaninvariant
condition,
 a function prob : S ! 2(S2C) assigning
to each node a set of discrete probability
distributions on S2C,
A clock is a real-valued variable which increases
at the same rate as real time. Let C = fx1 :::;xng
be a set of clocks. A clock valuation is a function
 : C ! R0 that assigns a real value to each
clock. Let (R0)C denote the set of all clock
 a family of functions hsis2S where, for any
s 2 S, s : prob(s) ! ZC assigns to each
p 2 prob(s) an enabling condition.
The last item in the definition says that all the
valuations, and 0 denote the clock valuation that
probabilistic choices according to a probabilistic
assigns 0 to each clock in C. For a set of clocks
distribution (selected at a node) have the same
X  Cwedenoteby[X := 0]theclockvaluation
enabling
condition.
The
probabilistic
timed
that assigns 0 to all clocks in X and agrees with 
automaton behaves nearly in the same way as a

Towards Model-checking Probabilistic Timed Automata against Probabilistic Duration Properties

Đăng ngày | Thể loại: | Lần tải: 0 | Lần xem: 0 | Page: 16 | FileSize: M | File type: PDF
0 lần xem

Towards Model-checking Probabilistic Timed Automata against Probabilistic Duration Properties. In this paper, we consider a subclass of Probabilistic Duration Calculus formula called Simple Probabilistic Duration Calculus (SPDC) as a language for specifying dependability requirements for real-time systems, and address the two problems: to decide if a probabilistic timed automaton satisfies a SPDC formula, and to decide if there exists a strategy of a probabilistic timed automaton satisfies a SPDC formula.. Giống các tài liệu khác được bạn đọc chia sẽ hoặc do tìm kiếm lại và giới thiệu lại cho các bạn với mục đích tham khảo , chúng tôi không thu tiền từ bạn đọc ,nếu phát hiện tài liệu phi phạm bản quyền hoặc vi phạm pháp luật xin thông báo cho chúng tôi,Ngoài tài liệu này, bạn có thể download tài liệu, bài tập lớn phục vụ học tập Có tài liệu download mất font không xem được, thì do máy tính bạn không hỗ trợ font củ, bạn download các font .vntime củ về cài sẽ xem được.

Nội dung


1134924

Tài liệu liên quan