In: Proc. 4th Int. Workshop on Petri Nets and Performance Models (PNPM'91), Melbourne, Australia, pages 204-209. IEEE Comp. Soc. Press, December 1991.
Abstract: Probabilistic validation is a new approach to deal with large state transitions systems. The user's need is to prove that, for a given period of operations, a given assertion on the reached states is true with a sufficient level of probability. The system to be validated is modeled by a stochastic Petri net. The analysis relies on a partial exploration of the reachability set and tries to reach as quickly as possible critical states (states in which the assertion is not verified). An exact linear program solution allows to ``travel'' through the graph. The main goal of this paper is to present the principles of this searching algorithm. This method can be used in probability computations in two ways. The first one is related to acyclic graphs. A breadth or a depth first search traversal can be done without considering all the trajectories but only those leading to critical states. The second one is related to importance sampling simulation.
Keywords: safety critical systems; distributed systems; probability; simulation; stochastic Petri nets; validation.