Multi-Robot Systems: Modeling, Specification, and Model Checking
Multi-Robot Systems: Modeling, Specification, and Model Checking
复制标题
多机器人系统：建模、规格说明和模型检查
DOI：
10.5772/7349
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Frieder Stolzenburg
中科院分区：
文献类型：
--
作者：
Ammar Mohammed;U. Furbach;Frieder Stolzenburg
物理多智能体系统（MAS）-也称为多机器人系统-的行为是一项艰巨的任务，特别是当它们被应用在安全关键的应用。对于这一点，形式化的方法的基础上的数学模型的系统设计是有帮助的。它们不仅允许我们在不同的抽象层次上正式地指定系统，而且还允许我们在实现它们之前分析指定系统的一致性。形式规格说明的目的是，一个精确和明确的描述MAS的行为，并正式验证是否满足给定的规范。例如，它应该能够表明不能到达状态空间的不安全区域，或者满足特定的属性。一般来说，MAS中的Agent的行为可以由外部事件和内部状态驱动。因此，一个有效的方法来建模这样的系统是使用状态转换图，这是建立在软件工程。状态转换图描述了代理的动态行为，根据代理在特定场景中的行为。
Specifying behaviors of physical multi-agent systems (MAS) – also called multi-robot systems – is a demanding task, especially when they are applied in safety critical applications. For this, formal methods based on mathematical models of the system under design are helpful. They allow us not only to formally specify the system at different levels of abstraction, but also to analyze the consistency of the specified systems before implementing them. The formal specification aims at both, a precise and unambiguous description of the behavior of MAS, and a formal verification whether a given specification is satisfied. For example, it should be possible to show that unsafe regions of the state space cannot be reached, or that a particular property is satisfied. Generally, the behavior of an agent in MAS can be driven by external events and internal states. Therefore, an efficient way to model such systems is to use state transition diagrams, which are well established in software engineering. A state transition diagram describes the dynamic behaviour of an agent in terms of how the agent acts in certain scenarios of the