Model Checking Agent Programming Languages

点击翻译按钮获取中文摘要

Our overall goal in this project is to develop model checkingtechniques that can be applied to various agent-oriented programminglanguages. Building on our previous work on model checking forAgentSpeak, we will investigate the key aspects underlying not only AgentSpeak but other agent-oriented programming languages based on Java, such as 3APL, Concurrent MetateM, and Jadex. Based on that, wewill develop a Java infrastructure layer that is (a) relevant to theimplementation of these agent languages (b) has clear semantics, and(c) is able to be verified through an extended version of JPF, an open source Java model checker.As a result of this investigation, we will be able to develop bothformal semantics for these major constructs of agent programming aswell as Java libraries that implement them (based on the semantics)- the resulting intermediate agent language will be called the AgentInfrastructure Layer (AIL). As in our existing body of work, JPF is tobe used as the model checker with which to carry out formalverification of implemented agent-based systems. The idea is then toprovide automatic (and provably correct) translations from variousexisting agent-oriented programming languages.