In: Proc. IEEE Int. Conf. on Systems, Man, and Cybernetics (SMC'99), 12-15 October 1999, Tokyo, Japan, Vol. 3, pages 875-880. 1999.
Abstract: A predicate/transition net mode of the basic distributed dynamic channel allocation algorithm is presented. Inhibitor arcs are used to give a compact model. The high-level net model has one simple net with only 12 places and 16 transitions for any number of channels and cells in the network and for any configuration of the network. This model illustrates how high-level Petri nets can be used to model dynamic features without problems. It is intended for formal verification of the algorithm using reachability analysis.
Keywords: dynamic channel allocation, mobile computing, predicate/transition nets.