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

作     者：Jingwen Xu Yanhong Huang Jianqi Shi Shengchao Qin Jingwen Xu;Yanhong Huang;Jianqi Shi;Shengchao Qin

作者机构：National Trusted Embedded Software Engineering Technology Research CenterEast China Normal University Shanghai 200062China College of Computer Science and Software EngineeringShenzhen UniversityShenzhen 518061China 

出 版 物：《Journal of Computer Science & Technology》 (计算机科学技术学报（英文版）)

年 卷 期：2021年第36卷第6期

页      面：1231-1247页

核心收录：

学科分类：08[工学] 082303[工学-交通运输规划与管理] 082302[工学-交通信息工程及控制] 0823[工学-交通运输工程] 

基　　金：supported by the National Key Research and Development Program of China under Grant No.2019YFB2102602 

主　　题：autonomous driving decision-making model platoon system safety verification timed automaton 

摘      要：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 *** 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 ***,there is currently a lack of verification methods to ensure the reliability of the scenario-based decision-making process in the platoon *** this paper,we focus on the platoon driving scenario,whereby the platoon is composed of intelligent heavy trucks driving on cross-sea *** propose a formal modeling and verification approach to provide safety assurance for platoon vehicles’cooperative driving *** 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 *** 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 *** then utilize a timed automata type supporting MASL formulas to model vehicles’decision controllers for platoon *** 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.