Exact and Approximate Abstraction for Classes ofStochastic Hybrid Systems


Electronic Communications of the EASST
Volume 70 (2014)

Proceedings of the
14th International Workshop on

Automated Verification of Critical Systems (AVoCS 2014)

Exact and Approximate Abstraction for Classes of
Stochastic Hybrid Systems

Jeremy Sproston

15 pages

Guest Editors: Marieke Huisman, Jaco van de Pol
Managing Editors: Tiziana Margaria, Julia Padberg, Gabriele Taentzer
ECEASST Home Page: http://www.easst.org/eceasst/ ISSN 1863-2122

http://www.easst.org/eceasst/


ECEASST

Exact and Approximate Abstraction for Classes of
Stochastic Hybrid Systems

Jeremy Sproston∗

Dipartimento di Informatica, University of Turin, Italy

Abstract: A stochastic hybrid system contains a collection of interacting discrete
and continuous components, subject to random behaviour. The formal verification
of a stochastic hybrid system often comprises a method for the generation of a
finite-state probabilistic system which either represents exactly the behaviour of the
stochastic hybrid system, or which approximates conservatively its behaviour. We
extend such abstraction-based formal verification of stochastic hybrid systems in
two ways. Firstly, we generalise previous results by showing how bisimulation-
based abstractions of non-probabilistic hybrid automata can be lifted to the set-
ting of probabilistic hybrid automata, a subclass of stochastic hybrid systems in
which probabilistic choices can be made with respect to finite, discrete alternatives
only. Secondly, we consider the problem of obtaining approximate abstractions for
discrete-time stochastic systems in which there are continuous probabilistic choices
with regard to the slopes of certain system variables. We restrict our attention to
the subclass of such systems in which the approximate abstraction of such a system,
obtained using the previously developed techniques of Fränzle et al., results in a
probabilistic rectangular hybrid automaton, from which in turn a finite-state proba-
bilistic system can be obtained. We illustrate this technique with an example, using
the probabilistic model checking tool PRISM.

Keywords: Probabilistic verification, stochastic hybrid systems, bisimulation

1 Introduction

Our increasing reliance on complex embedded and cyber-physical systems calls for the develop-
ment of methods for the verification of hybrid systems, which are systems in which behaviour is
described as an interplay between discrete and continuous components. In this paper, we con-
sider a well-known formalism for the description of hybrid systems, namely hybrid automata
[ACH+95], which comprise a finite-state graph, to represent the discrete part of the system, and
a finite set of real-valued variables, to represent the continuous part of the system. Interaction be-
tween the discrete and continuous parts of the system is represented by labelling the graph with
conditions on the variables and their first derivatives. Hence we can express that, as time passes
and the system resides in a particular node of the graph, the rate of change of the variables is de-
scribed in a certain way; we can also describe how the system moves from node to node when the

∗ Supported by the project AMALFI (University of Turin/Compagnia di San Paolo), the MIUR-PRIN project CINA,
and the EU ARTEMIS Joint Undertaking under grant agreement no. 332933 (HoliDes).

1 / 15 Volume 70 (2014)



Abstraction for Stochastic Hybrid Systems

lon
ẋ ∈ [1, 6], ẏ = 1

10 ≤ x ≤ 25

loff
ẋ ∈ [−4,−1], ẏ = 1

10 ≤ x ≤ 30

lmalf
ẋ ∈ [1, 6], ẏ = 1

10 ≤ x ≤ 30, y ≤ 20

ldeact
ẋ = 0, ẏ = 1
10 ≤ x ≤ 30

x ≥ 20
x ≤ 15

y′ = 0
1

10

9
10

x ≥ 26

y = 20

Figure 1: A probabilistic hybrid automaton modelling a faulty thermostat

value of the variables satisfies certain conditions. Hybrid automata can be subject to automatic
verification procedures, which have been implemented in a number of tools [HHW97, Fre08].

In many contexts, a representation of a hybrid system without information regarding the likeli-
hood of its various behaviours is insufficient. For example, a verification method for a particular
hybrid system may show the existence of a behaviour corresponding to an error or to a decrease
in performance, but without representing the fact that the behaviour is unlikely to occur. This ob-
servation has led to a number of formalisms for stochastic hybrid systems, in which the likelihood
of behaviours is represented, for example [HLS00, Spr00, Buj04, APLS08, FHH+11, Hah13].
In particular, probabilistic hybrid automata [Spr00] extend hybrid automata by associating prob-
abilities with edges of the graph. Stochastic hybrid automata [FHH+11, Hah13] extend proba-
bilistic hybrid automata by allowing the values of the continuous variables to be reset according
to continuous probability distributions.

An example of a probabilistic hybrid automaton modelling a faulty thermostat is shown in
Figure 1 (the model is a modification of an example of [Spr11]). We use a number of the usual
conventions for illustrating hybrid automata, and refer to the nodes of the graph as locations. The
ambient temperature is represented by the variable x, and variable y is a timer. When the heater
is on (location lon or location lmalf ), the temperature increases at a rate between 1 and 6; when the
heater is off (location loff ), the temperature changes at a rate between -4 and -1. The locations lon
and loff corresponds to non-faulty behaviour, whereas the location lmalf corresponds to the heater
being on in the presence of a fault in the temperature sensor that means that the measurement of
the temperature is temporarily unavailable. The system passes from lon to loff , with probability 1,
when the temperature is between 20 and 25, and from loff to lon, with probability

9
10 , or to lmalf ,

with probability 110 , when the temperature is between 10 and 15. The sensor fault means that
the temperature can increase to a higher level in lmalf than in lon. After a malfunction, either the
system is deactivated if the temperature reaches an excessive level (location ldeact), or the system
times-out exactly 20 time units after the location lmalf was entered, in which case the heater is
switched off. All edges of the probabilistic hybrid automaton correspond to reaching a certain
location with probability 1, apart from the probabilistically branching edge from loff .

Two main approaches for the verification of probabilistic and stochastic hybrid automata have
been presented. On the one hand, exact methods generally consider the construction of a finite-
state probabilistic system (more precisely, a probabilistic automaton or a Markov decision pro-

Proc. AVoCS 2014 2 / 15



ECEASST

cess [Put94]) that represents faithfully the behaviour of the original system. This approach has
been adopted for restricted subclasses of probabilistic hybrid automata in [Spr00, Spr11] using
probabilistic bisimulation [LS91, SL95] to obtain a finite number of equivalence classes from
which a finite-state system can be constructed. On the other hand approximate methods con-
sider generally the construction of a finite-state probabilistic system that overapproximates the
behaviour of the original system. This approach has been adopted for probabilistic hybrid au-
tomata in [Spr01, ZSR+12], and for stochastic hybrid automata in [FHH+11, Hah13].

