On Temporal Logic for Distributed Systems and Its Application to Processes Communicating by Interrupts

Abstract

We present a temporal logic suitable for axiomatic specification of properties of distributed systems. The temporal logic considered is first-order with atnext operators interpreted as local modalities. Its semantics, different from those provided in other approaches, does not rely on a succesor relation in a set of global states, and mirrors the nature of distributed computations. The logic introduced is applied to axiomatization of a process communication scheme based on sending and handling interrupts.