Strategic (Timed) Computation Tree Logic

TL;DR

This paper introduces strategic extensions of CTL and TCTL with new semantics for timed automata, demonstrating their increased expressiveness and analyzing the complexity of model checking, supported by a practical tool implementation.

Contribution

It defines SCTL and STCTL logics with various semantics, proves their relative expressiveness and complexity, and implements model checking with the IMITATOR tool.

Findings

SCTL is more expressive than ATL under all semantics.

Model checking complexity varies: same as ATL for SCTL[ir], same as TCTL for STCTL[ir], undecidable for STCTL[iR].

Practical model checking supported by IMITATOR.

Abstract

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].