Abstract
Dealing with the interplay of randomness and continuous
time is important for the formal verification of many real
systems. Considering both facets is especially important for
wireless sensor networks, distributed control applications,
and many other systems of growing importance. An important
traditional design and verification goal for such systems
is to ensure that unsafe states can never be reached. In the
stochastic setting, this translates to the question whether
the probability to reach unsafe states remains tolerable. In
this paper, we consider stochastic hybrid systems where
the continuous-time behaviour is given by differential equations,
as for usual hybrid systems, but the targets of discrete
jumps are chosen by probability distributions. These
distributions may be general measures on state sets. Also
non-determinism is supported, and the latter is exploited in
an abstraction and evaluation method that establishes safe
upper bounds on reachability probabilities. To arrive there
requires us to solve semantic intricacies as well as practical
problems. In particular, we show that measurability of a
complete system follows from the measurability of its constituent
parts. On the practical side, we enhance tool support
to work effectively on such general models. Experimental
evidence is provided demonstrating the applicability of
our approach on three case studies, tackled using a prototypical
implementation.
Original language | English |
---|---|
Title of host publication | Proceedings of the 14th international conference on Hybrid systems: computation and control |
Publisher | Association for Computing Machinery |
Publication date | 2011 |
Pages | 43-52 |
ISBN (Print) | 9781450306294 |
DOIs | |
Publication status | Published - 2011 |
Event | International Conference on Hybrid Systems 2011: Computation and Control - Chicago, United States Duration: 12 Apr 2011 → 14 Apr 2011 Conference number: 14 |
Conference
Conference | International Conference on Hybrid Systems 2011 |
---|---|
Number | 14 |
Country/Territory | United States |
City | Chicago |
Period | 12/04/2011 → 14/04/2011 |