Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

Decidable Model Checking of Probabilistic Hybrid Automata

Jeremy SprostonContact Information

(5)  School of Computer Science, University of Birmingham, Birmingham, B15 2TT, UK
Abstract
Hybrid automata offer a framework for the description of systems with both discrete and continuous components, such as digital technology embedded in an analogue environment. Traditional uses of hybrid automata express choice of transitions purely in terms of nondeterminism, abstracting potentially significant information concerning the relative likelihood of certain behaviours. To model such probabilistic information, we present a variant of hybrid automata augmented with discrete probability distributions. We concentrate on restricted subclasses of the model in order to obtain decidable model checking algorithms for properties expressed in probabilistic temporal logics.
Supported in part by the EPSRC grant GR/N22960.

Contact Information Jeremy Sproston
Email: J.Sproston@cs.bham.ac.uk
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.108 • Server: mpweb19
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)