Model Checking Agent Programming Languages

我们在这个项目中的总体目标是开发可以应用于各种面向代理的编程语言的模型检查技术。基于我们以前对AgentSpeak的模型检查工作，我们将研究不仅是AgentSpeak，而且是其他基于Java的面向代理的编程语言（如3APL，Concurrent MetateM和Jadex）的关键方面。在此基础上，我们将开发一个Java基础设施层，它（a）与这些代理语言的实现相关（B）具有清晰的语义，（c）能够通过开源Java模型检查器JPF的扩展版本进行验证。我们将能够为这些主要的代理编程结构以及实现它们的Java库开发正式的语义（基于语义）-所得到的中间代理语言将被称为代理基础结构层（AIL）。在我们现有的工作机构，JPF是被用来作为模型检查器，进行形式化验证的实现基于代理的系统。然后，我们的想法是从各种现有的面向代理的编程语言提供自动（和可证明正确的）翻译。

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.