Verifying Communicating Agents by Model Checking in a Temporal Action Logic