A Team Based Variant of CTL

TL;DR

This paper introduces two team semantics variants of CTL, analyzing their computational complexity for satisfiability and model checking, revealing EXPTIME-complete and PSPACE/P-complete results respectively.

Contribution

It presents novel asynchronous and synchronous team semantics for CTL and thoroughly investigates their computational properties and fundamental logical characteristics.

Findings

Satisfiability is EXPTIME-complete for both variants.

Model checking is PSPACE-complete for synchronous and P-complete for asynchronous semantics.

Fundamental properties of both semantics are established.

Abstract

We introduce two variants of computation tree logic CTL based on team semantics: an asynchronous one and a synchronous one. For both variants we investigate the computational complexity of the satisfiability as well as the model checking problem. The satisfiability problem is shown to be EXPTIME-complete. Here it does not matter which of the two semantics are considered. For model checking we prove a PSPACE-completeness for the synchronous case, and show P-completeness for the asynchronous case. Furthermore we prove several interesting fundamental properties of both semantics.