A Modal Logic for a Subclass of Event Structures

Abstract

This paper introduces a non-interleaved model for the behaviour of distributed computing systems, and an accompanying temporal logic with an explicit treatment of concurrency (based on a notion of local rather than global states).

A subclass of event structures (called n-agent event structures) is used as the underlying model -- intended to describe the computational behaviour of n communicating, sequential (and possibly non-deterministic) agents. The logic is centered around indexed modalities to describe the states of knowledge of the individual agents during such a computation.

An axiom system for the logic is presented, and a full proof of its soundness and completeness (Henkin style proof) is given.