一个用于表达因果关系的ATL的扩展(英文)

作     者：刘虎 Hu Liu

作者机构：中山大学逻辑与认知研究所 

基　　金：supported by A Foundation for the Author of National Excellent Doctoral Dissertation of PR China(FANEDD 2007B01) 

出 版 物：《逻辑学研究》 (Studies in Logic)

年 卷 期：2009年第2卷第4期

页      码：1-15页

摘      要：CTL模型检测技术已被广泛应用于形式验证领域。交互时态逻辑(ATL)是对CTL的一个扩展,用于表达多主体博弈结构上的性质。ATL使用合作算子来表达多个主体能够通过合作保证系统的设计目标。在实际应用中,我们需要知道主体的行动与系统的输出状态之间具有因果关系。在本文中,我们通过引入新的模态算子扩展ATL,使得这种因果关系得到表达。我们使用两种方式的扩展。其中之一是从主体的能力出发,直观上,如果一些主体可以通过合作的行动来保证系统进入某个状态,同时,这些主体也可以通过合作的行动保证系统不进入这个状态,则这些主体的行动与该系统状态间具有更强的因果关系。我们使用的另一种方式是从系统状态出发。我们考虑要想使系统进入某状态,哪些主体的行动的必不可少的,哪些主体的行动是充分的但非必要的条件。在本文中,我们扩展后的逻辑CATL和SATL表达力强于ATL,但计算复杂性与ATL相同。

主 题 词：因果关系 时态逻辑 计算复杂性 检测技术 博弈结构 设计目标 CTL 系统 

学科分类：01[哲学] 0101[哲学-哲学类] 010104[010104] 

D　O　I：10.3969/j.issn.1674-3202.2009.04.001

馆 藏 号：203579618...