The contributions of this paper are twofold. First, in Section 2, we generalise the results of
[Spr00, Spr11] concerning exact verification methods. Any probabilistic hybrid automaton can
be translated into a non-probabilistic hybrid automaton in which information concerning prob-
ability distributions is encoded in labels on edges of the graph. Consider a probabilistic hybrid
automaton H : we show that if the non-probabilistic hybrid automaton counterpart of H has
a finite bisimulation equivalence quotient, then H has a finite probabilistic bisimulation equiv-
alence quotient. This result unifies and generalises previous results, and has the consequence
that we can identify classes of probabilistic hybrid automata with a finite bisimulation equiva-
lence quotient on the basis of whether members of the corresponding class of hybrid automata
have finite bisimulation quotients. For example, we can conclude that the class of probabilistic
STORMED hybrid automata, which are probabilistic hybrid automata to which the restrictions
of STORMED hybrid automata [VPVD08] apply to the non-probabilistic characteristics of the
system, have a finite probabilistic bisimulation quotient, because STORMED hybrid automata
have finite bisimulation equivalence quotients. Any future results on the identification of classes
of hybrid automata with finite bisimulation quotients will also imply that the corresponding class
of probabilistic hybrid automata has finite probabilistic bisimulation quotients.

The second contribution, in Section 3, concerns approximate verification methods. In stochas-
tic hybrid automata, the rate of change of continuous variables as time passes is not (directly)
chosen probabilistically. However, the rate of change of a continuous variable x may be equal to
the value of another continuous variable y (that is, ẋ = y), and y could be subject to a reset by
a continuous probability distribution: hence, the rate of change of x is indirectly dependent on
a continuous probabilistic choice. We consider this approach in the context of stochastic hybrid
automata and the approximation method of [FHH+11, Hah13], which uses probabilistic hybrid
automata as approximate models of stochastic hybrid automata. We show that there exists a
class of probabilistic hybrid automata that features dependence of variable’s rate of change on
the value of other variables (where these variables are constant as time passes) that is equiv-
alent to probabilistic rectangular automata, a subclass of probabilistic hybrid automata which
has a finite probabilistic bisimulation equivalence quotient when considering a discrete-time se-
mantics [Spr11]. We apply this approach to the case of the faulty thermostat of Figure 1: for
example, when the heater is on, rather than increase nondeterministically with a rate in [1, 6],
we consider that the rate of increase of the temperature is chosen from the normal distribution
with mean 3.5 and standard deviation 1, truncated to the interval [1, 6]. This continuous distri-
bution is approximated according to the approach of [FHH+11, Hah13], which then results in
an intermediate probabilistic hybrid automaton that we can show is equivalent to a probabilistic
rectangular automaton, which (assuming a discrete-time semantics) can then be transformed into
a finite-state probabilistic system, which is then analysed using the probabilistic model check-
ing tool PRISM [KNP11]. We show that there is a significant difference in the results obtained

3 / 15 Volume 70 (2014)



Abstraction for Stochastic Hybrid Systems

from the probabilistic rectangular automaton in Figure 1 and from the probabilistic rectangular
automaton obtained as an approximation of an automaton involving continuous distributions, as
described above.

2 Exact Abstraction of Probabilistic Hybrid Automata

2.1 Preliminaries

We use R to denote the set of real numbers, R≥0 to denote the set of non-negative real num-
bers, Z to denote the set of integers, N to denote the set of natural numbers and Q to denote the
set of rational numbers. Given a set Q and a function µ : Q → R≥0, we define support(µ) =
{q ∈ Q | µ(q) > 0}. A (discrete) probability distribution over a countable set Q is a function
µ : Q → [0, 1]∩Q such that ∑q∈Q µ(q) = 1. Let Dist(Q) be the set of distributions over Q. If
Q is an uncountable set, we define Dist(Q) to be the set of functions µ : Q → [0, 1], such that
support(µ) is a countable set and µ restricted to support(µ) is a (discrete) probability distribu-
tion. Occasionally we use notation {q1 7→ λ1, ..., qn 7→ λn} to denote a distribution µ for which
µ(q1) = λ1, ..., µ(qn) = λn. Given a set Q′ ⊆ Q, we let µ[Q′] = ∑q∈Q′ µ(q).

A probabilistic automaton (PA) P = (S, Act,⇒) comprises the following components: a set
of states S; a set of actions Act; and a probabilistic, nondeterministic transition relation ⇒⊆
S×Act×Dist(S). Each of S, Act and ⇒ may be uncountable.

An infinite path of a PA is an infinite sequence r = s0a0 µ0s1a1 µ1 ··· such that (si, ai, µi) ∈⇒
and µi(si+1) > 0 for each i ∈ N. Similarly, a finite path of a PA is a finite sequence r =
s0a0 µ0s1a1 µ1 ···an−1 µn−1sn such that (si, ai, µi) ∈⇒ and µi(si+1) > 0 for each i < n. We use
PathPful to denote the set of infinite paths of P, and Path

P
fin to denote the set of finite paths of P.

When clear from the context we omit the superscript P. If r is a finite path, we denote by last(r)
the last state of r. Let PathPful(s) and Path

P
fin (s) refer to the sets of infinite and finite paths of P,

respectively, commencing in state s ∈ S.
Let P = (S, Act,⇒) be a PA. A strategy of P is a function σ mapping every finite path

r ∈ Pathfin to a transition (last(r), a, µ) ∈⇒. We write as ΣP the set of strategies of P. For
any strategy σ , let Pathσful and Path

σ
fin denote the sets of infinite and finite paths, respectively,

resulting from the choices of σ . For a state s ∈ S, let Pathσful(s) = Path
σ
ful ∩ Pathful(s) and

Pathσfin(s) = Path
σ
fin ∩Pathfin(s). Given a strategy σ ∈ ΣP and a state s ∈ S, we define the prob-

ability measure Probσs over Path
σ
ful(s) in the standard way [KSK76]. Note that we generally

consider pure strategies (that is, strategies that do not make randomized choices), the choices
of which may depend on the history of the system. The cases in which randomized strategies
(which map from finite paths r to Dist(⇒)) are considered will be signalled in the text.

Given state set S′⊆ S, we write Reach(S′) for the set of paths that reach S′, that is Reach(S′) =
{r | r ∈ Pathful ∧∃i ∈ N.r(i) ∈ S′} where r(i) is the (i + 1)-th state along r. Then, given state
s ∈ S, we write

MaxReachPs (S
′) = sup

σ∈ΣP
Probσs (Reach(S

′)) , MinReachPs (S
′) = inf

σ∈ΣP
Probσs (Reach(S

′))

to be the maximum and minimum probability of reaching a state in S′ from s, respectively.

Proc. AVoCS 2014 4 / 15



ECEASST

