The Logic of Events Bic09, BC08] is a logic inspired by the work of Winskel on event structures Win88], developed to deal with: (1) events; (2) their spatial locations; and (3) their “temporal locations,” represented as a well-founded partial ordering of these events (causal order). An event is triggered by receipt of a message; the data of the message body is called primitive information of the event. The Logic of Events provides ways to describe events by, among other things giving access to their associated information.
An event ordering is a structure consisting of: (1) a set of events, (2) a location function loc that associates a location with each event, (3) an information function info that associates primitive information with each event, and (4) a well-founded causal ordering relation on events < Lam78]. An event ordering represents a single run of a distributed system.
A basic concept in the Logic of Events is an event class Bic09], which effectively partitions the events of an event ordering into those it “recognizes” and those it does not, and associates values to the events it recognizes. Different classes may recognize the same event and assign it different values. For example, one class may recognize the arrival of a message and associate it with its primitive information, the message data. Another class may recognize that, in the context of some protocol, the arrival of that message signifies successful completion of the protocol and assign to it a value meaning “consensus achieved.” We specify a concurrent system in EventML by defining event classes that appropriately classify system events.
Event classes have two facets: a programming one and a logical one. On the logical side, event classes specify information flow on a network of reactive agents by observing the information computed by the agents when events occur, i.e., on receipt of messages. On the programming side, event classes can be seen as processes that aggregate information in an internal state from input messages and past observations, and compute appropriate values for them.
Formally, an event class X is a function whose inputs are event ordering and an event, and whose output is a bag of values (observations). If the observations are of type T, then the class X is called an event class of type T. The associated type constructor is Class(T) = EO → E → Bag(T), where EO is the type of event orderings and E the type of events.
Expressions denoting events or event orderings do not occur in EventML programs; the types EO and E are not EventML types. We will refer to them when explaining the semantics of programs or reasoning about them. In particular, we will speak about the bag of values returned by a class (at some event) and will reason about the event class relation: we say that the class X observes v at event e (in an event ordering eo), and write v ∈ X(e), if v is a member of (X eo e). In our discussions, eo will be clear from context, so our notation omits it. If the bag of return values is nonempty we say that event e is in the class X, and that e is an X-event. If an event class always returns either a singleton bag or an empty bag, we call it a single-valued class.
Event classes are ultimately defined from one kind of primitive event class (a base class) using a small number of primitive class combinators—though users can define new combinators, and we supply a useful library of them. These primitives, and a variety of useful defined combinators are introduced in the examples of section 3. Their definitions are gathered together in section 7.
The inductive logical form of a specification is a first order formula that characterizes completely the observations (the responses) made by the main class of the specification in terms of the event class relation. The formula is inductive because it typically characterizes the responses at event e in terms of observations made by a sub-component at a prior event e′ < e. Such inductive logical forms are automatically generated in Nuprl from event class definitions, and simplified using various rewritings. From an inductive logical form we can prove invariants of the specification by induction on causal order.
