A model checker for hierarchical probabilistic real-time systems

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

Full description

Saved in:
Bibliographic Details
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
Tags: Add Tag
No Tags, Be the first to tag this record!
Institution: Singapore Management University
Language: English
Description
Summary: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.

Similar Items