Verifying space and time requirements for resource-bounded agents

The effective reasoning capability of an agent can be defined as its capability to infer, within a given space and time bound, facts that are logical consequences of its knowledge base. In this paper we show how to determine the effective reasoning capability of an agent with limited memory by encoding the agent`s reasoning system as a finite state machine (FSM) Psi and verifying the existence of a program (sequence of inference steps) that, starting from a given knowledge base K, leads Psi to a state satisfying a given formula phi. Our approach is general enough to admit verification of any reasoning agent whose inference rules can be encoded as transitions between FSM states. As an illustration, we show how to encode two example reasoners: a classical propositional reasoner which can derive all classical consequences of its knowledge base given unlimited memory, and a forward-chaining rule-based reasoner of the kind found in many applications employing ontological reasoning and business rules. We then go on to show how the transition system can be used to automatically verify the existence of a derivation, and present experimental results using the Model Based Planner (mbp) which illustrates how the length of the deduction varies for different memory sizes