Practical verification of decision-making in agent-based autonomous systems
Practical verification of decision-making in agent-based autonomous systems
复制标题
DOI：
10.1007/s10515-014-0168-9
复制
发表时间：
2013-10
影响因子：
3.4
通讯作者：
Louise Dennis;Michael Fisher;N. Lincoln;A. Lisitsa;S. Veres
中科院分区：
文献类型：
--
作者：
Louise Dennis;Michael Fisher;N. Lincoln;A. Lisitsa;S. Veres
我们提出了一种验证方法来分析基于智能体的混合系统中的决策组件。传统上，混合自动机已经被用于实现和验证这样的系统，但是基于混合自动机的建模、编程和验证技术随着离散决策复杂性的增加而难以扩展，这使得它们在需要复杂逻辑推理的情况下没有吸引力。因此，在复杂系统的编程中，将逻辑决策分离为单独的、离散的组件变得很常见。然而，验证技术未能跟上这一发展的步伐。我们正在探索基于代理的逻辑组件，并为这些组件开发了一种模型检查技术，然后这些组件可以与混合系统的连续部分的单独分析组成。除此之外，这允许使用程序模型检查器来验证混合自治系统中决策的实际实现。
We present a verification methodology for analysing the decision-making component in agent-based hybrid systems. Traditionally hybrid automata have been used to both implement and verify such systems, but hybrid automata based modelling, programming and verification techniques scale poorly as the complexity of discrete decision-making increases making them unattractive in situations where complex logical reasoning is required. In the programming of complex systems it has, therefore, become common to separate out logical decision-making into a separate, discrete, component. However, verification techniques have failed to keep pace with this development. We are exploring agent-based logical components and have developed a model checking technique for such components which can then be composed with a separate analysis of the continuous part of the hybrid system. Among other things this allowsprogrammodel checkers to be used to verify the actual implementation of the decision-making in hybrid autonomous systems.