Affiliations: Utrecht University, Department of Computer Science, P.O. Box 80.089, 3508 TB Utrecht, The Netherlands. wiebe@cs.ruu.nl
Note: [] Address for correspondence: Utrecht University Department of Computer Science P.O. Box 80.089, 3508 TB Utrecht The Netherlands Currently at ABN-AMRO, Amsterdam.
Note: [] Address for correspondence: Utrecht University Department of Computer Science P.O. Box 80.089, 3508 TB Utrecht The Netherlands
Note: [] Address for correspondence: Utrecht University Department of Computer Science P.O. Box 80.089, 3508 TB Utrecht The Netherlands
Abstract: We present a formal system to reason about and specify the behavior of multiple intelligent artificial agents. Essentially, each agent can perform certain actions, and it may possess a variety of information in order to reason about its and other agent's actions. Thus, our KARO-framework tries to deal formally with the notion of Knowledge, possessed by the agents, and their possible execution of actions. In particular, each agent may reason about its —or, alternatively, other's— Abilities to perform certain actions, the possible Results of such an execution and the availability of the Opportunities to take a particular action. Formally, we combine dynamic and epistemic logic into one modal system, and add the notion of ability to it. We demonstrate that there are several options to define the ability to perform a sequentially composed action, and we outline several properties under two alternative choices. Also, the agents' views on the correctness and feasibility of their plans are highlighted. Finally, the complications in the completeness proof for both systems indicate that the presence of abilities in the logic makes the use of infinite proof rules useful, if not inevitable.
