Skip to Main content Skip to Navigation
Book sections

Proofs for temporal logics: focus on the multi-agent case

Abstract : In this work we present and discuss some features of proofs in the case of temporal logics. More precisely, we discuss the relation between proofs for temporal logics built in two distinct frameworks: sequent calculi and tableau based calculi, taking as a typical example of temporal logic propositional LTL (Linear Temporal Logic). This work is a survey focussing on the comparison between sequent calculi and tableaux proofs. We also illustrate with some details the tableau based proofs for ATL ⇤ (the most expressive logic of the family of Alternating-Time Temporal Logics) proposed by Amélie David in 2015. Such a logic takes into account the presence of several agents that can cooperate (or not) in a given scenario to achieve some temporal objectives. Up to our knowledge, no proof-system in the sequent style is known for ATL ⇤ .
Document type :
Book sections
Complete list of metadata

https://hal.archives-ouvertes.fr/hal-03228324
Contributor : Serenella Cerrito Connect in order to contact the contributor
Submitted on : Tuesday, May 18, 2021 - 9:34:54 AM
Last modification on : Saturday, July 23, 2022 - 1:37:02 PM
Long-term archiving on: : Thursday, August 19, 2021 - 6:22:25 PM

File

CerritoProofs_FinalVersion.pdf
Publisher files allowed on an open archive

Identifiers

  • HAL Id : hal-03228324, version 1

Citation

Serenella Cerrito. Proofs for temporal logics: focus on the multi-agent case. Proofs, In press. ⟨hal-03228324⟩

Share

Metrics

Record views

26

Files downloads

40