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 language | English |
---|---|
Number of pages | 36 |
Journal | LOGIC JOURNAL- IGPL |
Publication status | Accepted/In press - 14 Mar 2024 |