A tableaux-based decision procedure for distributed temporal logic

Carlos Caleiro; Paula Gouveia; Jaime Ramos; Luca Vigano

A tableaux-based decision procedure for distributed temporal logic

Carlos Caleiro
, Paula Gouveia
, Jaime Ramos
, Luca Vigano

Instituto Superior Técnico, Universidade de Lisboa

Research output: Chapter in Book/Report/Conference proceeding › Chapter › peer-review

1 Downloads (Pure)

Abstract

The distributed temporal logic DTL is a logic for reasoning about temporal properties of distributed systems from the local point of view of the system’s agents, which are assumed to execute sequentially and to interact by means of synchronous event sharing. Different versions of DTL have been given over the years for a number of different applications, reflecting different perspectives on how non-local information can be accessed by each agent. In this paper, we propose a decidable Fisher-Ladner-style tableaux system for an anchored version of DTL. Our tableaux system is built on top of a tableaux system for LTL and integrates in a smooth way both the usual rules for the temporal operators and rules for tackling the specific communication features of DTL. We endow our tableaux system with a specific decision procedure for dealing with entailment and we show that our system can be coupled with a model-checking-like feature for deciding global DTL properties.

Original language	English
Title of host publication	Logic and Computation
Subtitle of host publication	Essays in Honour of Amilcar Sernadas
Publisher	College Publications, London
Pages	73-124
Number of pages	51
Publication status	Published - 5 Jul 2017

Cite this

@inbook{f95cc031d0f34c19a7102a7096abb38e,

title = "A tableaux-based decision procedure for distributed temporal logic",

abstract = "The distributed temporal logic DTL is a logic for reasoning about temporal properties of distributed systems from the local point of view of the system{\textquoteright}s agents, which are assumed to execute sequentially and to interact by means of synchronous event sharing. Different versions of DTL have been given over the years for a number of different applications, reflecting different perspectives on how non-local information can be accessed by each agent. In this paper, we propose a decidable Fisher-Ladner-style tableaux system for an anchored version of DTL. Our tableaux system is built on top of a tableaux system for LTL and integrates in a smooth way both the usual rules for the temporal operators and rules for tackling the specific communication features of DTL. We endow our tableaux system with a specific decision procedure for dealing with entailment and we show that our system can be coupled with a model-checking-like feature for deciding global DTL properties.",

author = "Carlos Caleiro and Paula Gouveia and Jaime Ramos and Luca Vigano",

year = "2017",

month = jul,

day = "5",

language = "English",

pages = "73--124",

booktitle = "Logic and Computation",

publisher = "College Publications, London",

}

TY - CHAP

T1 - A tableaux-based decision procedure for distributed temporal logic

AU - Caleiro, Carlos

AU - Gouveia, Paula

AU - Ramos, Jaime

AU - Vigano, Luca

PY - 2017/7/5

Y1 - 2017/7/5

N2 - The distributed temporal logic DTL is a logic for reasoning about temporal properties of distributed systems from the local point of view of the system’s agents, which are assumed to execute sequentially and to interact by means of synchronous event sharing. Different versions of DTL have been given over the years for a number of different applications, reflecting different perspectives on how non-local information can be accessed by each agent. In this paper, we propose a decidable Fisher-Ladner-style tableaux system for an anchored version of DTL. Our tableaux system is built on top of a tableaux system for LTL and integrates in a smooth way both the usual rules for the temporal operators and rules for tackling the specific communication features of DTL. We endow our tableaux system with a specific decision procedure for dealing with entailment and we show that our system can be coupled with a model-checking-like feature for deciding global DTL properties.

AB - The distributed temporal logic DTL is a logic for reasoning about temporal properties of distributed systems from the local point of view of the system’s agents, which are assumed to execute sequentially and to interact by means of synchronous event sharing. Different versions of DTL have been given over the years for a number of different applications, reflecting different perspectives on how non-local information can be accessed by each agent. In this paper, we propose a decidable Fisher-Ladner-style tableaux system for an anchored version of DTL. Our tableaux system is built on top of a tableaux system for LTL and integrates in a smooth way both the usual rules for the temporal operators and rules for tackling the specific communication features of DTL. We endow our tableaux system with a specific decision procedure for dealing with entailment and we show that our system can be coupled with a model-checking-like feature for deciding global DTL properties.

M3 - Chapter

SP - 73

EP - 124

BT - Logic and Computation

PB - College Publications, London

ER -

A tableaux-based decision procedure for distributed temporal logic

Abstract

Fingerprint

Cite this