A Team Based Variant of CTL
Logic in Computer Science
2015-07-15 v2 Computational Complexity
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.
Keywords
Cite
@article{arxiv.1505.01964,
title = {A Team Based Variant of CTL},
author = {Andreas Krebs and Arne Meier and Jonni Virtema},
journal= {arXiv preprint arXiv:1505.01964},
year = {2015}
}
Comments
TIME 2015 conference version, modified title and motiviation