Affiliations: [a] Institute of Informatics, University of Warsaw, 00-901, Poland | [b] Department of Computing, Imperial College, London SW7 2BZ, England | [c] Sektion Mathematik, Karl-Marx-Universitaet, 7010 Leipzig, GDR
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.
Keywords: axiom system, communication mechanism, distributed system, interrupt, semantic consequence, semantics of concurrent computations, temporal logic
