Strategic (Timed) Computation Tree Logic

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 .