Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 3 of 3
Full-Text Articles in Physical Sciences and Mathematics
Scc-Based Improved Reachability Analysis For Markov Decision Processes, Lin Gui, Jun Sun, Songzheng Song, Yang Liu, Jin Song Dong
Scc-Based Improved Reachability Analysis For Markov Decision Processes, Lin Gui, Jun Sun, Songzheng Song, Yang Liu, Jin Song Dong
Research Collection School Of Computing and Information Systems
Markov decision processes (MDPs) are extensively used to model systems with both probabilistic and nondeterministic behavior. The problem of calculating the probability of reaching certain system states (hereafter reachability analysis) is central to the MDP-based system analysis. It is known that existing approaches on reachability analysis for MDPs are often inefficient when a given MDP contains a large number of states and loops, especially with the existence of multiple probability distributions. In this work, we propose a method to eliminate strongly connected components (SCCs) in an MDP using a divide-and-conquer algorithm, and actively remove redundant probability distributions in the MDP …
A Model Checker For Hierarchical Probabilistic Real-Time Systems, Songzheng Song, Jun Sun, Yang Liu, Jin Song Dong
A Model Checker For Hierarchical Probabilistic Real-Time Systems, Songzheng Song, Jun Sun, Yang Liu, Jin Song Dong
Research Collection School Of Computing and Information 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 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.
Model Checking Hierarchical Probabilistic Systems, Jun Sun, Songzheng Song, Yang Liu
Model Checking Hierarchical Probabilistic Systems, Jun Sun, Songzheng Song, Yang Liu
Research Collection School Of Computing and Information Systems
Probabilistic modeling is important for random distributed algorithms, bio-systems or decision processes. Probabilistic model checking is a systematic way of analyzing finite-state probabilistic models. Existing probabilistic model checkers have been designed for simple systems without hierarchy. In this paper, we extend the PAT toolkit to support probabilistic model checking of hierarchical complex systems. We propose to use PCSP#, a combination of Hoare’s CSP with data and probability, to model such systems. In addition to temporal logic, we allow complex safety properties to be specified by non-probabilistic PCSP# model. Validity of the properties (with probability) is established by refinement checking. Furthermore, …