2015 22nd International Symposium on Temporal Representation and Reasoning (TIME) (2015)
Sept. 23, 2015 to Sept. 25, 2015
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TIME.2015.11
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-completeess for the synchronous case, and show P-completeness for the asynchronous case. Furthermore we prove several interesting fundamental properties of both semantics.
Semantics, Model checking, Computational modeling, Computational complexity, Context, Syntactics
A. Krebs, A. Meier and J. Virtema, "A Team Based Variant of CTL," 2015 22nd International Symposium on Temporal Representation and Reasoning (TIME), Kassel, Germany, 2015, pp. 140-149.