基于扩展交替时序逻辑的控制器综合方法  

A controller synthesis method based on extended alternating-time temporal logic

作　　者：黄若寒 曹子宁[1,2,3] HUANG Ruo-han;CAO Zi-ning(College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,Jiangsu,China;Ministry Key Laboratory for Safty-Criticol Software Development and Verification,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,Jiangsu,China;Collaborative Innovation Center of Norel Software Technology and Industrialization,Nanjing 210023,Jiangsu,China)

机构地区：[1]南京航空航天大学计算机科学与技术学院,江苏南京211106 [2]南京航空航天大学高安全系统的软件开发与验证技术工信部重点实验室,江苏南京211106 [3]软件新技术与产业化协同创新中心,江苏南京210023

出　　处：《西北师范大学学报(自然科学版)》2025年第2期72-84,共13页Journal of Northwest Normal University(Natural Science)

基　　金：中央高校基本科研业务费项目(NJ2024030)。

摘　　要：形式化方法通过时序逻辑(如LTL和CTL)为复杂系统时序性描述提供了新途径,但其布尔值语义无法量化相关性能属性(如能耗、时间)且难以刻画多智能体协同;时序逻辑的扩展(如PCTL和CTML)虽引入概率与实值评估,但在多智能体系统描述方面仍存在不足.本文对交替时序逻辑(ATL)进行扩展,将公式的语义从布尔值推广到实数值,提出了一种面向多智能体系统时序性能评价的语言ATML.在ATML语言基础上给出控制器综合算法,算法求解给定性能评价公式约束下的控制器,案例展示表明该方法在多智能体系统中控制器综合的可行性.Formal methods provide a new way to describe the temporal properties of complex systems through temporal logic(such as LTL and CTL),but their Boolean semantics can not quantify the relevant performance attributes(such as energy consumption,time),and are difficult to characterize multi-agent collaboration.Although the extensions of temporal logic(such as PCTL and CTML)introduce probability and real-valued evaluation,but there are still deficiencies in the description of multi-agent systems.This paper extends the alternating temporal logic(ATL),and extends the semantics of formulas from Boolean values to real values,and then proposes a language ATML for timing performance evaluation of multi-agent systems.The controller synthesis algorithm is given based on the ATML language.The algorithm solves the controller under the constraint of the given performance evaluation formula,and the case shows the feasibility of the method in the controller synthesis of multi-agent systems.

关 键 词：交替时序逻辑 性能评价 控制器综合算法 多智能体系统 

分 类 号：TP3-0[自动化与计算机技术—计算机科学与技术]