Fulltext

Labelled Tableaux for Distributed Temporal Logic

Basin, David ; Basin, David ; Caleiro, Carlos ; Ramos, Jaime ; Viganò, Luca ; Viganò, Luca

In: Journal of Logic and Computation, 2009, vol. 19, no. 6, p. 1245-1279

Add to personal list
    Title
    • Labelled Tableaux for Distributed Temporal Logic
    Author
    • Basin, David. Department of Computer Science, ETH Zurich, Switzerland.E-mail: basin@inf.ethz.ch
    • Basin, David. Department of Computer Science, ETH Zurich, Switzerland.E-mail
    • Caleiro, Carlos. Department of Computer Science, ETH Zurich, Switzerland.E-mail
    • Ramos, Jaime. Department of Computer Science, ETH Zurich, Switzerland.E-mail
    • Viganò, Luca. Department of Computer Science, ETH Zurich, Switzerland.E-mail
    • Viganò, Luca. Department of Computer Science, University of Verona, Italy.E-mail: luca.vigano@univr.it
    Document Type
    • Postprint
    Language
    • English
    Published in
    • Journal of Logic and Computation, 2009, vol. 19, no. 6, p. 1245-1279. Oxford University Press
    Other Version
    OAI-PMH Identifier
    • oai:doc.rero.ch:302017
    Summary
    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