MODELING BROADCAST, MULTICAST, POINT TO POINT, AND HANDSHAKE COMMUNICATIONS OVER THE SAME CHANNEL IN A SPIN MODEL CHECKER

摘要

Module identifying bits corresponding to the modules of a communication network are used to indicate whether a communication is a broadcast communication to all modules in the communication network, a multicast communication to more than one but not all modules in the communication network, or a point-to-point communication to a specific module in the communication network. In addition, a handshake session is also indicated.