In: Proceedings of 10th IEEE Pacific Rim International Symposium on Dependable Computing (PRDC'04), March 03 - 05, 2004, Papeete, Tahiti, French Polynesia, pages 373-380. IEEE Press, March 2004.
Abstract: 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. In this paper, 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.
Keywords: Controllability; probabilistic Petri net; reachability; self-stabilization; verification.