Logics for describing computation: syntax, semantics, and computational complexity of the decision problem

The talk is devoted to logics intended for the formal description of computational processes—primarily propositional dynamic logics, as well as temporal logics such as $\mathsf{LTL}$ (linear-time temporal logic), $\mathsf{CTL}$ (computation tree logic), and $\mathsf{ATL}$ (alternating-time temporal logic). We provide syntactic and semantic descriptions of these logics, with particular attention to the complexity of the decision problem: we present complexity bounds both for the full languages and for various fragments (including those with a bounded number of variables). We also address not only decidable but also undecidable problems.