Model checking distributed temporal logic

Francisco Dionisio, Jaime Ramos, Fernando Subtil, Luca Viganò

Research output: Contribution to journalArticlepeer-review

120 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 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 an automata-theoretic model checking algorithm for DTL. To this end, we propose a notion of distributed transition system that will be used to specify the system to be verified. The properties that the system should meet are specified in DTL. In order to capture the models of these properties, we propose the notions of generalized distributed Bu ̈chi automaton and of distributed Bu ̈chi automaton. With these concepts, we are able to adapt results from automata-theoretic approaches to model checking in LTL to the distributed case.
Original languageEnglish
Number of pages36
JournalLOGIC JOURNAL- IGPL
Publication statusAccepted/In press - 14 Mar 2024

Fingerprint

Dive into the research topics of 'Model checking distributed temporal logic'. Together they form a unique fingerprint.

Cite this