The control and verification of similar agents operating in a broadcast network environment

We explore issues related to the control and verification of similar agents that interact through events broadcast over a network. The similar agents are modeled as discrete-event systems that have identical structure. System events are partitioned into global and private events that respectively affect all agents or exactly one agent. We show how the state explosion problem inherent to many concurrent systems is not as problematic in this setting. We give a procedure to test if these systems are globally deadlock-free or nonblocking. We explore control and verification problems related to both local and global specifications on these systems. For each module there is exactly one controller and all controllers enforce the same control policy. Necessary and sufficient conditions for achieving local and global specifications in this setting are identified.