Decomposing the model-checking of mobile robotics actions on a grid
| العنوان: | Decomposing the model-checking of mobile robotics actions on a grid |
|---|---|
| المؤلفون: | Karen Godary Dejean, Didier Crestani, Olivier Naud, Rim Saddem |
| المساهمون: | Robotique mobile pour l'exploration de l'environnement (EXPLORE), Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier (LIRMM), Université de Montpellier (UM)-Centre National de la Recherche Scientifique (CNRS)-Université de Montpellier (UM)-Centre National de la Recherche Scientifique (CNRS), Institut national de recherche en sciences et technologies pour l'environnement et l'agriculture (IRSTEA), Information – Technologies – Analyse Environnementale – Procédés Agricoles (UMR ITAP), Institut national d’études supérieures agronomiques de Montpellier (Montpellier SupAgro)-Institut national de recherche en sciences et technologies pour l'environnement et l'agriculture (IRSTEA), Centre National de la Recherche Scientifique (CNRS)-Université de Montpellier (UM)-Centre National de la Recherche Scientifique (CNRS)-Université de Montpellier (UM), Institut national de recherche en sciences et technologies pour l'environnement et l'agriculture (IRSTEA)-Institut national d’études supérieures agronomiques de Montpellier (Montpellier SupAgro), Institut national d'enseignement supérieur pour l'agriculture, l'alimentation et l'environnement (Institut Agro)-Institut national d'enseignement supérieur pour l'agriculture, l'alimentation et l'environnement (Institut Agro), Université de Montpellier (UM)-Centre National de la Recherche Scientifique (CNRS) |
| المصدر: | 20th IFAC World Congress 20th IFAC World Congress, Jul 2017, Toulouse, France. pp.11156-11162, ⟨10.1016/j.ifacol.2017.08.1236⟩ IFAC-Papers IFAC-PapersOnLine, Elsevier, 2017, 50 (1), pp.11156-11162 |
| بيانات النشر: | HAL CCSD, 2017. |
| سنة النشر: | 2017 |
| مصطلحات موضوعية: | Model checking, Theoretical computer science, decomposition methods, Computer science, automata, Distributed computing, 02 engineering and technology, spatial process, [SPI.AUTO]Engineering Sciences [physics]/Automatic, models, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], Reachability, 020204 information systems, 0202 electrical engineering, electronic engineering, information engineering, Decomposition (computer science), Formal verification, robotics, precision agriculture, REACHABILITY PROPERTY, business.industry, 020207 software engineering, Mobile robot, Robotics, Grid, spatial grid, Test case, Control and Systems Engineering, [SDE]Environmental Sciences, Robot, Artificial intelligence, UNIQUE ACTION, business |
| الوصف: | International audience; Mobile automated systems, such as robots or machinery for precision agriculture, may be designed to perform actions that vary in space according to information from sensors or to a mission map. To be reliable, the design process of such systems should involve the combined verification of spatial and dynamic properties. We consider here CTL model-checking of a mobile robot's behavior, using the UppAal Timed Automata verifier. We consider reachability properties including path finding. Space is modeled as a 2D grid and the mobile robot path is unknown a priori. In this case, the exhaustive state space exploration of model-checking leads to the generation of many possible movements. This exposes such model-checking to combinatorial issues depending on the grid size and the complexity of system dynamics. In this paper, we propose a decomposition methodology reducing the memory requirements for the verification task. The decomposition is twofold. The grid is decomposed in sub-grids and the model-checking query on the whole grid is decomposed in a set of queries on the sub-grids. A set of test cases and check the validity of the decomposition concept. The decomposition methodology is compared to a simpler method that verifies the reachability property without proceeding to decomposition. |
| اللغة: | English |
| تدمد: | 2405-8963 |
| DOI: | 10.1016/j.ifacol.2017.08.1236⟩ |
| URL الوصول: | https://explore.openaire.eu/search/publication?articleId=doi_dedup___::5ff8fbfcb043a7a8e0d748bd93b8de6e https://hal-lirmm.ccsd.cnrs.fr/lirmm-01592588 |
| Rights: | OPEN |
| رقم الانضمام: | edsair.doi.dedup.....5ff8fbfcb043a7a8e0d748bd93b8de6e |
| قاعدة البيانات: | OpenAIRE |
| تدمد: | 24058963 |
|---|---|
| DOI: | 10.1016/j.ifacol.2017.08.1236⟩ |