B-fairness and structural B-fairness in Petri net models of concurrent systems

摘要

Fairness properties are very important for the behavior characterization of distributed concurrent systems. This paper discusses in detail a bounded-fairness (or B-fairness) theory applied to Petri Net (PN) models. For a given initial marking two transitions in a Petri Net are said to be in a B-fair relation (BF-relation) if the number of times that either can fire before the other fires is bounded. Two transitions are in a structural B-fair relation (SF-relation) if they are in a B-fair relation for any initial marking. A (structural) B-fair net is a net in which every pair of transitions is in a (structural) B-fair relation. The above B-fairness concepts are further extended to groups (or subsets) of transitions, and are called group B-fairness. This paper presents complete characterizations of these B-fairness concepts. In addition, algorithms are given for determining B-fairness and structural B-fairness relations. It is shown that structural B-fairness relations can be computed in polynomial time.