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-completeess for the synchronous case, and show P-completeness for the asynchronous case. Furthermore we prove several interesting fundamental properties of both semantics. |
Year | DOI | Venue |
---|---|---|
2015 | 10.1109/TIME.2015.11 | Workshops |
Keywords | Field | DocType |
computation tree logic,team semantics,computational complexity | Computation tree logic,Discrete mathematics,Operational semantics,Model checking,Axiomatic semantics,Computational semantics,Boolean satisfiability problem,Denotational semantics,Algorithm,Theoretical computer science,Mathematics,Well-founded semantics | Conference |
ISSN | Citations | PageRank |
1530-1311 | 4 | 0.40 |
References | Authors | |
19 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Andreas Krebs | 1 | 21 | 8.20 |
Arne Meier | 2 | 126 | 19.00 |
Jonni Virtema | 3 | 79 | 11.93 |