We define extensions of CTL and TCTL with strategic operators, called Strategic CTL (SCTL) and Strategic TCTL (STCTL), respectively. For each of the above logics we give a synchronous and asynchronous semantics, i.e., STCTL is interpreted over networks of extended Timed Automata (TA) that either make synchronous moves or synchronise via joint actions. We consider several semantics regarding information: imperfect (i) and perfect (I), and recall: imperfect (r) and perfect (R). We prove that SCTL is more expressive than ATL for all semantics, and this holds for the timed versions as well. Moreover, the model checking problem for SCTL[ir] is of the same complexity as for ATL[ir], the model checking problem for STCTL[ir] is of the same complexity as for TCTL, while for STCTL[iR] it is undecidable as for ATL[iR]. The above results suggest to use SCTL[ir] and STCTL[ir] in practical applications. Therefore, we use the tool IMITATOR to support model checking of STCTL[ir].

翻译：我们定义了带有策略算子的CTL和TCTL的扩展，分别称为策略CTL（SCTL）和策略时间化CTL（STCTL）。针对上述每种逻辑，我们给出了同步和异步语义，即STCTL在扩展时间自动机（TA）网络上进行解释，这些网络要么执行同步移动，要么通过联合动作进行同步。我们考虑了关于信息的多种语义：不完全信息（i）和完全信息（I），以及记忆：不完全记忆（r）和完全记忆（R）。我们证明SCTL在所有语义下均比ATL更具表达力，并且这一结论对时间化版本同样成立。此外，SCTL[ir]的模型检测问题与ATL[ir]具有相同复杂度，STCTL[ir]的模型检测问题与TCTL具有相同复杂度，而STCTL[iR]的模型检测问题与ATL[iR]一样不可判定。上述结果表明，在实际应用中应使用SCTL[ir]和STCTL[ir]。因此，我们利用工具IMITATOR来支持STCTL[ir]的模型检测。