A Labeled Tableaux System for the Distributed Temporal Logic DTL

DTL is a distributed temporal 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. We present a sound and complete labeled tableaux system for future-time DTL. To achieve this, we first formalize a labeled tableaux system for reasoning locally at each agent, which provides a system for full future-time LTL, and afterwards we combine the local systems into a global one by adding rules that capture the distributed nature of DTL.