Validation of multiagent systems by symbolic model checking