A model checker for hierarchical probabilistic real-time systems

• Main Authors: SONG, Songzheng, SUN, Jun, LIU, Yang, DONG, Jin Song
• Format: text
• Language: English
• Published: Institutional Knowledge at Singapore Management University 2012
• Subjects: Model Checker; Markov Decision Process; Stochastic Game; Time Automaton; Friendly User Interface; Programming Languages and Compilers; Software Engineering
• Online Access: https://ink.library.smu.edu.sg/sis_research/5015; https://ink.library.smu.edu.sg/context/sis_research/article/6018/viewcontent/A_Model_Checker_for_Hierarchical_Probabilistic_Real_Time_Systems.pdf
• Institution: Singapore Management University

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.