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.
|