https://www.mdu.se/

mdu.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Combining Model Checking and Reinforcement Learning for Scalable Mission Planning of Autonomous Agents
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. (Formal Modelling and Analysis of Embedded Systems)
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0003-2416-4205
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. (Formal Modelling and Analysis of Embedded Systems)ORCID iD: 0000-0003-2870-2680
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0003-0904-3712
2020 (English)Report (Other academic)
Abstract [en]

The problem of mission planning for multiple autonomous agents, including path planning and task scheduling, is often complex. Recent efforts aiming at solving this problem have explored ways of using formal methods to synthesize mission plans that satisfy various requirements. However, when the number of agents grows or requirements include real-time constraints, the complexity of the problem increases to the extent that current algorithmic formal methods cannot handle. In this paper, we propose a novel approach called MCRL, which overcomes this shortcoming by integrating model checking and reinforcement learning techniques. Our approach employs timed automata and timed computation tree logic to describe the autonomous agents' behavior and requirements, and trains the model by a reinforcement learning algorithm, namely Q-learning, to populate a table used to restrict the state space of the model. MCRL combines the ability of model checking to synthesize verifiable mission plans, and the exploration and exploitation capabilities of Q-learning to alleviate the state-space-explosion problem of exhaustive model checking. Our method provides a means to synthesize mission plans for autonomous systems whose complexity exceeds the scalability boundaries of exhaustive model checking, but also to analyze and verify synthesized mission plans in order to ensure given requirements. We evaluate the proposed method on various relevant scenarios involving autonomous agents, and also present and discuss comparisons with other methods and tools.

Place, publisher, year, edition, pages
2020. , p. 10
Keywords [en]
autonomous agents, mission planning, model checking, reinforcement learning
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:mdh:diva-47917OAI: oai:DiVA.org:mdh-47917DiVA, id: diva2:1429051
Funder
Knowledge Foundation, 20150022Available from: 2020-05-07 Created: 2020-05-07 Last updated: 2020-10-22Bibliographically approved
In thesis
1. Automatic Model Generation and Scalable Verification for Autonomous Vehicles: Mission Planning and Collision Avoidance
Open this publication in new window or tab >>Automatic Model Generation and Scalable Verification for Autonomous Vehicles: Mission Planning and Collision Avoidance
2020 (English)Licentiate thesis, comprehensive summary (Other academic)
Abstract [en]

Autonomous vehicles such as mobile driver-less construction equipment bear the promise of increased safety and industrial productivity by automating repetitive tasks and reducing manual labor costs. These systems are usually involved in safety- or mission-critical scenarios, therefore they require thorough analysis and verification. Traditional approaches such as simulation and prototype testing are limited in their scope of verifying a system that interacts autonomously with an unpredictable environment that assumes the presence of humans and varying site conditions. Methods for formal verification could be more suitable in providing guarantees of safe operation of autonomous vehicles within specified unpredictable environments. However, employing them entails addressing two main challenges: (i) constructing the models of the systems and their environment, and (ii) scaling the verification to the incurred model complexity. We address these two challenges for two essential aspects of autonomous vehicle design: mission planning and collision avoidance. Though inherently different, communication between these two aspects is necessary, as the information obtained from verifying collision avoidance can help to improve the mission planning and vice versa. Finding a solution that addresses both mission planning and collision avoidance modeling and verification, while decoupling them for solution maintainability is one crux of this study. Another one deals with demonstrating the applicability and scalability of the proposed approach on complex and industrial-level systems.

In this thesis, we propose a two-layer framework for mission planning and verification of autonomous vehicles. The framework separates the modeling and computing mission plans in a discrete environment, from the vehicle movement within a continuous environment, in which collision avoidance algorithms based on dipole fields are proven to ensure safe behavior. We call the layer for mission planning, the "static layer", and the other one the "dynamic layer". Due to the inherent difference between the layers, we use different modeling and verification approaches, namely: (i) the timed automata formalism and the UPPAAL model checker to compute mission plans for the autonomous vehicles, and (ii) hybrid automata and statistical model checking using UPPAAL Statistical Model Checker to verify collision avoidance and safe operation. We create model-generation algorithms, based on which we develop tool support for the static layer, called TAMAA (Timed-Automata-Based Planner for Autonomous Agents). The tool enables the designers to configure their systems and environments in a graphical user interface, and utilize formal methods and advanced path-planning algorithms to generate mission plans automatically. TAMAA also integrates reinforcement learning with model checking to alleviate the state-space explosion problem when the number of vehicles increases. We create a hybrid model for the dynamic layer of the framework and propose a pattern-based modeling method for the embedded control systems of the autonomous vehicles to ease the design and facilitate reuse. We validate the proposed framework and design method on an industrial use case involving autonomous wheel loaders, for which we verify invariance, reachability, and liveness properties.

Place, publisher, year, edition, pages
Västerås: Mälardalen University, 2020
Series
Mälardalen University Press Licentiate Theses, ISSN 1651-9256 ; 291
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Research subject
Computer Science
Identifiers
urn:nbn:se:mdh:diva-47918 (URN)978-91-7485-469-5 (ISBN)
Presentation
2020-06-15, Västerås Campus (+ Online/Zoom), Mälardalen University, Västerås, 09:00 (English)
Opponent
Supervisors
Projects
DPAC
Funder
Knowledge Foundation, 20150022
Available from: 2020-05-08 Created: 2020-05-07 Last updated: 2022-11-08Bibliographically approved

Open Access in DiVA

No full text in DiVA

Authority records

Gu, RongEnoiu, Eduard PaulSeceleanu, CristinaLundqvist, Kristina

Search in DiVA

By author/editor
Gu, RongEnoiu, Eduard PaulSeceleanu, CristinaLundqvist, Kristina
By organisation
Embedded Systems
Electrical Engineering, Electronic Engineering, Information Engineering

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

urn-nbn
Total: 488 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf