Verifying Multi-agent Systems via Unbounded Model Checking