Abstract
Temporal logics are a well investigated formalism for the specification, verification, and synthesis of reactive systems. Within this family, Alternating-Time Temporal Logic (Atl \(^{*}\), for short) has been introduced as a useful generalization of classical linear- and branching-time temporal logics, by allowing temporal operators to be indexed by coalitions of agents. Classically, temporal logics are memoryless: once a path in the computation tree is quantified at a given node, the computation that has led to that node is forgotten. Recently, mCtl \(^{*}\) has been defined as a memoryful variant of Ctl \(^{*}\), where path quantification is memoryful. In the context of multi-agent planning, memoryful quantification enables agents to “relent” and change their goals and strategies depending on their history. In this work, we define mAtl \(^{*}\), a memoryful extension of Atl \(^{*}\), in which a formula is satisfied at a certain node of a path by taking into account both the future and the past. We study the expressive power of mAtl \(^{*}\), its succinctness, as well as related decision problems. We also investigate the relationship between memoryful quantification and past modalities and show their equivalence. We show that both the memoryful and the past extensions come without any computational price; indeed, we prove that both the satisfiability and the model-checking problems are 2ExpTime-complete, as they are for Atl \(^{*}\).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
In Middle English to relent means to melt. In modern English it is used only in the combination of “relentless”.
- 2.
A pure-past formula contains only past-time operators. In Item 4, we also consider pure-future formulas, which contain only future-time operators, and pure-present formulas, which do not contain any temporal operator at all.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2013 Atlantis Press and the authors
About this chapter
Cite this chapter
Mogavero, F. (2013). Relentful Strategic Reasoning. In: Logics in Computer Science. Atlantis Studies in Computing, vol 3. Atlantis Press, Paris. https://doi.org/10.2991/978-94-91216-95-4_4
Download citation
DOI: https://doi.org/10.2991/978-94-91216-95-4_4
Published:
Publisher Name: Atlantis Press, Paris
Print ISBN: 978-94-91216-94-7
Online ISBN: 978-94-91216-95-4
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)