A logical characterization of well branching event structures

Mukund, Madhavan ; Thiagarajan, P. S. (1992) A logical characterization of well branching event structures Theoretical Computer Science, 96 (1). pp. 35-72. ISSN 0304-3975

Full text not available from this repository.

Official URL: http://www.sciencedirect.com/science/article/pii/0...

Related URL: http://dx.doi.org/10.1016/0304-3975(92)90181-E


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.

Item Type:Article
Source:Copyright of this article belongs to Elsevier Science.
ID Code:50511
Deposited On:25 Jul 2011 11:43
Last Modified:25 Jul 2011 11:43

Repository Staff Only: item control page