License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TIME.2018.6
URN: urn:nbn:de:0030-drops-97714
URL: https://drops.dagstuhl.de/opus/volltexte/2018/9771/
Go to the corresponding LIPIcs Volume Portal

Bozzelli, Laura ; Murano, Aniello ; Sorrentino, Loredana

Results on Alternating-Time Temporal Logics with Linear Past

pdf-format:
LIPIcs-TIME-2018-6.pdf (0.6 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{bozzelli_et_al:LIPIcs:2018:9771,
  author =	{Laura Bozzelli and Aniello Murano and Loredana Sorrentino},
  title =	{{Results on Alternating-Time Temporal Logics with Linear Past}},
  booktitle =	{25th International Symposium on Temporal Representation  and Reasoning (TIME 2018)},
  pages =	{6:1--6:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-089-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{120},
  editor =	{Natasha Alechina and Kjetil N{\o}rv{\aa}g and Wojciech Penczek},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9771},
  URN =		{urn:nbn:de:0030-drops-97714},
  doi =		{10.4230/LIPIcs.TIME.2018.6},
  annote =	{Keywords: Alternating-time temporal logics, Linear Past, Model Checking}
}

Keywords: Alternating-time temporal logics, Linear Past, Model Checking
Collection: 25th International Symposium on Temporal Representation and Reasoning (TIME 2018)
Issue Date: 2018
Date of publication: 08.10.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI