Verifying space and time requirements for resource-bounded agents