Let P = (S, Act,⇒) be a PA. For distributions µ, ν ∈ Dist(S) and for an equivalence relation
≡⊆ S×S, we denote by µ ≡ ν the condition that, for each equivalence class C of ≡, the equality
µ[C] = ν[C] holds. Let ≡⊆ S×S be an equivalence relation on S. A probabilistic bisimulation
respecting ≡ on P [LS91, SL95] is an equivalence relation '⊆ S×S such that s ' t implies
that (1) s ≡ t, and (2) if (s, a, µ) ∈⇒, then there exists (t, a, ν) ∈⇒ such that µ ' ν . States s
and t are called probabilistically bisimilar with respect to ≡ in P if there exists a probabilistic
bisimulation ' respecting ≡ such that s ' t. Probabilistic bisimilar states exhibit the same
maximum and minimum probabilities of reachability (or, more generally, ω -regular properties
[BK08]), and satisfy the same properties of the probabilistic temporal logic PCTL∗ [SL95].

A PA P = (S, Act,⇒) for which all transitions (s, a, µ) ∈⇒ are such that µ is of the form
{s′ 7→ 1} for some s′∈ S is called a nondeterministic automaton. In the case of nondeterministic
automata, we often write (s, a, s′) to denote the transition (s, a,{s′ 7→ 1}). If P is a nondeter-
ministic automaton, then we can simplify the definition of probabilistic bisimulation, which, in
this context, is called simply bisimulation, in the following way: a bisimulation respecting ≡ on
a nondeterministic automaton is an equivalence relation ≈⊆ S×S such that s ≈ t implies that
(1’) s ≡ t, and (2’) if (s, a, s′) ∈⇒, then there exists (t, a,t′) ∈⇒ such that s′ ≈ t′. States s and
t are called bisimilar with respect to ≡ in the nondeterministic automaton P if there exists a
bisimulation ≈ respecting ≡ such that s ≈ t.

2.2 Probabilistic Hybrid Automata

Let X be a finite set of real-valued variables. A valuation v : X → R is a function that assigns
a value to each variable of X . Let V (X ) be the set of valuations of X . When the set X is
clear from the context, we generally write V .

A probabilistic hybrid automaton (PHA) H = (L, X , Events, post, prob) consists of the fol-
lowing components: a finite set L of locations; a finite set X of variables; a finite set Events
of events; a post operator post : L ×V ×R≥0 → 2V ; a finite set prob ⊆ L ×2V ×Events×
Dist(Upd(X )×L) of probabilistic edges, where Upd(X ) is the set of functions ϑ : V → 2V .
A probabilistic edge (l, g, e, p) ∈ prob comprises (1) a source location l, (2) a set g of valuations,
called a guard, (3) an event e, and (4) a probability distribution p that assigns probability to pairs
of the form (ϑ , l′), where ϑ ∈ Upd(X ) is a function describing the manner in which variables
are updated and l′ ∈ L is a target location.

The behaviour of a PHA takes a similar form to that of a classical, non-probabilistic hybrid
automaton [ACH+95]. If the PHA is currently in location l, as time passes, the value of the vari-
ables in X change according to the post operator post: more precisely, if the current valuation is
v and δ ∈ R≥0 time units elapse, the subsequent valuation belongs to the set post(l, v, δ ). If the
current valuation of the variables belongs to the guard g of a probabilistic edge (l, g, e, p), then
the probabilistic edge can be taken. This involves a probabilistic choice according to the distri-
bution p: if the pair (ϑ , l′) is chosen, then the PHA goes to location l′, updating the variables
according to the function ϑ . More precisely, if the current valuation of the variables is v and the
pair (ϑ , l′) is chosen, then the state after taking the probabilistic edge will be (l′, v′) for some
v′ that is chosen nondeterministically from the set ϑ (v). To summarise, the following choices
made by the PHA are nondeterministic: the amount of time to let advance in the current location
l; the valuation used to describe the values of the variables after time has elapsed, according to

5 / 15 Volume 70 (2014)



Abstraction for Stochastic Hybrid Systems

post; the probabilistic edge taken (provided that the guard of the probabilistic edge is satisfied by
the current variable valuation); and, finally, the values to which the variables are updated when a
probabilistic edge is taken. Instead, the only probabilistic choice featured in the model concerns
the choice of pair (ϑ , l′) once a probabilistic edge has been chosen.

We make a number of standard assumptions on the components of a PHA [Spr01, Hah13].

• (Assumptions on post.) For all locations l ∈ L and valuations v ∈ V , we require the
following: (1) post(l, v, 0) = {v}; (2) for all δ , δ ′ ∈ R≥0 such that δ ≥ δ ′, we have
post(l, v, δ ) =

⋃
v′∈post(l,v,δ ′) post(l, v

′, δ −δ ′); (3) there exists δ ∈ R≥0 such that δ > 0
and post(l, v, δ ) = /0.

• (Probabilistic edges can be taken when no more time can elapse.) If l ∈ L and v ∈ V are
such that, for all δ ∈ R≥0 such that δ > 0, we have post(l, v, δ ) = /0, then there must exist
some probabilistic edge (l, g, e, p) ∈ prob such that v ∈ g.

• (Non-empty updates.) For all probabilistic edges (l, g, e, p) ∈ prob and each (ϑ , l′) ∈
support(p), we have ϑ (v) 6= /0 for all v ∈ g.

We now introduce formally the semantics of PHA in terms of PA. The (dense-time) semantics
of the PHA H = (L, X , Events, post, prob) is the PA [[H ]] = (S, Act,⇒) defined in the following
way. The set of states of [[H ]] is defined as S = L×V . The set of actions of [[H ]] is Act =
R≥0 ∪Events. To define the transition relation ⇒, we first define a transition relation for each
time duration and event.

• (Time elapse.) Let δ ∈ R≥0. Then
δ⇒⊆ S ×R≥0 ×Dist(S) is the largest set such that

((l, v), δ ,{(l′, v′) 7→ 1}) ∈ δ⇒ implies that (1) l = l′ and (2) v′ ∈ post(l, v, δ ).

• (Jumps.) Let e∈Events. Consider a distribution p∈Dist(Upd(X )×L), where support(p) =
{(ϑ1, l1), ..., (ϑn, ln)}. Then, for valuation v, we write Bundle(v, p) ⊆ V n to denote the
largest set of vectors of valuations such that [v1, ..., vn] ∈ Bundle(v, p) implies vi ∈ ϑi(v)
for each 1 ≤ i ≤ n. Then e⇒⊆ S × Dist(S) is the largest set of transitions such that
((l, v), e, µ) ∈ e⇒ implies that there exists a probabilistic edge (l, g, e, p) ∈ prob such that
(a) v ∈ g and (b) there exists [v1, ..., vn] ∈ Bundle(v, p) such that, for each (l′, v′) ∈ S:

µ(l′, v′) = ∑
1≤i≤n s.t. v′=vi

