JAAMAS Journal 2026 Journal Article
Strategic (timed) computation tree logic
- Jaime Arias
- Wojciech Jamroga
- Teofil Sidoruk
Abstract We define extensions of \(\textbf{CTL}\) and TCTL with strategic operators, called Strategic \(\textbf{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 \(_{{\textbf {ir}}}\) is of the same complexity as for ATL \(_{{\textbf {ir}}}\), the model checking problem for STCTL \(_{{\textbf {iR}}}\) is of the same complexity as for TCTL, while for STCTL \(_{{\textbf {iR}}}\) it is undecidable as for ATL \(_{{\textbf {iR}}}\). The above results suggest to use SCTL \(_{{\textbf {ir}}}\) and STCTL \(_{{\textbf {ir}}}\) in practical applications. Therefore, we use the tool IMITATOR to support model checking of STCTL \(_{{\textbf {ir}}}\).