Academic
Publications
Quantitative automata model checking of autonomous stochastic hybrid systems
Quantitative automata model checking of autonomous stochastic hybrid systems   (Citations: 1)
BibTex | RIS | RefWorks Download
This paper considers the quantitative verification of discrete-time stochastic hybrid systems (DTSHS) against linear time objectives. The central question is to determine the likelihood of all the trajectories in a DTSHS that are accepted by an automaton on finite or infinite words. This verification covers regular and ω-regular properties, and thus comprises the linear temporal logic LTL. This work shows that these quantitative verification problems can be reduced to computing reachability probabilities over the product of an automaton and the DTSHS under study. The computation of reachability probabilities can be performed in a backward-recursive manner, and quantitatively approximated by procedures over discrete-time Markov chains. A case study shows the feasibility of the approach.
Published in 2011.
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
Order by: