[HahnH13]
Rewarding probabilistic hybrid automata
In Proceedings of the 16th International Conference on Hybrid
Systems: Computation and Control (HSCC), pages 313-322, ACM, 2013.
Downloads: pdf, bibURL: http://doi.acm.org/10.1145/2461328.2461375
Abstract. The joint consideration 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. Apart
from proving the quantitative safety of such systems, it is important to
analyse properties related to resource consumption (energy, memory, bandwidth,
etc.) and properties that lie more on the economical side (monetary gain, the
expected time or cost until termination, etc.). This paper provides a
framework to decide such reward properties effectively for a generic class of
models which have a discrete-continuous behaviour and involve both
probabilistic as well as nondeterministic decisions. Experimental evidence is
provided demonstrating the applicability of our approach.