一个用于表达因果关系的ATL的扩展

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

An Extension of ATL for Model Checking Causality

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.