Verifying space and time requirements for resource-bounded agents

We present a novel procedure for automatically verifying the space and time requirements for resource-bounded reasoning agents. We represent agents as a finite state machines in which the states correspond the formulas currently held in the agent's memory and the transitions between states correspond to applying the agent's inference rules. To check whether an agent has enough memory to derive a formula Φ, we specify the FSM as input to the model-based planner MBP, and check whether the agent has a plan (a choice of memory allocations and inference rule applications), all executions of which lead to states containing Φ. Our approach is general enough to admit verification of reasoners with any set of inference rules which can be encoded as transitions between FSM states.