p(ϑi, l
′) .

Then we define ⇒ as the transition relation (
⋃

δ∈R≥0
δ⇒)∪(

⋃
e∈Events

e⇒).
We note that the summation in the definition of jump transitions is necessary for the case in

which the same state can be obtained by more than one element (ϑ , l) in the support set of the
distribution of a probabilistic edge.

In the next section, we generally consider a time-abstract semantics of H , in which actions
corresponding to durations of time-elapse transitions are replaced by a single action τ (where
we assume that τ 6∈ Events). Formally, the time-abstract semantics of H is the PA [[H ]]ta =
(S, Act,⇒), where the set S of states is the same as for the dense-time semantics of H , the
set of actions is defined as Act = {τ}∪Events, and the transition relation ⇒ is defined as τ⇒
∪(

⋃
e∈Events

e⇒), where τ⇒= {(s, τ, µ) | ∃δ ∈ R≥0.(s, δ , µ) ∈
δ⇒}.

Proc. AVoCS 2014 6 / 15



ECEASST

2.3 From Non-Probabilistic to Probabilistic Bisimulation

A hybrid automaton (HA) is a PHA (L, X , Events, post, prob) for which all probabilistic edges
(l, g, e, p) ∈ prob correspond to a trivial probabilistic choice over a single element; more pre-
cisely, each (l, g, e, p) ∈ prob is such that p is of the form {(ϑ , l′) 7→ 1} for some ϑ ∈ Upd(X )
and l′ ∈ L). We refer to probabilistic edges of the above form as edges.

Consider an arbitrary PHA H = (L, X , Events, post, prob). We let ind(prob) be the smallest
set of edges such that, if (l, g, e, p) ∈ prob then, for each (ϑ , l′) ∈ support(p), there exists the
probabilistic edge (l, g, (e, p, ϑ ),{(ϑ , l′) 7→ 1}) ∈ ind(prob). Let ind(H ) = (L, X , Events×
Dist(Upd(X )×L)×Upd(X ), post, ind(prob)) be the HA induced by the PHA H . Note that
the location, variable and post sets are the same in H and ind(H ). The events of ind(H )
feature tuples comprising an event of H , the distribution over updates and locations, and an
update. The set of probabilistic edges of ind(H ) is ind(prob), i.e., a set of edges in which the
events encode information derived from probabilistic edges in prob.

We present our first result, namely that bisimilar states of the time-abstract semantics of
ind(H ) are probabilistically bisimilar in the time-abstract semantics of H . In this paper, we
regard locations as being observable from the point of view of properties (such as PCTL∗ formu-
lae or ω -regular objectives), and hence we consider (probabilistic) bisimulation with respect to
an equivalence relation that considers as equivalent states with the same location. We define the
equivalence relation ≡loc⊆ S×S in the following way: (l, v) ≡loc (m, w) if and only if l = m, for
all states (l, v), (m, w) ∈ S.

Proposition 1 Let ≈ be a bisimulation with respect to ≡loc on [[ind(H )]]ta. Then ≈ is a
probabilistic bisimulation with respect to ≡loc on [[H ]]ta.

Proof. We use [[H ]]ta = (S, Act[[H ]]ta ,⇒[[H ]]ta ) and [[ind(H )]]ta = (S, Act[[ind(H )]]ta ,⇒[[ind(H )]]ta )
be the time-abstract semantics of H and ind(H ), respectively (note that [[H ]]ta and [[ind(H )]]ta

have the same set of states, S = L×V ). Let ≈ be a bisimulation respecting ≡loc on [[ind(H )]]ta.
Consider states (l, v), (m, w) ∈ S, and assume that (l, v) ≈ (m, w). This implies that the two

conditions in the definition of bisimulation are satisfied: more precisely, we have (1’) l = m, and
(2’) if ((l, v), a, (l′, v′))∈⇒[[ind(H )]]ta , then there exists ((m, w), a, (m′, w′))∈⇒[[ind(H )]]ta such that
(l′, v′) ≈ (m′, w′).

Given that l = m, condition (1) in the definition of probabilistic bisimulation is satisfied.
Therefore it remains to show condition (2) in the definition of probabilistic bisimulation. Re-
call the definition of the action sets Act[[H ]]ta = {τ}∪Events and Act[[ind(H )]]ta = {τ}∪(Events×
Dist(Upd(X )×L)×Upd(X )). We first consider transitions of [[H ]]ta and [[ind(H )]]ta that
correspond to the action τ , i.e., the transitions corresponding to time elapsing. The definition
of time-elapse transitions depends on post, which is identical in both H and ind(H ). Hence,
for (l, v), the existence of a transition ((l, v), τ, (l′, v′)) ∈⇒[[ind(H )]]ta implies the existence of
a transition ((l, v), τ,{(l′, v′) 7→ 1}) ∈⇒[[H ]]ta . Similarly, for (m, w), the existence of a transi-
tion ((m, w), τ, (m′, w′))∈⇒[[ind(H )]]ta implies the existence of a transition ((m, w), τ,{(m′, w′) 7→
1}) ∈⇒[[H ]]ta . Recalling that (l′, v′) ≈ (m′, w′), we conclude that, in the case of action τ , we
have that condition (2’) in the definition of bisimulation implies condition (2) in the definition of
probabilistic bisimulation.

7 / 15 Volume 70 (2014)



Abstraction for Stochastic Hybrid Systems

We now consider jump transitions. Consider an edge (l, g, (e, p, ϑ ),{(ϑ , l′) 7→1})∈ ind(prob)
such that v ∈ g. We write support(p) = {(ϑ1, l1), ..., (ϑn, ln)}. From the definition of the edge
set ind(prob), we have that there exist edges (l, g, (e, p, ϑi),{(ϑi, li) 7→ 1}) ∈ ind(prob) for all
1≤ i≤n, where ϑ = ϑi and l′ = li for some 1≤ i≤n. Consider some vector a = [v1, ..., vn]∈V n
such that vi ∈ ϑi(v) for each 1 ≤ i ≤ n. We then consider the set of transitions corresponding to a,
namely Ta ={((l, v), (e, p, ϑi), (li, vi)) | vi ∈ ϑi(v)∧1 ≤ i ≤ n}. We have that Ta ⊆⇒[[ind(H )]]ta for
the following reasons: first, we have assumed above that v ∈ g; second, for each 1 ≤ i ≤ n,
noting that Bundle(v,{(ϑi, li) 7→ 1}) contain vectors of length 1, namely those valuations v′
such that v′ ∈ ϑi(v), we obtain that vi ∈ Bundle(v,{(ϑi, li) 7→ 1}), which then implies that
((l, v), (e, p, ϑi),{(li, vi) 7→ 1}) ∈⇒[[ind(H )]]ta (furthermore, recall that we simplify the notation
of such transitions to ((l, v), (e, p, ϑi), (li, vi))). Informally, (li, vi) is the unique state which cor-
responds to the traversal of edge (l, g, (e, p, ϑi),{(ϑi, li) 7→ 1}) from (l, v).

