Rewarding probabilistic hybrid automata

Ernst Moritz Hahn*, Holger Hermanns

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Citation (Scopus)

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.

Original languageEnglish
Title of host publicationHSCC 2013 - Proceedings of the 16th International Conference on Hybrid Systems
Subtitle of host publicationComputation and Control, Part of CPSWeek 2013
Pages313-322
Number of pages10
DOIs
Publication statusPublished - 2012
Externally publishedYes
Event16th International Conference on Hybrid Systems: Computation and Control, HSCC 2013 - Philadelphia, United States
Duration: 8 Apr 201311 Apr 2013
Conference number: 16

Conference

Conference16th International Conference on Hybrid Systems: Computation and Control, HSCC 2013
Abbreviated titleHSCC 2013
Country/TerritoryUnited States
CityPhiladelphia
Period8/04/1311/04/13
OtherPart of CPSWeek 2013

Keywords

  • Abstraction
  • Continuous time
  • Expected rewards
  • Model checking
  • Nonde-terminism
  • Performability
  • Performance evaluation
  • Probabilistic automaton
  • Probabilistic hybrid automaton
  • Simulation relation

Fingerprint

Dive into the research topics of 'Rewarding probabilistic hybrid automata'. Together they form a unique fingerprint.

Cite this