Alternating-time temporal logics with linear past

We investigate the succinctness gap between two known equally-expressive and different linear-past extensions of standard ATL⁎. We establish by formal non-trivial arguments that the ‘memoryful’ linear-past extension (the history leading to the current state is taken into account) can be exponentially more succinct than the standard ‘local’ linear-past extension (the history leading to the current state is forgotten). As a second contribution, we consider the ATL-like fragment, denoted ATLlp, of the known ‘memoryful’ linear-past extension of ATL⁎. We show that ATLlp is strictly more expressive than ATL, and interestingly, it can be exponentially more succinct than the more expressive logic ATL⁎. Moreover, we prove that both satisfiability and model-checking for the logic ATLlp are EXPTIME -complete.