HomeNewsCase StudiesPeoplePublications
[HH13] E. M. Hahn and H. Hermanns. Rewarding Probabilistic Hybrid Automata. In Proc. 16th International Conference on Hybrid Systems: Computation and Control (HSCC 2013), pages 313-322, ACM. 2013. [pdf] [bib]
Downloads:  pdf pdf (341 KB)  bib bib
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.