Proofs for temporal logics: focus on the multi-agent case - Archive ouverte HAL Access content directly
Book Sections Year : 2021

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

(1)
1

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 ⇤ .
Fichier principal
Vignette du fichier
CerritoProofs_FinalVersion.pdf (860.32 Ko) Télécharger le fichier
Origin : Publisher files allowed on an open archive

Dates and versions

hal-03228324 , version 1 (18-05-2021)

Identifiers

  • HAL Id : hal-03228324 , version 1

Cite

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

Share

Gmail Facebook Twitter LinkedIn More