Abstract
Real-life systems are usually hard to control, due to their complicated structures, quantitative time factors and even stochastic behaviors. In this work, we present a model checker to analyze hierarchical probabilistic real-time systems. A modeling language called PRTS is used to specify such systems, and automatic zone-abstraction approach, which is probability preserving, is used to generate finite state MDP. We have implemented PRTS in model checking framework PAT so that friendly user interface can be used to edit, simulate and verify PRTS models. Some experiments are conducted to show our tool's efficiency. © 2012 Springer-Verlag.
Cite
CITATION STYLE
Song, S., Sun, J., Liu, Y., & Dong, J. S. (2012). A model checker for hierarchical probabilistic real-time systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7358 LNCS, pp. 705–711). https://doi.org/10.1007/978-3-642-31424-7_53
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
