 Process
Analysis Toolkit (PAT) 3.5
Help |
A probabilistic system is useful in modeling randomized algorithms (e.g.,
consensus algorithms), unreliable or unpredictable behaviors (e.g., human
behaviors in decision making process), etc.. Markov Decision Process (MDP) is
used to construct this kind of system. In MDPs, nondeterministic and
probabilistic choices coexist. Randomized distributed algorithms are typically
appropriately modeled by MDPs, as probabilities affect just a small part of the
algorithm and non-determinism is used to model concurrency between processes by
means of interleaving. There are several model checkers concentrating on this
field (e.g., PRISM, MRMC). Model checking probabilistic systems against LTL formulae is to compute the
probability that the system satisfies formulae. It works by firstly identifying
the set of system states which form end components that almost surely satisfies
the property. Then it computes the probability of reaching those states from the
initial system state. If the property is safety, we show that the problem is
reduced to a probabilistic refinement checking problem. If the negation of the
property is safety, then the problem is reduced to a probabilistic
deadlock-freeness checking problem. In both cases, we can avoid identifying end
components or building a Deterministic Rabin Automaton(DRA), which is
computational expensive. Otherwise, a DRA of the formula is built and we use it
to make a product with the MDP and then calculate the reach-ability to specified
end components. In addition, we are working to fulfill the algorithm to PCTL
(Probabilistic Computation Tree Logic). This model has unique characteristic compared with other modules since it
supports the probabilistic choices. We have our own syntax
based on CSP# to support this. For probabilistic calculation, we use the value
iteration method. Now in PAT, the default threshold for stopping the iteration
is 10E-6, and the results keep 5 digits after dot. Users could adjust these
value in "Options" in GUI. In GUI, choose Tools -> Options -> Probability CSP module then we could
get the following window. Currently this is still in beta stage. We are actively developing it now. Any
suggestion or feedback is extremely welcome. 
Copyright © 2007-2012 Semantic Engineering Pte. Ltd.