摘要
形式化方法通过时序逻辑(如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.
作者
黄若寒
曹子宁
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)
出处
《西北师范大学学报(自然科学版)》
2025年第2期72-84,共13页
Journal of Northwest Normal University(Natural Science)
基金
中央高校基本科研业务费项目(NJ2024030)。
关键词
交替时序逻辑
性能评价
控制器综合算法
多智能体系统
alternating temporal logic
performance evaluation
controller synthesis algorithm
multi-agent system
