Real-time systems exhibiting probabilistic behavior due to uncertainty in timing or failure rates require sophisticated analysis techniques beyond traditional deterministic or purely probabilistic approaches. This work innovates by developing methods to bridge probabilistic and timed models enabling rigorous analysis of systems with both characteristics. The approximation approach enables practical analysis of realistic systems while maintaining verification guarantees.
This paper presents modeling and analysis of probabilistic timed systems using approximation with Markov Decision Processes to enable verification of safety, liveness, and bounded time reachability properties. The work develops techniques to convert probabilistic timed automata into equivalent Markov decision processes enabling analysis of probabilistic real-time systems. The approach supports analysis of systems with both stochastic and timed behaviors enabling verification of temporal properties of probabilistic systems.
The approach successfully analyzes probabilistic timed systems including reachability, safety, and bounded time properties through conversion to Markov decision processes. Results demonstrate effective approximation of probabilistic timed automata enabling practical verification. The framework enables analysis of complex systems with both timed and probabilistic behaviors.
@inproceedings{Dubey2009a,
author = {Dubey, Abhishek and Riley, Derek and Abdelwahed, Sherif and Bapty, Ted},
booktitle = {16th Annual {IEEE} International Conference and Workshop on the Engineering of Computer Based Systems, {ECBS} 2009, San Francisco, California, USA, 14-16 April 2009},
title = {Modeling and Analysis of Probabilistic Timed Systems},
year = {2009},
pages = {69--78},
abstract = {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.},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/bib/conf/ecbs/DubeyRAB09},
category = {conference},
contribution = {lead},
doi = {10.1109/ECBS.2009.44},
file = {:Dubey2009a-Modeling_and_Analysis_of_Probabilistic_Timed_Systems.pdf:PDF},
keywords = {probabilistic systems, timed automata, verification, safety, reachability, Markov processes},
project = {cps-reliability},
timestamp = {Wed, 16 Oct 2019 14:14:51 +0200},
url = {https://doi.org/10.1109/ECBS.2009.44}
}