A model checker for hierarchical probabilistic real-time systems

Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-642-31424-7_53

Title:	A model checker for hierarchical probabilistic real-time systems
Authors:	Song, S. Sun, J. Liu, Y. Dong, J.S.
Issue Date:	2012
Citation:	Song, S.,Sun, J.,Liu, Y.,Dong, J.S. (2012). A model checker for hierarchical probabilistic real-time systems. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 7358 LNCS : 705-711. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-642-31424-7_53
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. © 2012 Springer-Verlag.
Source Title:	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
URI:	http://scholarbank.nus.edu.sg/handle/10635/43161
ISBN:	9783642314230
ISSN:	03029743
DOI:	10.1007/978-3-642-31424-7_53
Appears in Collections:	Staff Publications

There are no files associated with this item.

Check