Dependability analysis of a class of probabilistic Petri nets

Verification of various properties associated with concurrent/distributed systems is critical in the process of designing and analyzing dependable systems. While techniques for the automatic verification of finite-state systems are relatively well studied, one of the main challenges in the domain of verification is concerned with the development of new techniques capable of coping with problems beyond the finite state framework. We investigate a number of problems closely related to dependability analysis in the context of probabilistic infinite-state systems modelled by probabilistic conflict-free Petri nets. Using a valuation method, we are able to demonstrate effective procedures for solving the termination with probability 1, the self-stabilization with probability 1, and the controllability with probability 1 problems in a unified framework.