DROPS

Document

DOI: 10.4230/LIPIcs.TIME.2018.6

Results on Alternating-Time Temporal Logics with Linear Past

Authors: Laura Bozzelli, Aniello Murano, and Loredana Sorrentino

Published in: LIPIcs, Volume 120, 25th International Symposium on Temporal Representation and Reasoning (TIME 2018)

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.

Cite as

Laura Bozzelli, Aniello Murano, and Loredana Sorrentino. Results on Alternating-Time Temporal Logics with Linear Past. In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 6:1-6:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bozzelli_et_al:LIPIcs.TIME.2018.6,
  author =	{Bozzelli, Laura and Murano, Aniello and Sorrentino, Loredana},
  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 =	{Alechina, Natasha and N{\o}rv\r{a}g, Kjetil and Penczek, Wojciech},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2018.6},
  URN =		{urn:nbn:de:0030-drops-97714},
  doi =		{10.4230/LIPIcs.TIME.2018.6},
  annote =	{Keywords: Alternating-time temporal logics, Linear Past, Model Checking}
}

Document

DOI: 10.4230/LIPIcs.TIME.2017.6

Hierarchical Cost-Parity Games

Authors: Laura Bozzelli, Aniello Murano, Giuseppe Perelli, and Loredana Sorrentino

Published in: LIPIcs, Volume 90, 24th International Symposium on Temporal Representation and Reasoning (TIME 2017)

Abstract

Cost-parity games are a fundamental tool in system design for the analysis of reactive and distributed systems that recently have received a lot of attention from the formal methods research community. They allow to reason about the time delay on the requests granted by systems, with a bounded consumption of resources, in their executions. In this paper, we contribute to research on Cost-parity games by combining them with hierarchical systems, a successful method for the succinct representation of models. We show that determining the winner of a Hierarchical Cost-parity Game is PSpace-Complete, thus matching the complexity of the proper special case of Hierarchical Parity Games. This shows that reasoning about temporal delay can be addressed at a free cost in terms of complexity.

Cite as

Laura Bozzelli, Aniello Murano, Giuseppe Perelli, and Loredana Sorrentino. Hierarchical Cost-Parity Games. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bozzelli_et_al:LIPIcs.TIME.2017.6,
  author =	{Bozzelli, Laura and Murano, Aniello and Perelli, Giuseppe and Sorrentino, Loredana},
  title =	{{Hierarchical Cost-Parity Games}},
  booktitle =	{24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
  pages =	{6:1--6:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-052-1},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{90},
  editor =	{Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.6},
  URN =		{urn:nbn:de:0030-drops-79175},
  doi =		{10.4230/LIPIcs.TIME.2017.6},
  annote =	{Keywords: Parity Games, Cost-Parity Games, Hierarchical Systems, System Verification}
}

Search Results

Documents authored by Sorrentino, Loredana

Results on Alternating-Time Temporal Logics with Linear Past

Abstract

Cite as

Hierarchical Cost-Parity Games

Abstract

Cite as

Thanks for your feedback!

Could not send message