Abstract

Mark Bickford and Bob Constable

In 2003 we defined and formalized a logic of events for specifiying distributed computing tasks and for reasoning about distributed systems.  This is a very abstract account of distributed computing that applies to natural processes as well as to processes in an asynchronous message passing network computing model.

Although the logic is very abstract, we can show that it is "not too abstract" in the sense that from constructive proofs that tasks are achievable, we can extract abstract distributed systems.  Mark and his colleague David Guaspari have translated this abstract code, called Message Automata, into Java.

The logic naturally formalizes the intuitive language of events that we have been using for the past several years in work with Robbert and Ken on Ensemble and in recent efforts to formalize parts of the APSS security protocol of Lidong Zhou, Fred, and Robbert.