作　　者： ;

机构地区： 中山大学人文科学学院逻辑与认知研究所

出　　处： 《逻辑学研究》 2009年第4期1-15,共15页

摘　　要： CTL模型检测技术已被广泛应用于形式验证领域。交互时态逻辑(ATL)是对CTL的一个扩展,用于表达多主体博弈结构上的性质。ATL使用合作算子来表达多个主体能够通过合作保证系统的设计目标。在实际应用中,我们需要知道主体的行动与系统的输出状态之间具有因果关系。在本文中,我们通过引入新的模态算子扩展ATL,使得这种因果关系得到表达。我们使用两种方式的扩展。其中之一是从主体的能力出发,直观上,如果一些主体可以通过合作的行动来保证系统进入某个状态,同时,这些主体也可以通过合作的行动保证系统不进入这个状态,则这些主体的行动与该系统状态间具有更强的因果关系。我们使用的另一种方式是从系统状态出发。我们考虑要想使系统进入某状态,哪些主体的行动的必不可少的,哪些主体的行动是充分的但非必要的条件。在本文中,我们扩展后的逻辑CATL和SATL表达力强于ATL,但计算复杂性与ATL相同。 CTL model checking has been widely used in formal specification and verification. The so called alternating time temporal logic （ATL） is an extension of CTL to formalize a game-like multiplayer specification. The property that players can guarantee desired system state is modeled in ATL by using cooperation operators. In practice, it is usually important to know that a causal link indeed exists between players＇ actions and states of a system, especially when modularity is considered. We extend ATL by introducing new operators to characterize causalities. The resultant logics are more expressive than ATL, while share the same computational complexity.

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

领　　域： [自动化与计算机技术] [自动化与计算机技术] [自动化与计算机技术] [自动化与计算机技术]