An Adaptive Task-Based Model for Autonomous Multi-Robot Using HARMS and NuSMV

We propose an adaptive task-based model that allows cyber-physical systems (CPS) to update their environmental model and helps them analyse reachability to their goal from current state using the updated environmental model and its capabilities. Proposed model consists of two parts: information exchange module and model validation module. Information exchange module utilizes Human-Agent-Robot-Machine-Sensor (HARMS) model to exchange messages between CPS. Model validation module uses NuSMV, which is one of Model Checking tools, to check whether the system can continue its mission toward the goal in the given environment. In order to see feasibility of the proposed model, we explain a practical set up of the model in a situation in which homogeneous robots that has the same capability work in the same environment.