Search. Read. Cite.

Easy to search. Easy to read. Easy to cite with credible sources.

Journal of Logic and Computation

Year: 2009  |  Volume: 19  |  Issue: 6  |  Page No.: 1245 - 1279

Labelled Tableaux for Distributed Temporal Logic

D Basin, C Caleiro, J Ramos and L. Vigano


The distributed temporal logic DTL is a logic for reasoning about temporal properties of discrete 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 labelled tableaux system for full DTL. To achieve this, we first formalize a labelled tableaux system for reasoning locally at each agent and afterwards we combine the local systems into a global one by adding rules that capture the distributed nature of DTL. We also provide examples illustrating the use of DTL and our tableaux system.

View Fulltext