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

摘要

形式化方法通过时序逻辑(如LTL和CTL)为复杂系统时序性描述提供了新途径,但其布尔值语义无法量化相关性能属性(如能耗、时间)且难以刻画多智能体协同;时序逻辑的扩展(如PCTL和CTML)虽引入概率与实值评估,但在多智能体系统描述方面仍存在不足.本文对交替时序逻辑(ATL)进行扩展,将公式的语义从布尔值推广到实数值,提出了一种面向多智能体系统时序性能评价的语言ATML.在ATML语言基础上给出控制器综合算法,算法求解给定性能评价公式约束下的控制器,案例展示表明该方法在多智能体系统中控制器综合的可行性.

关键词

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