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

Additional URL

https://doi.org/10.1007/978-3-642-31424-7_53

Share

COinS