A Complete Temporal and Spatial Logic for Distributed Systems

Abstract. In this paper, we introduce a spatial and temporal logic for reasoning about distributed computation. The logic is a combination of an extension of hybrid logic, that allows us to reason about the spatial structure of a computation, and linear temporal logic, which accounts for the temporal aspects. On the pragmatic side, we show the wide applicability of this logic by means of many examples. Our main technical contribution is completeness of the logic both with respect to spatial/temporal structures and a class of spatial transition systems.

• Type: Conference
• Year: 2005
• Where: FROCOS
• Authors: Dirk Pattinson, Bernhard Reus
• Keywords: FROCOS 2005, Hybrid Logic, Linear Temporal Logic, Temporal Logic