B\"uchi automata for distributed temporal logic

TL;DR

This paper introduces a novel distributed Büchi automaton framework designed to facilitate model-checking for the distributed temporal logic DTL, which models local reasoning about temporal properties in distributed systems.

Contribution

It proposes a new notion of distributed Büchi automaton tailored for DTL, enabling effective model-checking of distributed temporal properties.

Findings

Enables model-checking of distributed temporal logic DTL.

Provides a formal automaton framework for distributed systems.

Facilitates verification of local temporal properties in distributed environments.

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 provided 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 novel notion of distributed B\"uchi automaton envisaged to encompass DTL with a model-checking mechanism.