Now, by condition (2’) of the definition of bisimulation, the existence of each transition in Ta
implies the existence of an equally-labelled transition from (m, w) leading to a bisimilar state.
Formally, we can obtain a set U = {((m, w), (e, p, ϑi), (mi, wi)) | ((l, v), (e, p, ϑi), (li, vi)) ∈ Ta ∧
(li, vi) ≈ (mi, wi)}, and U ⊆⇒[[ind(H )]]ta .

Next, we show that the transition sets Ta and U imply the existence of probabilistic transitions
from (l, v) and (m, w) in [[H ]]ta. First note that a ∈ Bundle(v, p), because vi ∈ ϑi(v) for each
1 ≤ i ≤ n. Then a induces the transition ((l, v), e, µa) ∈⇒[[H ]]ta where the distribution µa is
defined as µa(l′, v′) = ∑1≤i≤n∧v′=a[i] p(ϑi, li) for each (l

′, v′) ∈ S.
Let b = [w1, ..., wn]. Note that, for each 1 ≤ i ≤ n, we have (li, a[i]) ≈ (mi, b[i]) (because

(li, vi) ≈ (mi, wi)). We also have b ∈ Bundle(v, p) because, for each 1 ≤ i ≤ n, the existence
of the transition ((m, w), (e, p, ϑi), (mi, wi)) implies that wi ∈ ϑi(w). In a similar manner to the
case of a, we have that b induces the transition ((m, w), e, νb) ∈⇒[[H ]]ta , where νb(m′, w′) =
∑1≤i≤n∧w′=b[i] p(ϑi, mi) for each (m

′, w′) ∈ S.
We now show that µa[C] = νb[C] for all equivalence classes C of ≈. Recall that:

µa[C] = ∑
(l′,v′)∈C

µa(l
′, v′) = ∑

(l′,v′)∈C
∑

1≤i≤n s.t. v′=a[i]
p(ϑi, l

′)

νb[C] = ∑
(m′,w′)∈C

νb(m
′, w′) = ∑

(m′,w′)∈C
∑

1≤i≤n s.t. w′=b[i]
p(ϑi, m

′) .

Given that ≈ respects ≡loc, then, for all (l′, v′), (l′′, v′′) ∈ C, we have l′ = l′′. We use lC to
denote the location component of the states in C. Now consider the sets I aC = {i ∈ N | 1 ≤ i ≤
n∧(lC, a[i]) ∈C} and I bC = {i ∈ N | 1 ≤ i ≤ n∧(lC, b[i]) ∈C}. Note that we can write:

∑
(lC ,v′)∈C

∑
1≤i≤n s.t. v′=a[i]

p(ϑi, lC) = ∑
i∈I aC

p(ϑi, lC)

∑
(lC ,w′)∈C

∑
1≤i≤n s.t. w′=b[i]

p(ϑi, lC) = ∑
i∈I bC

p(ϑi, lC) .

Hence, to show that µa[C] = νb[C], it suffices to show that ∑i∈I aC p(ϑi, l
′) = ∑i∈I bC p(ϑi, m

′).
Given that we established above that, for each 1 ≤ i ≤ n, we have (lC, a[i]) ≈ (lC, b[i]), we

also conclude that (lC, a[i]) ∈ C if and only if (lC, b[i]) ∈ C. This implies that I aC = I
b

C . We
then have that ∑i∈I aC p(ϑi, l

′) = ∑i∈I bC p(ϑi, m
′). Hence µa[C] = νb[C]. We thus conclude that

µa ≈ νb. Condition (2) of the definition of probabilistic bisimulation has been satisfied.

Proc. AVoCS 2014 8 / 15



ECEASST

3 Approximate Abstraction of a Class of Stochastic Hybrid Automata

In this section, we consider the analysis of a restricted class of stochastic hybrid automata (SHA)
by a reduction to probabilistic rectangular automata (PRA), which can then be transformed into
a finite-state PA. We describe briefly SHA in Section 3.1 and PRA in Section 3.2. As an interme-
diate step between SHA and PRA, we introduce a class of PHA called probabilistic slope-update
hybrid automata (PSUHA) in Section 3.3. Given certain assumptions, we show that PSUHA can
be reduced to PRA. We illustrate the approach with respect to the example of Figure 1.

3.1 Stochastic Hybrid Automata: A Brief Overview

We now describe briefly the SHA formalism; for a more technical introduction, see [FHH+11,
Hah13]. A SHA features the same components as a PHA, but also features a set of continuous
probabilistic edges. A continuous probabilistic edge (l, g, e, p̃) comprises (1) a source location l,
(2) a guard g, (3) an event e, and (4) a measurable function p̃ mapping each state to a probability
measure over locations and valuations. We assume that post, guards and update sets of standard
probabilistic edges, and guards of continuous probabilistic edges are measurable in the sense of
[FHH+11, Hah13].

We informally describe the semantics of SHA. As in the case of PHA, from state (l, v) time
can pass with the values of the continuous variables changing as described by the operator post.
The conditions in which standard probabilistic edges can be taken, and their effects on the lo-
cation and continuous variables, are also as in the case of prob of PHA. Similarly to standard
probabilistic edges, a continuous probabilistic edge (l, g, e, p̃) can be taken if the current state
is (l, v) for v ∈ g, and the location and valuation is updated according to a probabilistic choice.
However, for a continuous probabilistic edge, a probability measure (which depends on the cur-
rent state) described by p̃ is used; in particular, this allows us to update variables according to
infinite-support probability distributions, such as the continuous normal or uniform distributions.
In [FHH+11, Hah13], continuous probabilistic edges have been used in the modelling of hybrid
systems that are subject to measurement errors.

Note that, as with PHA, SHA do not feature probabilistic choice over elements of the post
operator: therefore, choices regarding the amount of time to let elapse, and regarding the change
to the continuous variables corresponding to time elapsing, are nondeterministic. However, the
change to continuous variables corresponding to time elapsing can be made to be dependent on
continuous probabilistic choice indirectly. Consider an example of a stochastic hybrid system in
which the rate of change of a continuous variable x as time passes in location l is determined by
a continuous probabilistic choice, say a uniform distribution over the interval [1, 3], made when
location l is entered. Then we can model this system as a SHA with a continuous variable x that
is updated by continuous probabilistic edges according to a uniform distribution over [1, 3] on
entry to location l. The post operator then specifies that the rate of change of x as time passes in
l is equal to the value of x, and that the value of x does not change as time passes in l.

