Modeling and Analysis of Probabilistic Timed Systems

Probabilistic models are useful for analyzing systems which operate under the presence of uncertainty. In this paper, we present a technique for verifying safety and liveness properties for probabilistic timed automata. The proposed technique is an extension of a technique used to verify stochastic hybrid automata using an approximation with Markov Decision Processes. A case study for CSMA/CD protocol has been used to show case the methodology used in our technique.

• Type: Conference
• Year: 2009
• Where: ECBS
• Authors: Abhishek Dubey, Derek Riley, Sherif Abdelwahed, Ted Bapty
• Keywords: ECBS 2009, Hardware, Probabilistic Models, Probabilistic Timed Automata, Stochastic Hybrid Automata