Publication Type
Conference Proceeding Article
Version
publishedVersion
Publication Date
7-2012
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.
Keywords
Model Checker, Markov Decision Process, Stochastic Game, Time Automaton, Friendly User Interface
Discipline
Programming Languages and Compilers | Software Engineering
Research Areas
Software and Cyber-Physical Systems
Publication
Proceedings of the 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13
First Page
705
Last Page
711
ISBN
9783642314230
Identifier
10.1007/978-3-642-31424-7_53
Publisher
Springer Link
City or Country
Berkeley, CA, USA
Citation
SONG, Songzheng; SUN, Jun; LIU, Yang; and DONG, Jin Song.
A model checker for hierarchical probabilistic real-time systems. (2012). Proceedings of the 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13. 705-711.
Available at: https://ink.library.smu.edu.sg/sis_research/5015
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
https://doi.org/10.1007/978-3-642-31424-7_53