A Model Checker for Hierarchical Probabilistic Real-Time Systems

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 c 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.

• Type: Journal
• Year: 2012
• Where: CAV
• Authors: Songzheng Song, Jun Sun 0001, Yang Liu 0003, Jin Song Dong
• Keywords: CAV 2012, Hardware, Model Checker, Real Time Systems, Time Factors