We now explain briefly the methodology of [FHH+11, Hah13] for the construction of approx-
imate abstractions of SHA. This approach concerns the construction of a PHA that is identical
to the SHA except for the fact that each continuous probabilistic edge is replaced by a standard
probabilistic edge with the same source location, guard and event, but for which the distribution

9 / 15 Volume 70 (2014)



Abstraction for Stochastic Hybrid Systems

ranges over update sets and target locations rather than over variable values and target locations.
For example, consider the case of a continuous probabilistic edge (l, g, e, p̃), where p̃ corresponds
to the choice of a single target location l′, and updates the value of a variable x according to a
uniform distribution over [1, 3], while leaving the values of the other variables unchanged. The
continuous probabilistic edge can be replaced by a discrete probabilistic edge (l, g, e, p), where p
is defined in the following manner. The interval [1, 3] is represented by a finite number of inter-
vals, the union of which contains [1, 3], and each of which corresponds to a probability derived
from the original distribution. For example, we can consider the intervals [1, 2] and [2, 3], which
each correspond to probability 12 , in accordance with the original uniform distribution. Then we
let p = {(ϑ1, l′) 7→ 12 , (ϑ2, l

′) 7→ 12}, where ϑ1 (ϑ2, respectively) corresponds to a nondetermin-
istic choice of which value to update x to within the interval [1, 2] ([2, 3], respectively), while
leaving the values of the other variables unchanged. It can be seen that this construction results
in a conservative approximation of a SHA, in the sense that any strategy of the SHA can be emu-
lated by a randomised strategy of the constructed PHA (see [Hah13], Theorem 4.22). Hence the
minimum (maximum, respectively) probability of reaching a certain location in the PHA will be
no greater than (no less than, respectively) the minimum (maximum, respectively) probability of
reaching the location in the SHA. This approximate abstraction methodology then allows tools
for the analysis for PHA to be applied to the analysis of SHA.

3.2 Probabilistic Rectangular Automata

Let I be the set of intervals {[a, b] | a, b ∈Z}∪{(−∞, a] | a ∈Z}∪{[a, ∞) | a ∈Z}∪{(−∞, ∞)}.
In the following, we describe a set V of valuations V (X ) over X ⊆ X to be rectangular over X
if, for each variable x ∈ X , we have that there exists an interval Ix ∈I such that v ∈V if and only
if v(x) ∈ Ix for all x ∈ X . In this case, we often write ∏x∈X Ix to denote V . If a set of valuations is
rectangular over X , we simply describe the set as being rectangular.

In a PRA, all guards and updates are described in terms of rectangular sets over subsets of
the set X of continuous variables. The post operator of a PRA is characterised in the fol-
lowing way: for each location, (1) the rate of change of each variable belongs to an interval,
and (2) the variable values that can be obtained as time passes are constrained to be within a
rectangular set. Formally a PRA R = (L, X , Events, post, prob) is defined as a PHA with the
following restrictions. For each probabilistic edge (l, g, e, p) ∈ prob, we have that g is rectan-
gular. Furthermore, writing support(p) = {(ϑ1, l1), ..., (ϑn, ln)}, for each 1 ≤ i ≤ n there exists
variable set Reset(ϑi) ⊆ X and a rectangular set ∏x∈Reset(ϑi)[u

ϑi
x , u

ϑi
x ] over Reset(ϑi) such that,

for each v ∈ V , v′ ∈ ϑi(v), we have v′(x) ∈ [uϑix , u
ϑi
x ] for each x ∈ Reset(ϑi) and v′(x) = v(x)

for each x ∈ X \Reset(ϑi). The post operator post takes the following form: for each loca-
tion l ∈ L, there exists a rectangular set inv(l) = ∏x∈X Ilx, and there exists an interval [f

l
x, f

l
x]

with flx, f
l
x ∈ Z for each x ∈ X such that, for each valuation v ∈ V and delay δ ∈ R≥0, we have

post(l, v, δ ) = {v′ | (∀x ∈ X .v′(x) ∈ [v(x) + δ ∗flx, v(x) + δ ∗f
l
x])∧v′ ∈ inv(l)}.

As PRA is a subclass of PHA, we can define the dense-time semantics [[R]] of a PRA as in
Section 2. The discrete-time semantics of the PRA R = (L, X , Events, post, prob) with respect
to k ∈ N\{0} is the PA 〈〈R〉〉k = (S, Act,⇒) defined as for the dense-time semantics except for

⇒, which is defined as
1
k⇒∪(

⋃
e∈Events

e⇒). We say that the variable x ∈ X is nondecreasing if

Proc. AVoCS 2014 10 / 15



ECEASST

both Ilx ⊆ R≥0 and [f
l
x, f

l
x] ⊆ R≥0 for all locations l ∈ L. The variable x ∈ X is bounded if Ilx is

a bounded set, for all locations l ∈ L. The PRA R has nondecreasing or bounded variables if
all variables in X are either nondecreasing or bounded. Given a PRA R with nondecreasing
or bounded variables, the discrete-time semantics 〈〈R〉〉k of R with respect to any k ∈ N has a
finite number of classes for probabilistic bisimulation with respect to ≡loc [Spr11]. This result
permits the construction of a finite-state PA that is equivalent to the PRA, and which can then be
analysed using tools for finite-state PA, such as PRISM [KNP11].

3.3 Probabilistic Slope-Update Hybrid Automata

We now consider PSUHA, a class of PHA that generalises PRA, and in which the rate of change
of some variables can be described as the value of other (constant) variables. A PSUHA U =
(L, X , Events, post, prob) is a PHA where the components L, X , Events and prob are defined
as in the case of PRA, and where the post operator post is defined in the following way. First,
we identify a subset C ⊆ X of variables that remain constant as time passes, in each location
(variables in C may be reset when probabilistic edges are taken). For each location l ∈ L, there
exists a subset Dep(l) ⊆ X of variables that have a rate of change that is equal to the value of
a variable in C (note that Dep(l)∩C = /0). For variable x ∈ Dep(l), we write DepOn(l, x) ∈ C
to denote the variable on which the rate of change of x depends in l. Let Rectangular(l) =
X \(C∪Dep(l)). We can now proceed to define the post operator post: for each location l ∈ L,
there exists a rectangular set inv(l) = ∏x∈X Ix, and an interval [f

l
x, f

l
x] with f

l
x, f

l
x ∈ Z for each

x ∈ Rectangular(l) such that, for each valuation v ∈ V and delay δ ∈ R≥0, we have:

