Affordable Access

Access to the full text

A Multi-Agent Spatial Logic for Scenario-Based Decision Modeling and Verification in Platoon Systems

Authors
  • Xu, Jingwen1
  • Huang, Yanhong1
  • Shi, Jianqi1
  • Qin, Shengchao2
  • 1 East China Normal University, Shanghai, 200062, China , Shanghai (China)
  • 2 Shenzhen University, Shenzhen, 518061, China , Shenzhen (China)
Type
Published Article
Journal
Journal of Computer Science and Technology
Publisher
Springer-Verlag
Publication Date
Nov 30, 2021
Volume
36
Issue
6
Pages
1231–1247
Identifiers
DOI: 10.1007/s11390-021-1565-8
Source
Springer Nature
Keywords
Disciplines
  • Regular Paper
License
Yellow

Abstract

To cater for the scenario of coordinated transportation of multiple trucks on the highway, a platoon system for autonomous driving has been extensively explored in the industry. Before such a platoon is deployed, it is necessary to ensure the safety of its driving behavior, whereby each vehicle’s behavior is commanded by the decision-making function whose decision is based on the observed driving scenario. However, there is currently a lack of verification methods to ensure the reliability of the scenario-based decision-making process in the platoon system. In this paper, we focus on the platoon driving scenario, whereby the platoon is composed of intelligent heavy trucks driving on cross-sea highways. We propose a formal modeling and verification approach to provide safety assurance for platoon vehicles’ cooperative driving behaviors. The existing Multi-Lane Spatial Logic (MLSL) with a dedicated abstract model can express driving scene spatial properties and prove the safety of multi-lane traffic maneuvers under the single-vehicle perspective. To cater for the platoon system’s multi-vehicle perspective, we modify the existing abstract model and propose a Multi-Agent Spatial Logic (MASL) that extends MLSL by relative orientation and multi-agent observation. We then utilize a timed automata type supporting MASL formulas to model vehicles’ decision controllers for platoon driving. Taking the behavior of a human-driven vehicle (HDV) joining the platoon as a case study, we have implemented the model and verified safety properties on the UPPAAL tool to illustrate the viability of our framework.

Report this publication

Statistics

Seen <100 times