Thomas Ågotnes 教授 "合作推理"报告简述

发布时间:2017-06-03 来源:本站原创 作者:本站编辑   浏览次数:

201762日,挪威卑尔根大学 Thomas Ågotnes 教授应西南大学逻辑与智能研究中心之邀,为中心师生做了题为合作推理Reasoning about Cooperation)的报告,Jeremy Seligman教授对 Ågotnes 教授做了简要的介绍。


Ågotnes 教授首先简要介绍了CTL的语言和语义, 并就表示主体能力的模态公式<A>\phi 在一系列相关逻辑中所表达的自然语义做了介绍。进一步,Ågotnes 教授介绍了ATL的模型和语言, 对于单个主体的策略,是由针对于具体状态(state)上的可执行的行动/动作(action)的集合来定义的(之后我们称之为无记忆策略” memoryless strategy), 而群体的策略则是群体中每一主体在群体中可执行策略的集合。在ATL中的关于群体策略的模态算子 <[G]>与关于路径(path)或状态/时间(state/time)的模态算子是成对出现的,如<[G]>O\phi<[G]> \phi U \psi<[G]>[]\phi等,分别表示群体G有一个策略使得\phi在下一步为真群体G有一个策略使得在\psi真之前,\phi都为真群体G有一个策略使得\phi一直为真ATL关于群体的模态公式可以简要理解为,群体有一个策略使得对任意群体外的主体而言,无论他们采取任何策略,群体执行策略的结果不会受到影响,如之上所提的O\phi 为真,\phi U \psi为真,[]\phi为真等等,Ågotnes 教授运用一些例子阐明了这些模态公式的语义,并给出了ATL的公理系统。基于ATL中模态算子是成对出现的现象,Ågotnes 教授进一步介绍了其扩张,ATL*。在ATL*中模态算子可以分开出现,即我们可以表示类似于<[G]>(O\phi\wedge[]\psi)一样的公式。然而ATL*的公理系统和完全性问题至今还未被解决。即便如此,Ågotnes 教授给出了ATLATL*之间一些有趣的关系。比如,对于一个新的策略语义,完美记忆策略prefect recall strategy):主体对于任意有穷状态序都有一个策略。ATL不能区分无记忆策略语义与完美策略语义之间的区别, ATL*却可以。另言之,在ATL*中,存在着一个公式在完美策略语义下为真,但是在无记忆策略语义下为假。Ågotnes 教授对此进行了例示和阐明。


最后,Ågotnes 教授介绍了不可重用irrevocable)策略。一个策略对于某一主体是不可重用的,意指该主体一旦执行了该策略之后,则不可再次执行该策略。基于该策略语义的ATL的完全性问题依然未被解决。在问答环节,大家对此表现出了浓厚的兴趣,提出了很多相关的建议与问题。