Title :
Modelling a distributed dynamic channel allocation algorithm for mobile computing using predicate/transition nets
Author :
Ojala, Leo ; Husberg, Nisse ; Blom, Simo
Author_Institution :
Dept. of Comput. Sci., Helsinki Univ. of Technol., Espoo, Finland
fDate :
6/21/1905 12:00:00 AM
Abstract :
Prakash et al. (1995) presented an algorithm for distributed dynamic channel allocation for mobile computing. A predicate/transition net model of the basic algorithm is presented. Inhibitor arcs are used to give a compact model. The same model can be used for any number of channels and cells with any configuration. This model illustrates how high level Petri nets can be used to model dynamic features. It is intended for formal verification of the algorithm using reachability analysis
Keywords :
Petri nets; channel allocation; distributed algorithms; formal verification; mobile computing; reachability analysis; cells; distributed dynamic channel allocation algorithm; dynamic features; formal verification; high level Petri nets; inhibitor arcs; mobile computing; modelling; predicate/transition nets; reachability analysis; Algorithm design and analysis; Channel allocation; Computer science; Distributed computing; Formal verification; Heuristic algorithms; Inhibitors; Laboratories; Mobile computing; Petri nets;
Conference_Titel :
Systems, Man, and Cybernetics, 1999. IEEE SMC '99 Conference Proceedings. 1999 IEEE International Conference on
Conference_Location :
Tokyo
Print_ISBN :
0-7803-5731-0
DOI :
10.1109/ICSMC.1999.823343
