2026-07-22T21:49:13Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9771 2024-03-06T10:44:53Z ddc:004 open_access

Results on Alternating-Time Temporal Logics with Linear Past Bozzelli, Laura Murano, Aniello Sorrentino, Loredana Alternating-time temporal logics Linear Past Model Checking We investigate the succinctness gap between two known equally-expressive and different linear-past extensions of standard CTL^* (resp., 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 ATL_{lp}, of the known "memoryful" linear-past extension of ATL^{*}. We show that ATL_{lp} 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 ATL_{lp} are Exptime-complete. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Laura Bozzelli and Aniello Murano and Loredana Sorrentino 2018 Is Part Of LIPIcs, Volume 120, 25th International Symposium on Temporal Representation and Reasoning (TIME 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TIME.2018.6 urn:nbn:de:0030-drops-97714 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.6 eng https://creativecommons.org/licenses/by/3.0/legalcode