post(l, v, δ ) = {v′ | (∀x ∈ Rectangular(l).v′(x) ∈ [v(x) + δ ∗flx, v(x) + δ ∗f
l
x])

∧(∀x ∈ Dep(l).v′(x) = v(x) + δ ∗v(DepOn(l, x))
∧(∀x ∈ C.v′(x) = v(x))
∧v′ ∈ inv(l)} .

The set prob of probabilistic edges of a PSUHA is subject to the following assumptions:

1. (Variables in C are reset on entry to each location.) Each (l, g, e, p) ∈ prob is such that,
for each (ϑ , l′) ∈ support(p) and for each x ∈ C, we have that x ∈ Reset(ϑ ).

2. (On entry to a given location by multiple probabilistic edges, the same interval is used to
define the value of a variable in C.) For each l ∈ L and each x ∈ C, there exist ulx, u

l
x ∈ Z

such that, for each (ϑ , l) ∈
⋃

(l′,g,e,p)∈prob support(p), we have u
ϑ
x = u

l
x and u

ϑ
x = u

l
x.

3. (No probabilistic edge features a probabilistic choice between updates associated with the
same location.) For each (l, g, e, p)∈ prob, for each pair (ϑ ′, l′), (ϑ ′′, l′′)∈ support(p), we
have l′ 6= l′′.

4. (The guards of probabilistic edges do not constrain values of variables in C.) For each
(l, g, e, p) ∈ prob where we write g = ∏x∈X Ix, and each x ∈ C, we have that Ix = (−∞, ∞).

We now show that, for any PSUHA, we can construct a PRA with the same state set such that
the maximum reachability probabilities are identical in the PSUHA and PRA, and similarly for

11 / 15 Volume 70 (2014)



Abstraction for Stochastic Hybrid Systems

the minimum reachability probabilities. We present the result in the context of the discrete-time
semantics, although we note that an analogous result holds for the dense-time semantics. Let
k ∈ N\{0}, and let U and R be PSUHA and PRA, respectively, such that 〈〈U 〉〉k and 〈〈R〉〉k
have the same state set. Then we introduce the following equivalence relation on states: for state
(l, v) of 〈〈U 〉〉k and state (m, w) of 〈〈R〉〉k, we write (l, v) ≡C (m, w) if and only if (1) l = m and
(2) v(x) = w(x) for all x ∈ X \C.

Proposition 2 Let U be a PSUHA, k ∈ N\{0} and F ⊆ L be a set of locations. Then there ex-
ists a PRA R such that 〈〈U 〉〉k and 〈〈R〉〉k have the same state set and, for each pair (l, v), (m, w)
of states such that (l, v) ≡C (m, w), we have:

MaxReach〈〈U 〉〉
k

(l,v) (SF ) = MaxReach
〈〈R〉〉k
(m,w) (SF ) , MinReach

〈〈U 〉〉k
(l,v) (SF ) = MinReach

〈〈R〉〉k
(m,w) (SF ) .

where SF = {(l, v) | (l, v) ∈ S∧l ∈ F}.

Proof sketch. For details of the proof, see [Spr14]. Let U = (L, X , Events, post, prob) be a
PSUHA. We construct the PRA R = (L, X , Events, post′, prob) to be identical to U except for
the post operator. For each state (l, v) ∈ S and each duration δ ∈ R≥0, we define:

post′(l, v, δ ) = {v′ | (∀x ∈ Rectangular(l).v′(x) ∈ [v(x) + δ ∗flx, v(x) + δ ∗f
l
x])

∧(∀x ∈ Dep(l).v′(x) ∈ [v(x) + δ ∗ul
DepOn(l,x), v(x) + δ ∗u

l
DepOn(l,x)])

∧(∀x ∈ C.v′(x) = v(x))
∧v′ ∈ inv(l)} .

Note that, for each variable x in Dep(l), the slope of x in l is chosen the interval
[ul

DepOn(l,x), u
l
DepOn(l,x)], i.e., the interval used to determine the value of the variable DepOn(l, x)

on which x depends on entry to l. It can be seen that post′ conforms to the definition of possible
post operators of PRA, hence R is a PRA.

The proof then involves showing the following condition: a jump transition of 〈〈U 〉〉k followed
by a sequence of time transitions can be replicated by a jump transition of 〈〈R〉〉k followed by a
sequence of time transitions, and vice versa, where the states before and after the transitions are
related by ≡C. Furthermore, the jump transitions are made using the same probabilistic edges,
which means that corresponding transitions can be shown to have the same probability. Note
that we consider such a multi-step equivalence relation (that is, we compare 〈〈U 〉〉k and 〈〈R〉〉k
by considering a jump transition and sequences of time-elapse transitions), rather than a 1-step
relation such as probabilistic bisimulation, for the following reason: when considering the case
in which 〈〈U 〉〉k must emulate a jump transition of 〈〈R〉〉k, the rates of change chosen by 〈〈R〉〉k
in subsequent transitions must be known by 〈〈U 〉〉k, so that 〈〈U 〉〉k knows what value to set the
constants on which the rates of change of variables will depend.

Using this multi-step equivalence property, given that time-elapse transitions correspond to
probability 1, it follows that, for state (l, v) of 〈〈U 〉〉k and state (m, w) of 〈〈R〉〉k such that
(l, v)≡C (m, w), we have MaxReach

〈〈U 〉〉k
(l,v) (SF ) = MaxReach

〈〈R〉〉k
(m,w) (SF ) and MinReach

〈〈U 〉〉k
(l,v) (SF ) =

MinReach〈〈R〉〉
k

(m,w) (SF ).

Proc. AVoCS 2014 12 / 15



ECEASST

Figure 2: Maximum and minimum probabilities of visiting ldeact within time bound T

Proposition 2 suggests the following approximate analysis method for the class of discrete-
time SHA that, when abstracted using the method of [FHH+11, Hah13], result in a discrete-time
PSUHA with nondecreasing or bounded variables: from the PSUHA, then obtain an equivalent
PRA according to Proposition 2; subsequently, the obtained PRA is transformed into a finite-state
PA using the results of [Spr11].

We also mention that we can encode in PSUHA (and hence in the associated PRA) the periodic
resampling of variables in C, which can be done every 1k time units, for some k ∈ N\{0}. The
intuition underlying the encoding is that at most 1k time units can elapse in each location before
taking a probabilistic edge. This can be enforced by adding a clock variable x and by defining the
post operator so that the value of x cannot exceed 1k . Each location has a “self-loop” probabilistic
edge that is enabled when x is equal to 1k , resets x to 0, resets variables in C and does not change
any other variable.1

3.4 Example: Faulty Thermostat

We now illustrate the approximate analysis method proposed in the previous section with an
application to the PRA model of a faulty thermostat presented in Figure 1. As described in Sec-
tion 1, when the heater is on, we consider that the rate of increase of the temperature is chosen
from the normal distribution with mean 3.5 and standard deviation 1, truncated to the interval
[1, 6]. Similarly, when the heater is off, instead of a nondeterministically chosen decrease of
within [−4,−1], we consider the normal distribution with mean −2.5 and standard deviation
0.5, truncated to the interval [−4,−1]. This system can be modelled as a SHA in the sense of
Section 3.1. Now we consider how the approximate abstraction approach of [FHH+11, Hah13]
can be used to obtain a PSUHA. For the case in which the heater is on, we consider three subin-
tervals, [1, 3], [3, 4] and [4, 6], which correspond approximately to the probabilities 0.312, 0.376
and 0.312, respectively, of the aforementioned normal distribution. For the case in which the

1 Note that this construction involves probabilistic edges that choose between alternatives involving the same location:
to satisfy the assumption (3) in the definition of the set of probabilistic edges of a PSUHA, we can consider multiple
copies of the location, each corresponding to a different alternative associated with each probabilistic edge, w.l.o.g.

13 / 15 Volume 70 (2014)



Abstraction for Stochastic Hybrid Systems

heater is off, we consider the three subintervals [−4,−3], [−3,−2] and [−2,−1], corresponding
to the probabilities 0.159, 0.682 and 0.159, respectively. We then constructed the PSUHA ac-
cording to the discrete-time resampling construction, then transformed the resulting model to a
PRA and, in turn, to a finite-state PA, which was analysed with PRISM.

In Figure 2, we present the maximum and minimum probabilities of visiting location ldeact
within time bound T , both in the “original” PRA model shown in Figure 1, and in the “new”
PRA model obtained by the method described above. In both cases, we use the time granularity
k = 10, resulting in a PA with 136112 states. It is clear that the results obtained for the original
PRA model bound those obtained by the new PRA model, often by a substantial amount.

4 Conclusions

We have presented general results on obtaining finite bisimulation quotients for the exact verifi-
cation of PHA, and a method for the approximate verification of a restricted subclass of SHA,
based on a combination of the approximation technique of [FHH+11, Hah13] and the discrete-
time verification method of [Spr11]. We mention some limitations of the latter approach. First,
the approach of choosing probabilistically a slope of a variable on entry to a location, which
then remains constant in that location, may be unrealistic for some applications, in which the
slope of a variable may be subject to stochastic fluctuation as time passes. This criticism applies
principally to the case of the dense-time semantics: in a discrete-time context, only the target
state after 1k time units is important, rather than the trajectory used to reach it, because nonde-
terministic choice is disabled as time passes during the 1k time units. Second, our restriction of
bounded slopes in the context of PSUHA leads to the necessity of truncation of some continuous
distributions. We envisage that this restriction can be lifted. In future work we plan to apply the
results of Section 3 to more realistic case studies.

Acknowledgements: Thanks to Ahmed Bouajjani for comments regarding the results of Sec-
tion 2.

Bibliography

[ACH+95] R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.-H. Ho, X. Nicollin,
A. Olivero, J. Sifakis, S. Yovine. The Algorithmic Analysis of Hybrid Systems. TCS
138(1):3–34, 1995.

[APLS08] A. Abate, M. Prandini, J. Lygeros, S. Sastry. Probabilistic reachability and safety for
controlled discrete time stochastic hybrid systems. Automatica 44(11):2724–2734,
2008.

[BK08] C. Baier, J.-P. Katoen. Principles of model checking. MIT Press, 2008.

[Buj04] M. L. Bujorianu. Extended Stochastic Hybrid Systems and Their Reachability Prob-
lem. In Proc. HSCC’04. LNCS 2993, pp. 234–249. Springer, 2004.

Proc. AVoCS 2014 14 / 15



ECEASST

[FHH+11] M. Fränzle, E. M. Hahn, H. Hermanns, N. Wolovick, L. Zhang. Measurability and
Safety Verification for Stochastic Hybrid Systems. In Proc. HSCC’11. Pp. 43–52.
ACM, 2011.

[Fre08] G. Frehse. PHAVer: Algorithmic Verification of Hybrid systems Past HyTech. STTT
10(3), 2008.

[Hah13] E. M. Hahn. Model checking stochastic hybrid systems. Dissertation, Universität des
Saarlandes, 2013.

[HHW97] T. A. Henzinger, P.-H. Ho, H. Wong-Toi. HyTech: A Model Checker for Hybrid
Systems. STTT 1(1-2):110–122, 1997.

[HLS00] J. Hu, J. Lygeros, S. Sastry. Towards a Theory of Stochastic Hybrid Systems. In
Proc. HSCC’00. LNCS 1790, pp. 160–173. Springer, 2000.

[KNP11] M. Kwiatkowska, G. Norman, D. Parker. PRISM 4.0: Verification of Probabilistic
Real-time Systems. In Proc. CAV’11. LNCS 6806, pp. 585–591. Springer, 2011.

[KSK76] J. G. Kemeny, J. L. Snell, A. W. Knapp. Denumerable Markov Chains. Graduate
Texts in Mathematics. Springer, 2nd edition, 1976.

[LS91] K. G. Larsen, A. Skou. Bisimulation through Probabilistic Testing. I & C 94(1):1–
28, 1991.

[Put94] M. L. Puterman. Markov Decision Processes. J. Wiley & Sons, 1994.

[SL95] R. Segala, N. A. Lynch. Probabilistic Simulations for Probabilistic Processes. Nordic
Journal of Computing 2(2):250–273, 1995.

[Spr00] J. Sproston. Decidable Model Checking of Probabilistic Hybrid Automata. In Proc.
FTRTFT’00. LNCS 1926, pp. 31–45. Springer, 2000.

[Spr01] J. Sproston. Model Checking for Probabilistic Timed and Hybrid Systems. PhD the-
sis, School of Computer Science, University of Birmingham, 2001.

[Spr11] J. Sproston. Discrete-Time Verification and Control for Probabilistic Rectangular
Hybrid Automata. In Proc. QEST’11. Pp. 79–88. IEEE, 2011.

[Spr14] J. Sproston. Exact and Approximate Abstraction for Classes of Stochastic Hybrid
Systems. 2014. Available from http://www.di.unito.it/∼sproston/Research/avocs14-
extended.pdf.

[VPVD08] V. Vladimerou, P. Prabhakar, M. Viswanathan, G. E. Dullerud. STORMED Hybrid
Systems. In Proc. ICALP’08. LNCS 5126, pp. 136–147. Springer, 2008.

[ZSR+12] L. Zhang, Z. She, S. Ratschan, H. Hermanns, E. M. Hahn. Safety Verification for
Probabilistic Hybrid Systems. European Journal of Control 18(6):572–587, 2012.

15 / 15 Volume 70 (2014)


	Introduction
	Exact Abstraction of Probabilistic Hybrid Automata
	Preliminaries
	Probabilistic Hybrid Automata
	From Non-Probabilistic to Probabilistic Bisimulation

	Approximate Abstraction of a Class of Stochastic Hybrid Automata
	Stochastic Hybrid Automata: A Brief Overview
	Probabilistic Rectangular Automata
	Probabilistic Slope-Update Hybrid Automata
	Example: Faulty Thermostat

	Conclusions