Logics in computer science. A study on extensions of temporal and strategic logics (Q357126)

Temporal logics extend classical logic by means of modalities that express statements concerning time. Semantics of formulas is given in terms of paths, that is, infinite sequences of truth evaluations. Among the mainly considered temporal logics are linear-time temporal logics, such as LTL, and branching-time temporal logics, such as CTL and CTL*. The main difference between these two categories is that linear-time temporal logics assume the existence of a unique future, while branching-time temporal logics treat time nondeterministically and thus have modalities to state properties holding in some or all possible future paths. Another widely used temporal logic is an extension of CTL* called alternating-time temporal logic, or simply ATL*. Essentially, in ATL* ``strategic modalities'' are introduced in order to express that some or all agents in a multi-agent system obey a certain strategy. This book collects four works of the author in the context of temporal logics. In the first work, CTL is extended by means of graded path modalities, that is, modalities of the form \(E^{\geq g}\) and \(A^{< g}\), where \(g\) is either a positive integer or \(\omega\). Intuitively, \(E^{\geq g} \phi\) means that formula \(\phi\) is true in at least \(g\) paths, while \(A^{< g} \phi\) means that \(\phi\) is true in all but less that \(g\) paths. The resulting logic is called graded CTL, or GCTL for short. It is exponentially more succinct than CTL and does not increase computational complexity, which remains EXPTIME. Several semantic notions are introduced and used to show nontrivial properties of the language. In the second work, the author introduces a new temporal logic, called MCTL*, that extends CTL* by means of minimal model operators. These operators allow for quantification over models and in particular allow to select minimal submodels. Several semantics are proposed, one of which also enjoying decidability of the associated satisfiability problem. The third work introduces a new logic, called SL, for reasoning about strategies in multi-agent concurrent systems. It is more general than the previous logic SL introduced by \textit{K. Chatterjee} et al. [Lect. Notes Comput. Sci. 4703, 59--73 (2007; Zbl 1151.03327)], has the same complexity for the model checking problem, and the satisfiability problem remains undecidable. In the fourth work, the author introduces mATL*, a temporal logic extending ATL* by means of memoryful semantics, that is, semantics in which satisfaction of a formula depends also on the past states of the system. It is equivalent to ATL* but exponentially more succinct. Satisfiability and model checking remain 2-EXPTIME-complete. To sum up, an interesting reading with several non-trivial results concerning new temporal logics and their computational properties.