Alternating-time temporal logics with linear past

DOI10.1016/j.tcs.2019.11.028zbMath1433.03050OpenAlexW2996139545MaRDI QIDQ1989330

Loredana Sorrentino, Laura Bozzelli, Aniello Murano

Publication date: 21 April 2020

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2019.11.028

zbMATH Keywords

formal verificationmulti-agent systemsstrategic reasoningalternating-time temporal logiclogics with past modalities

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items (1)

A separation theorem for discrete-time interval temporal logic

Uses Software

• MCMAS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• \textit{Once} and \textit{for all}
• A hierarchy of temporal logics with past
• Strategy logic
• Reasoning about infinite computations
• Practical verification of multi-agent systems against \textsc{Slk} specifications
• Specification in CTL + past for verification in CTL.
• The complexity of propositional linear temporal logics in simple cases
• Coalitional Responsibility in Strategic Settings
• An alternating-time temporal logic with knowledge, perfect recall and past: axiomatisation and model-checking
• Reasoning About Strategies
• Relentful strategic reasoning in alternating-time temporal logic
• Alternating-time temporal logic
• ATL* Satisfiability Is 2EXPTIME-Complete
• The Complexity of Enriched Mu-Calculi
• Automata for the modal μ-calculus and related results
• ATL with Strategy Contexts and Bounded Memory
• Satisfiability and Finite Model Property for the Alternating-Time μ-Calculus
• “Sometimes” and “not never” revisited
• Alternation
• Characterising Responsibility in Organisational Structures: The Problem of Many Hands
• An automata-theoretic approach to branching-time model checking
• The Complexity of CTL* + Linear Past

This page was built for publication: Alternating-time temporal logics with linear past