A logical characterization of well branching event structures

Abstract

We develop a tense logic for reasoning about the occurrences of events in a subclass of prime event structures called well branching event structures. The well branching property ensures that two events being in conflict can always be traced back-via the causality relation-to two events being in minimal conflict. Two events are in minimal conflict if they are in conflict and their "unified" past is conflict-free. Thus the minimal conflict relation captures the branching points of the computations supported by the event structure. Our logical language has explicit modalities for talking about causality, conflict, concurrency and minimal conflict. We define the semantics of this logic using well branching event structures as Kripke frames. Our main result is a sound and complete axiomatization of the valid formulas over the chosen class of frames.