Return to search

A Bigraphical Framework for Modeling and Simulation of UAV-based Inspection Scenarios

We present a formal modeling approach for the design and simulation of Multi-Unmanned Aerial Vehicle (multi-UAV) inspection scenarios, where planning is based on model checking. As demonstration, we formalize and simulate a compositional UAV inspection system of a solar park using bigraphical reactive systems, which introduce the notion of time-varying bigraphs. Specifically, the UAV system is modeled as a process-algebraic expression, whose semantics is a bigraph state in a labeled transition system.
The underlying Multi-Agent Path Finding problem is solved model-theoretically using Planning-by-Model-Checking. It solves the inherently connected collision-free path planning problem for multiple UAVs subject to contexts and local conditions. First, a bigraph is constructed algebraically, which can be decomposed systematically into separate parts with interfaces. The layered composite model accounts for location, navigation, UAVs, and contexts, which enables simple configuration and extension (changeability). Second, the executable operational semantics of our formal bigraph model are given by bigraphical reactive systems, where rules constitute the behavioral component of our model. Rules reconfigure the bigraph to simulate state changes, i.e., they allow to alter the conditions under which UAVs are permitted to move.
Properties can be attached to nodes of the bigraph and evaluated in a simulation over the traces of the transition system according to some cost-based policies.
In essence, the inherent multi-UAV path planning problem of our scenario is formulated as a reachability problem and solved by model checking the generated transition system. The bigraph-algebraic expression also allows us to reason about potential parallelization opportunities when moving UAVs. Moreover, we sketch how to directly simulate the bigraph specification in a ROS-based Gazebo simulation by examining the inspection and monitoring of a solar park as an application.
The reactive system specification provides the blueprint for analysis, simulation, implementation and execution. Thus, the same algorithm used for verification is used as well for the simulation in ROS/Gazebo to execute plans.:1 Introduction

2 Overview: Scenario Description and Formal Modeling Approach

3 Background: Bigraphs and Model Checking

4 Construction of the UAV System via Composition

5 Making the Drones Fly: Executable Model Semantics

6 Collision-Free Path Planning Problem

7 Prototypical Implementation

8 Discussion

9 Related Work

10 Conclusion

A UAV State Machine
B Bigraphical Reactive Systems
C RPO/IPO Semantic

Identiferoai:union.ndltd.org:DRESDEN/oai:qucosa:de:qucosa:90865
Date11 April 2024
CreatorsGrzelak, Dominik, Lindner, Martin
ContributorsBelov, Mikhail, Aßmann, Uwe, Husak, Oleksandr, Fricke, Hartmut, Technische Universität Dresden
Source SetsHochschulschriftenserver (HSSS) der SLUB Dresden
LanguageEnglish
Detected LanguageEnglish
Typeinfo:eu-repo/semantics/submittedVersion, doc-type:preprint, info:eu-repo/semantics/preprint, doc-type:Text
Rightsinfo:eu-repo/semantics/openAccess
Relationinfo:eu-repo/grantAgreement/Deutsche Forschungsgemeinschaft/Exzellenzcluster/390696704//Centre for Tactile Internet with Human-in-the-Loop/CeTI

Page generated in 0.0025 seconds