Contextual Reasoning in the Verification of PRS Agent Programs

Wayne Wobcke

Although software agents are becoming more widely used, methodology for constructing agent programs is poorly understood. In this paper, we take a step towards specifying and proving correctness for a class of agent programs based on the PRS architecture, Georgeff and Lansky (1987), one of the most widely used in industrial settings. We view PRS as a simplified operating system, capable of running concurrently a series of plans, each of which at any time is in a state of partial execution. The PRS system is construed as using a simplified interrupt mechanism that enables it, using information about goal priorities, to "recover" from various contingencies so that the blocked plans can be resumed and eventually successfully completed. We develop a simple methodology for PRS program construction, then present a formalism combining dynamic logic and context-based reasoning that can be used to reason about such PRS plans.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.